CoordinatePackets.lean

1 import MachineTheory.PositivePackets
2 import Mathlib.Algebra.Order.BigOperators.Group.Finset
3 import Mathlib.Tactic.Linarith
4 
5 /-!
6 # Complete positive idempotents on the coordinate cone
7 
8 Core 2.5, coordinate sector. Positivity and completeness force diagonal form.
9 Idempotence then forces a partition of the coordinates. Orthogonality and
10 unique ownership of each coordinate are conclusions, not hypotheses.
11 -/
12 namespace Komorebi.MachineTheory.PositivePackets.Coordinate
13 
14 noncomputable section
15 
16 open scoped BigOperators
17 attribute [local instance] Classical.propDecidable
18 
19 universe uN uI
20 variable {N : Type uN} {I : Type uI}
21 
22 /-- The actual nonnegative coordinate cone. -/
23 def cone (N : Type uN) : ConvexCone ℝ (N → ℝ) where
24   carrier := {v | ∀ j, 0 ≤ v j}
25   smul_mem' := by
26     intro c hc v hv j
27     exact mul_nonneg (le_of_lt hc) (hv j)
28   add_mem' := by
29     intro v hv w hw j
30     exact add_nonneg (hv j) (hw j)
31 
32 @[simp] theorem mem_cone (v : N → ℝ) : v ∈ cone N ↔ ∀ j, 0 ≤ v j := Iff.rfl
33 
34 /-- Coefficients of the given linear map, obtained on standard basis vectors. -/
35 def coefficient (P : (N → ℝ) →ₗ[ℝ] (N → ℝ)) (r c : N) : ℝ := by
36   classical
37   exact P (Pi.single c 1) r
38 
39 variable [Fintype N]
40 
41 /-- The coordinate basis expands every input vector exactly. -/
42 theorem basis_expansion (v : N → ℝ) :
43     (∑ j, v j • Pi.single j (1 : ℝ)) = v := by
44   classical
45   ext r
46   simp [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, Pi.single_apply]
47 
48 /-- The coefficients represent the actual linear operation on every vector. -/
49 theorem coordinate_action (P : (N → ℝ) →ₗ[ℝ] (N → ℝ)) (v : N → ℝ) (r : N) :
50     P v r = ∑ c, coefficient P r c * v c := by
51   classical
52   calc
53     P v r = P (∑ c, v c • Pi.single c (1 : ℝ)) r := by rw [basis_expansion]
54     _ = ∑ c, coefficient P r c * v c := by
55       simp [coefficient, map_sum, map_smul, Finset.sum_apply, mul_comm]
56 
57 /-- Cone preservation is equivalent to nonnegative entries of the actual matrix. -/
58 theorem preserves_iff_coefficients (P : (N → ℝ) →ₗ[ℝ] (N → ℝ)) :
59     Preserves (cone N) P ↔ ∀ r c, 0 ≤ coefficient P r c := by
60   classical
61   constructor
62   · intro hp r c
63     apply hp (Pi.single c 1)
64     intro j
65     by_cases h : j = c <;> simp [h]
66   · intro hc v hv r
67     rw [coordinate_action]
68     exact Finset.sum_nonneg (fun c _ => mul_nonneg (hc r c) (hv c))
69 
70 variable [Fintype I]
71 
72 omit [Fintype N] in
73 /-- Completeness sums every matrix entry to the corresponding identity entry. -/
74 theorem complete_coefficient_sum (P : I → (N → ℝ) →ₗ[ℝ] (N → ℝ))
75     (hc : Complete P) (r c : N) :
76     (∑ i, coefficient (P i) r c) = if r = c then 1 else 0 := by
77   classical
78   have h := congrArg (fun F : (N → ℝ) →ₗ[ℝ] (N → ℝ) => F (Pi.single c 1) r) hc
79   simpa [coefficient, LinearMap.sum_apply, Finset.sum_apply, Pi.single_apply, eq_comm] using h
80 
81 /-- Positivity prevents off-diagonal cancellation in a complete family. -/
82 theorem off_diagonal_zero (P : I → (N → ℝ) →ₗ[ℝ] (N → ℝ))
83     (hp : ∀ i, Preserves (cone N) (P i)) (hc : Complete P)
84     (i : I) {r c : N} (hrc : r ≠ c) : coefficient (P i) r c = 0 := by
85   classical
86   have hnon : ∀ k, 0 ≤ coefficient (P k) r c :=
87     fun k => (preserves_iff_coefficients (P k)).mp (hp k) r c
88   have hle := Finset.single_le_sum (fun k (_ : k ∈ (Finset.univ : Finset I)) => hnon k)
89     (Finset.mem_univ i)
90   rw [complete_coefficient_sum P hc r c, ite_eq_right hrc] at hle
91   exact le_antisymm hle (hnon i)
92 
93 /-- Complete positive maps act diagonally even before idempotence is assumed. -/
94 theorem diagonal_action (P : I → (N → ℝ) →ₗ[ℝ] (N → ℝ))
95     (hp : ∀ i, Preserves (cone N) (P i)) (hc : Complete P)
96     (i : I) (v : N → ℝ) (r : N) :
97     P i v r = coefficient (P i) r r * v r := by
98   classical
99   rw [coordinate_action]
100   apply Finset.sum_eq_single r
101   · intro c _ hcr
102     rw [off_diagonal_zero P hp hc i hcr.symm, zero_mul]
103   · simp
104 
105 /-- Idempotence makes each diagonal entry multiplicatively idempotent. -/
106 theorem diagonal_idempotent (P : I → (N → ℝ) →ₗ[ℝ] (N → ℝ))
107     (hp : ∀ i, Preserves (cone N) (P i)) (hc : Complete P)
108     (hi : ∀ i, (P i).comp (P i) = P i) (i : I) (r : N) :
109     coefficient (P i) r r * coefficient (P i) r r = coefficient (P i) r r := by
110   classical
111   have h := congrArg (fun F : (N → ℝ) →ₗ[ℝ] (N → ℝ) => F (Pi.single r 1) r) (hi i)
112   change P i (P i (Pi.single r 1)) r = P i (Pi.single r 1) r at h
113   rw [diagonal_action P hp hc] at h
114   exact h
115 
116 /-- Every diagonal entry of a complete positive idempotent is zero or one. -/
117 theorem diagonal_zero_or_one (P : I → (N → ℝ) →ₗ[ℝ] (N → ℝ))
118     (hp : ∀ i, Preserves (cone N) (P i)) (hc : Complete P)
119     (hi : ∀ i, (P i).comp (P i) = P i) (i : I) (r : N) :
120     coefficient (P i) r r = 0 ∨ coefficient (P i) r r = 1 := by
121   have h := diagonal_idempotent P hp hc hi i r
122   have hz : coefficient (P i) r r * (coefficient (P i) r r - 1) = 0 := by nlinarith
123   rcases mul_eq_zero.mp hz with h0 | h1
124   · exact Or.inl h0
125   · exact Or.inr (sub_eq_zero.mp h1)
126 
127 /-- Every coordinate is selected by exactly one operator. -/
128 theorem unique_owner (P : I → (N → ℝ) →ₗ[ℝ] (N → ℝ))
129     (hp : ∀ i, Preserves (cone N) (P i)) (hc : Complete P)
130     (hi : ∀ i, (P i).comp (P i) = P i) (r : N) :
131     ∃! i, coefficient (P i) r r = 1 := by
132   classical
133   have hsum : (∑ i, coefficient (P i) r r) = 1 := by
134     simpa using complete_coefficient_sum P hc r r
135   have hnon : ∀ i, 0 ≤ coefficient (P i) r r :=
136     fun i => (preserves_iff_coefficients (P i)).mp (hp i) r r
137   have hex : ∃ i, coefficient (P i) r r = 1 := by
138     by_contra hn
139     have hall : ∀ i, coefficient (P i) r r = 0 := by
140       intro i
141       exact (diagonal_zero_or_one P hp hc hi i r).resolve_right (fun h => hn ⟨i, h⟩)
142     simp [hall] at hsum
143   obtain ⟨i, hival⟩ := hex
144   refine ⟨i, hival, ?_⟩
145   intro k hk
146   by_contra hki
147   have hsplit := Finset.sum_erase_add Finset.univ
148     (fun j => coefficient (P j) r r) (Finset.mem_univ i)
149   have hzero : (∑ j ∈ Finset.univ.erase i, coefficient (P j) r r) = 0 := by
150     rw [hsum, hival] at hsplit
151     linarith
152   have hle := Finset.single_le_sum (fun j (_ : j ∈ Finset.univ.erase i) => hnon j)
153     (Finset.mem_erase.mpr ⟨hki, Finset.mem_univ k⟩)
154   rw [hzero, hk] at hle
155   exact (not_le_of_gt zero_lt_one) hle
156 
157 /-- A partition of coordinates determines its actual linear selector maps. -/
158 def selector (owner : N → I) (i : I) : (N → ℝ) →ₗ[ℝ] (N → ℝ) := by
159   classical
160   exact {
161     toFun := fun v r => if owner r = i then v r else 0
162     map_add' := by
163       intro v w
164       funext r
165       by_cases h : owner r = i <;> simp [h]
166     map_smul' := by
167       intro c v
168       funext r
169       by_cases h : owner r = i <;> simp [h] }
170 
171 omit [Fintype N] [Fintype I] in
172 @[simp] theorem selector_apply (owner : N → I) (i : I) (v : N → ℝ) (r : N) :
173     selector owner i v r = if owner r = i then v r else 0 := by
174   classical
175   rfl
176 
177 omit [Fintype N] [Fintype I] in
178 /-- Every selector preserves the coordinate cone. -/
179 theorem selector_preserves (owner : N → I) (i : I) :
180     Preserves (cone N) (selector owner i) := by
181   classical
182   intro v hv r
183   simp only [selector_apply]
184   split_ifs
185   · exact hv r
186   · exact le_rfl
187 
188 omit [Fintype N] in
189 /-- A selector family is complete, including the zero-dimensional case. -/
190 theorem selector_complete (owner : N → I) : Complete (selector owner) := by
191   classical
192   apply LinearMap.ext
193   intro v
194   funext r
195   simp [LinearMap.sum_apply, Finset.sum_apply, selector_apply]
196 
197 omit [Fintype N] [Fintype I] in
198 /-- Every selector is idempotent. -/
199 theorem selector_idempotent (owner : N → I) (i : I) :
200     (selector owner i).comp (selector owner i) = selector owner i := by
201   classical
202   apply LinearMap.ext
203   intro v
204   funext r
205   simp only [LinearMap.comp_apply, selector_apply]
206   split_ifs <;> rfl
207 
208 omit [Fintype N] [Fintype I] in
209 /-- Distinct selectors have zero composition. -/
210 theorem selector_disjoint (owner : N → I) {i k : I} (hik : i ≠ k) :
211     (selector owner i).comp (selector owner k) = 0 := by
212   classical
213   apply LinearMap.ext
214   intro v
215   funext r
216   simp only [LinearMap.comp_apply, selector_apply, LinearMap.zero_apply, Pi.zero_apply]
217   split_ifs with hri hrk
218   · exact False.elim (hik (hri.symm.trans hrk))
219   · rfl
220   · rfl
221 
222 /-- Construction of the unique coordinate assignment from the original maps. -/
223 theorem exists_selectors (P : I → (N → ℝ) →ₗ[ℝ] (N → ℝ))
224     (hp : ∀ i, Preserves (cone N) (P i)) (hc : Complete P)
225     (hi : ∀ i, (P i).comp (P i) = P i) :
226     ∃ owner : N → I, ∀ i, P i = selector owner i := by
227   classical
228   choose owner howner hunique using unique_owner P hp hc hi
229   refine ⟨owner, ?_⟩
230   intro i
231   apply LinearMap.ext
232   intro v
233   funext r
234   rw [diagonal_action P hp hc, selector_apply]
235   by_cases hri : owner r = i
236   · rw [ite_eq_left hri, ← hri, howner r, one_mul]
237   · rw [ite_eq_right hri]
238     have hzero : coefficient (P i) r r = 0 :=
239       (diagonal_zero_or_one P hp hc hi i r).resolve_right
240         (fun h => hri (hunique r i h).symm)
241     rw [hzero, zero_mul]
242 
243 /-- The selector representation also implies all the original hypotheses. -/
244 theorem classification_iff (P : I → (N → ℝ) →ₗ[ℝ] (N → ℝ)) :
245     ((∀ i, Preserves (cone N) (P i)) ∧ Complete P ∧ ∀ i, (P i).comp (P i) = P i) ↔
246       ∃ owner : N → I, ∀ i, P i = selector owner i := by
247   constructor
248   · rintro ⟨hp, hc, hi⟩
249     exact exists_selectors P hp hc hi
250   · rintro ⟨owner, h⟩
251     have heq : P = selector owner := funext h
252     subst P
253     exact ⟨selector_preserves owner, selector_complete owner, selector_idempotent owner⟩
254 
255 /-- Source-facing classification, with disjointness derived rather than assumed. -/
256 theorem source_core25_coordinate (P : I → (N → ℝ) →ₗ[ℝ] (N → ℝ))
257     (hp : ∀ i, Preserves (cone N) (P i)) (hc : Complete P)
258     (hi : ∀ i, (P i).comp (P i) = P i) :
259     (∃ owner : N → I, ∀ i, P i = selector owner i) ∧
260     (∀ r, ∃! i, coefficient (P i) r r = 1) ∧
261     (∀ i k, i ≠ k → (P i).comp (P k) = 0) := by
262   obtain ⟨owner, ho⟩ := exists_selectors P hp hc hi
263   refine ⟨⟨owner, ho⟩, unique_owner P hp hc hi, ?_⟩
264   intro i k hik
265   rw [ho i, ho k]
266   exact selector_disjoint owner hik
267 
268 end
269 end Komorebi.MachineTheory.PositivePackets.Coordinate

Back to source controls