BoundaryChecks.lean

1 module
2 public import TransferSupport
3 import all TransferSupport
4 import all PacketIR
5 import all QuantumPacketCore
6 public import Mathlib.Tactic.NormNum
7 public import Mathlib.Tactic.FinCases
8 public import Mathlib.Tactic.Linarith
9 
10 /-!
11 Author: Komorebi P.
12 Boundary checks for the strengthened Paper VIII.
13 A support path need not survive cancellation.
14 A nonempty positive allocation requires a strictly positive total budget (item 8.4).
15 These are not proofs of the full continuous precision optimization theorem.
16 -/
17 
18 public section
19 set_option autoImplicit false
20 set_option backward.isDefEq.respectTransparency false
21 set_option backward.isDefEq.respectTransparency.types false
22 namespace KomorebiPaperVIII
23 open scoped BigOperators
24 open KomorebiPaperVII
25 
26 /-- A rational, nonzero matrix with exact square zero. -/
27 def cancellationMatrix : Matrix (Fin 2) (Fin 2) ℚ := fun i _ => if i = 0 then 1 else -1
28 
29 theorem cancellation_square_zero : cancellationMatrix ^ 2 = 0 := by
30   ext i j
31   fin_cases i <;> fin_cases j <;>
32     norm_num [pow_two, cancellationMatrix, Matrix.mul_apply, Fin.sum_univ_two]
33 
34 theorem cancellation_block_nonzero :
35     (coordinatePackets (K := ℚ) (fun i : Fin 2 => i)).block cancellationMatrix 0 0 ≠ 0 := by
36   intro h
37   have he := congrArg (fun M : Matrix (Fin 2) (Fin 2) ℚ => M 0 0) h
38   norm_num [coordinatePackets, PacketFamily.block, cancellationMatrix,
39     Matrix.mul_apply, Fin.sum_univ_two, Matrix.diagonal_apply] at he
40 
41 /-- Exact counterexample to replacing the support inclusion by equality. -/
42 theorem paths_can_cancel :
43     let P := coordinatePackets (K := ℚ) (fun i : Fin 2 => i)
44     TransferPath P cancellationMatrix 2 0 0 ∧ P.block (cancellationMatrix ^ 2) 0 0 = 0 := by
45   dsimp
46   constructor
47   · exact ⟨0, cancellation_block_nonzero, 0, cancellation_block_nonzero, rfl⟩
48   · rw [cancellation_square_zero]
49     simp [PacketFamily.block]
50 
51 /-- Positive sensitivities and tolerances force the equality budget to be positive. -/
52 theorem positive_allocation_budget {E : Type*} [Fintype E] [Nonempty E]
53     (s ε : E → ℝ) (hs : ∀ e, 0 < s e) (hε : ∀ e, 0 < ε e) :
54     0 < ∑ e, s e * ε e := by
55   exact Finset.sum_pos (fun e _ => mul_pos (hs e) (hε e)) Finset.univ_nonempty
56 
57 /-- Theorem 8.4 cannot assert a minimizer at a nonpositive budget on a nonempty edge set. -/
58 theorem no_positive_allocation_nonpositive_budget {E : Type*} [Fintype E] [Nonempty E]
59     (s : E → ℝ) (hs : ∀ e, 0 < s e) (τ : ℝ) (hτ : τ ≤ 0) :
60     ¬ ∃ ε : E → ℝ, (∀ e, 0 < ε e) ∧ (∑ e, s e * ε e) = τ := by
61   rintro ⟨ε, hε, hbudget⟩
62   have h := positive_allocation_budget s ε hs hε
63   linarith
64 
65 /-- One positive-sensitivity edge at budget zero is already infeasible. -/
66 theorem one_edge_zero_budget_infeasible :
67     ¬ ∃ ε : Fin 1 → ℝ, (∀ e, 0 < ε e) ∧ (∑ e, (1 : ℝ) * ε e) = 0 := by
68   exact no_positive_allocation_nonpositive_budget (fun _ => 1) (by intro e; norm_num) 0 le_rfl
69 
70 end KomorebiPaperVIII
71 
72 #print axioms KomorebiPaperVIII.cancellation_square_zero
73 #print axioms KomorebiPaperVIII.cancellation_block_nonzero
74 #print axioms KomorebiPaperVIII.paths_can_cancel
75 #print axioms KomorebiPaperVIII.positive_allocation_budget
76 #print axioms KomorebiPaperVIII.no_positive_allocation_nonpositive_budget
77 #print axioms KomorebiPaperVIII.one_edge_zero_budget_infeasible

Back to source controls