PositivePackets.lean

1 import KomorebiLSM.FiniteInstrument
2 import Mathlib.LinearAlgebra.Matrix.Diagonal
3 
4 /-! P30: positivity is an additional packet contract, not a consequence of
5 reconstruction. Complete positive idempotents on an orthant are coordinate selectors. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.PositivePackets
8 open scoped BigOperators
9 
10 section Mixtures
11 variable {X J : Type*} [AddCommGroup X] [Module ℝ X] [Fintype J]
12 
13 /-- Nonzero cone points have strictly positive mass. -/
14 def StrictMass (C : Set X) (l : X →ₗ[ℝ] ℝ) : Prop :=
15   ∀ x ∈ C, x ≠ 0 → 0 < l x
16 
17 theorem mass_nonnegative (C : Set X) (l : X →ₗ[ℝ] ℝ) (hl : StrictMass C l)
18     (x : X) (hx : x ∈ C) : 0 ≤ l x := by
19   by_cases h : x = 0
20   · simp [h]
21   · exact (hl x hx h).le
22 
23 theorem mass_zero_iff (C : Set X) (l : X →ₗ[ℝ] ℝ) (hl : StrictMass C l)
24     (x : X) (hx : x ∈ C) : l x = 0 ↔ x = 0 := by
25   constructor
26   · intro hm
27     by_contra h
28     exact (ne_of_gt (hl x hx h)) hm
29   · intro h; simp [h]
30 
31 theorem packet_weights_sum (l : X →ₗ[ℝ] ℝ) (P : J → X →ₗ[ℝ] X)
32     (hP : ∑ j, P j = LinearMap.id) (z : X) (hz : l z = 1) :
33     ∑ j, l (P j z) = 1 := by
34   rw [← map_sum]
35   have he : ∑ j, P j z = z := by
36     simpa only [LinearMap.sum_apply,LinearMap.id_apply] using
37       congrArg (fun F : X →ₗ[ℝ] X => F z) hP
38   rw [he,hz]
39 
40 /-- An individual normalized packet belongs to the cone only by positivity. -/
41 theorem normalized_packet (C : Set X)
42     (hscale : ∀ (c : ℝ), 0 ≤ c → ∀ x ∈ C, c • x ∈ C)
43     (l : X →ₗ[ℝ] ℝ) (P : X →ₗ[ℝ] X) (hp : ∀ x ∈ C, P x ∈ C)
44     (z : X) (hz : z ∈ C) (hw : 0 < l (P z)) :
45     (l (P z))⁻¹ • P z ∈ C ∧ l ((l (P z))⁻¹ • P z) = 1 := by
46   refine ⟨hscale _ (inv_nonneg.mpr hw.le) _ (hp z hz), ?_⟩
47   simp [ne_of_gt hw]
48 
49 /-- The positive-weight mixture reconstructs z; zero-weight terms vanish. -/
50 theorem positive_packet_mixture [DecidableEq J] (C : Set X)
51     (l : X →ₗ[ℝ] ℝ) (hl : StrictMass C l)
52     (P : J → X →ₗ[ℝ] X) (hp : ∀ j x, x ∈ C → P j x ∈ C)
53     (hP : ∑ j, P j = LinearMap.id) (z : X) (hz : z ∈ C) :
54     ∑ j ∈ Finset.univ.filter (fun j => 0 < l (P j z)),
55       l (P j z) • ((l (P j z))⁻¹ • P j z) = z := by
56   classical
57   rw [Finset.sum_filter]
58   have he : ∑ j, P j z = z := by
59     simpa only [LinearMap.sum_apply,LinearMap.id_apply] using
60       congrArg (fun F : X →ₗ[ℝ] X => F z) hP
61   apply Eq.trans (b := ∑ j, P j z) ?_ he
62   apply Finset.sum_congr rfl
63   intro j _
64   by_cases hw : 0 < l (P j z)
65   · simp [hw,smul_smul,ne_of_gt hw]
66   · have hm : l (P j z) = 0 := le_antisymm (le_of_not_gt hw) (mass_nonnegative C l hl _ (hp j z hz))
67     have hv := (mass_zero_iff C l hl _ (hp j z hz)).mp hm
68     simp [hv]
69 
70 end Mixtures
71 
72 section OrthantMass
73 variable {I : Type*} [Fintype I]
74 
75 /-- Ordinary probability mass is strict on nonzero nonnegative finite vectors. -/
76 theorem orthant_strict_mass :
77     StrictMass {x : I → ℝ | ∀ i, 0 ≤ x i} FiniteInstruments.mass := by
78   intro x hx hne
79   have hn := FiniteInstruments.mass_nonneg x hx
80   apply lt_of_le_of_ne hn
81   intro hz
82   apply hne
83   funext i
84   have he : ∑ i, x i = 0 := by simpa only [FiniteInstruments.mass_apply] using hz.symm
85   exact (Finset.sum_eq_zero_iff_of_nonneg (fun i _ => hx i)).mp he i (Finset.mem_univ i)
86 
87 end OrthantMass
88 
89 section Orthant
90 variable {I J : Type*} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J]
91 
92 /-- Positivity for all nonnegative inputs equals entrywise matrix positivity. -/
93 theorem orthant_preserving_iff (M : Matrix I I ℝ) :
94     (∀ x : I → ℝ, (∀ i, 0 ≤ x i) → ∀ i, 0 ≤ M.mulVec x i) ↔
95       ∀ i j, 0 ≤ M i j := by
96   constructor
97   · intro h i j
98     have hp : ∀ k, 0 ≤ FiniteBayes.pointMass j k := by
99       intro k
100       simp only [FiniteBayes.pointMass]
101       positivity
102     have hm := h (FiniteBayes.pointMass j) hp i
103     simpa [Matrix.mulVec,dotProduct,FiniteBayes.pointMass] using hm
104   · intro h x hx i
105     exact Finset.sum_nonneg (fun j _ => mul_nonneg (h i j) (hx j))
106 
107 omit [Fintype I] [DecidableEq J] in
108 /-- Nonnegative matrices summing to identity have no off-diagonal entries. -/
109 theorem off_diagonal_zero (P : J → Matrix I I ℝ)
110     (hp : ∀ k i j, 0 ≤ P k i j) (hP : ∑ k, P k = 1)
111     (k : J) (i j : I) (hij : i ≠ j) : P k i j = 0 := by
112   have hs : ∑ k, P k i j = 0 := by
113     have he := congrArg (fun M : Matrix I I ℝ => M i j) hP
114     simpa only [Matrix.sum_apply,Matrix.one_apply_ne hij] using he
115   have he : P k i j ≤ ∑ k, P k i j :=
116     Finset.single_le_sum (fun k _ => hp k i j) (Finset.mem_univ k)
117   rw [hs] at he
118   exact le_antisymm he (hp k i j)
119 
120 omit [Fintype I] [DecidableEq J] in
121 theorem matrix_eq_diagonal (P : J → Matrix I I ℝ)
122     (hp : ∀ k i j, 0 ≤ P k i j) (hP : ∑ k, P k = 1) (k : J) :
123     P k = Matrix.diagonal (fun i => P k i i) := by
124   ext i j
125   by_cases h : i=j
126   · subst j; simp
127   · rw [Matrix.diagonal_apply_ne _ h,off_diagonal_zero P hp hP k i j h]
128 
129 omit [DecidableEq J] in
130 /-- Idempotence restricts each diagonal entry to zero or one. -/
131 theorem diagonal_boolean (P : J → Matrix I I ℝ)
132     (hp : ∀ k i j, 0 ≤ P k i j) (hP : ∑ k, P k = 1)
133     (hid : ∀ k, P k * P k = P k) (k : J) (i : I) :
134     P k i i = 0 ∨ P k i i = 1 := by
135   have he := hid k
136   rw [matrix_eq_diagonal P hp hP k,Matrix.diagonal_mul_diagonal] at he
137   have hv := congrArg (fun M : Matrix I I ℝ => M i i) he
138   simp only [Matrix.diagonal_apply_eq] at hv
139   have hz : P k i i * (P k i i - 1) = 0 := by nlinarith
140   rcases mul_eq_zero.mp hz with h|h
141   · exact Or.inl h
142   · exact Or.inr (sub_eq_zero.mp h)
143 
144 /-- Completeness makes the coordinate selections disjoint and exhaustive. -/
145 theorem unique_selected_packet (P : J → Matrix I I ℝ)
146     (hp : ∀ k i j, 0 ≤ P k i j) (hP : ∑ k, P k = 1)
147     (hid : ∀ k, P k * P k = P k) (i : I) : ∃! k, P k i i = 1 := by
148   have hs : ∑ k, P k i i = 1 := by
149     have he := congrArg (fun M : Matrix I I ℝ => M i i) hP
150     simpa only [Matrix.sum_apply,Matrix.one_apply_eq] using he
151   have hex : ∃ k, P k i i = 1 := by
152     by_contra hn
153     push Not at hn
154     have hz : ∀ k, P k i i = 0 := fun k =>
155       (diagonal_boolean P hp hP hid k i).resolve_right (hn k)
156     simp only [hz,Finset.sum_const_zero] at hs
157     norm_num at hs
158   obtain ⟨k,hk⟩ := hex
159   refine ⟨k,hk, ?_⟩
160   intro j hj
161   by_contra hne
162   have herase : ∑ q ∈ Finset.univ.erase k, P q i i = 0 := by
163     have he := Finset.sum_erase_add Finset.univ (fun q => P q i i) (Finset.mem_univ k)
164     rw [hs,hk] at he
165     linarith
166   have hjmem : j ∈ Finset.univ.erase k := Finset.mem_erase.mpr ⟨hne,Finset.mem_univ j⟩
167   have hjle : P j i i ≤ ∑ q ∈ Finset.univ.erase k, P q i i :=
168     Finset.single_le_sum (fun q _ => hp q i i) hjmem
169   rw [hj,herase] at hjle
170   norm_num at hjle
171 
172 /-- P30's orthant boundary: positive complete projectors are only selections. -/
173 theorem positive_idempotents_are_coordinate_selections (P : J → Matrix I I ℝ)
174     (hp : ∀ k, ∀ x : I → ℝ, (∀ i, 0 ≤ x i) → ∀ i, 0 ≤ (P k).mulVec x i)
175     (hP : ∑ k, P k = 1) (hid : ∀ k, P k * P k = P k) :
176     (∀ k, P k = Matrix.diagonal (fun i => P k i i)) ∧
177     (∀ k i, P k i i = 0 ∨ P k i i = 1) ∧
178     (∀ i, ∃! k, P k i i = 1) := by
179   have hnonneg := fun k => (orthant_preserving_iff (P k)).mp (hp k)
180   exact ⟨matrix_eq_diagonal P hnonneg hP,
181     diagonal_boolean P hnonneg hP hid,unique_selected_packet P hnonneg hP hid⟩
182 
183 end Orthant
184 end Komorebi.LSM.PositivePackets

Back to source controls