PositiveLift.lean

1 import KomorebiLSM.PositivePackets
2 import KomorebiLSM.TestCones
3 
4 /-! P39: nonnegative coefficient witnesses are constructed from invariance of
5 an actual finitely generated cone. The synthesis map need not be injective. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.PositiveLift
8 open scoped BigOperators
9 open FiniteInstruments FiniteBayes
10 variable {E J : Type*} [AddCommGroup E] [Module ℝ E] [Fintype J] [DecidableEq J]
11 
12 noncomputable def hull (V : (J → ℝ) →ₗ[ℝ] E) : Set E :=
13   {x | ∃ a : J → ℝ, (∀ j, 0 ≤ a j) ∧ V a = x}
14 
15 noncomputable def generator (V : (J → ℝ) →ₗ[ℝ] E) (j : J) : E := V (pointMass j)
16 
17 noncomputable def normalizedHull (V : (J → ℝ) →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ) : Set E :=
18   {x | x ∈ hull V ∧ l x = 1}
19 
20 omit [DecidableEq J] in
21 theorem normalized_mass (V : (J → ℝ) →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
22     (hn : l.comp V = mass) (a : J → ℝ) : l (V a) = ∑ j, a j := by
23   simpa only [LinearMap.comp_apply,mass_apply] using
24     congrArg (fun F : (J → ℝ) →ₗ[ℝ] ℝ => F a) hn
25 
26 theorem mass_generator (V : (J → ℝ) →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
27     (hn : l.comp V = mass) (j : J) : l (generator V j) = 1 := by
28   simpa only [generator,← mass_apply,mass_pointMass] using normalized_mass V l hn (pointMass j)
29 
30 theorem generator_mem (V : (J → ℝ) →ₗ[ℝ] E) (j : J) : generator V j ∈ hull V :=
31   ⟨pointMass j,(point_prior j).1,rfl⟩
32 
33 omit [Fintype J] [DecidableEq J] in
34 theorem hull_zero (V : (J → ℝ) →ₗ[ℝ] E) : (0 : E) ∈ hull V :=
35   ⟨0,fun _ => le_rfl,map_zero V⟩
36 
37 omit [Fintype J] [DecidableEq J] in
38 theorem hull_add (V : (J → ℝ) →ₗ[ℝ] E) {x y : E} (hx : x ∈ hull V) (hy : y ∈ hull V) :
39     x+y ∈ hull V := by
40   obtain ⟨a,ha,rfl⟩ := hx
41   obtain ⟨b,hb,rfl⟩ := hy
42   exact ⟨a+b,fun j => add_nonneg (ha j) (hb j),map_add V a b⟩
43 
44 omit [Fintype J] [DecidableEq J] in
45 theorem hull_smul (V : (J → ℝ) →ₗ[ℝ] E) {c : ℝ} (hc : 0 ≤ c)
46     {x : E} (hx : x ∈ hull V) : c • x ∈ hull V := by
47   obtain ⟨a,ha,rfl⟩ := hx
48   exact ⟨c • a,fun j => mul_nonneg hc (ha j),map_smul V c a⟩
49 
50 omit [Fintype J] [DecidableEq J] in
51 theorem hull_convex (V : (J → ℝ) →ₗ[ℝ] E) : Convex ℝ (hull V) := by
52   intro x hx y hy a b ha hb _
53   exact hull_add V (hull_smul V ha hx) (hull_smul V hb hy)
54 
55 omit [DecidableEq J] in
56 theorem hull_mass_nonneg (V : (J → ℝ) →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
57     (hn : l.comp V = mass) {x : E} (hx : x ∈ hull V) : 0 ≤ l x := by
58   obtain ⟨a,ha,rfl⟩ := hx
59   rw [normalized_mass V l hn]
60   exact Finset.sum_nonneg (fun j _ => ha j)
61 
62 omit [DecidableEq J] in
63 theorem hull_mass_zero (V : (J → ℝ) →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
64     (hn : l.comp V = mass) {x : E} (hx : x ∈ hull V) (hm : l x = 0) : x = 0 := by
65   obtain ⟨a,ha,rfl⟩ := hx
66   rw [normalized_mass V l hn] at hm
67   have he : a = 0 := by
68     funext j
69     exact (Finset.sum_eq_zero_iff_of_nonneg (fun j _ => ha j)).mp hm j (Finset.mem_univ j)
70   simp [he]
71 
72 omit [DecidableEq J] in
73 theorem hull_strict_mass (V : (J → ℝ) →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
74     (hn : l.comp V = mass) : PositivePackets.StrictMass (hull V) l := by
75   intro x hx hne
76   have hnonneg := hull_mass_nonneg V l hn hx
77   have hmass : l x ≠ 0 := fun hm => hne (hull_mass_zero V l hn hx hm)
78   exact lt_of_le_of_ne hnonneg (Ne.symm hmass)
79 
80 omit [DecidableEq J] in
81 theorem hull_pointed (V : (J → ℝ) →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
82     (hn : l.comp V = mass) {x : E} (hx : x ∈ hull V) (hmx : -x ∈ hull V) : x = 0 := by
83   apply hull_mass_zero V l hn hx
84   have h₁ := hull_mass_nonneg V l hn hx
85   have h₂ := hull_mass_nonneg V l hn hmx
86   rw [map_neg] at h₂
87   exact le_antisymm (neg_nonneg.mp h₂) h₁
88 
89 theorem synthesis_sum (V : (J → ℝ) →ₗ[ℝ] E) (a : J → ℝ) :
90     V a = ∑ j, a j • generator V j := by
91   conv_lhs => rw [vector_eq_sum_pointMass a]
92   simp only [map_sum,map_smul,generator]
93 
94 theorem hull_spans (V : (J → ℝ) →ₗ[ℝ] E) (hs : Function.Surjective V) :
95     Submodule.span ℝ (hull V) = ⊤ := by
96   apply top_unique
97   intro x _
98   obtain ⟨a,rfl⟩ := hs x
99   rw [synthesis_sum]
100   exact Submodule.sum_mem _ (fun j _ => Submodule.smul_mem _ _
101     (Submodule.subset_span (generator_mem V j)))
102 
103 omit [DecidableEq J] in
104 theorem normalizedHull_eq_prior_image (V : (J → ℝ) →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
105     (hn : l.comp V = mass) : normalizedHull V l = V '' {a | IsPrior a} := by
106   ext x
107   constructor
108   · rintro ⟨⟨a,ha,rfl⟩,hm⟩
109     exact ⟨a,⟨ha,by simpa only [normalized_mass V l hn] using hm⟩,rfl⟩
110   · rintro ⟨a,ha,rfl⟩
111     exact ⟨⟨a,ha.1,rfl⟩,by simpa only [normalized_mass V l hn] using ha.2⟩
112 
113 /-- Images of the finitely many generators suffice for invariance of the whole cone. -/
114 theorem invariant_iff_generators (V : (J → ℝ) →ₗ[ℝ] E) (B : E →ₗ[ℝ] E) :
115     (∀ x ∈ hull V, B x ∈ hull V) ↔ ∀ j, B (generator V j) ∈ hull V := by
116   constructor
117   · intro h j; exact h _ (generator_mem V j)
118   · intro h x hx
119     obtain ⟨a,ha,rfl⟩ := hx
120     rw [synthesis_sum,map_sum]
121     have hsum : ∀ t : Finset J, (∑ j ∈ t, B (a j • generator V j)) ∈ hull V := by
122       intro t
123       induction t using Finset.induction_on with
124       | empty => simpa using hull_zero V
125       | @insert j t hj ih =>
126         rw [Finset.sum_insert hj]
127         apply hull_add V _ ih
128         rw [map_smul]
129         exact hull_smul V (ha j) (h j)
130     simpa using hsum Finset.univ
131 
132 /-- The nonnegative matrix is constructed column by column, not assumed. -/
133 theorem positive_lift_iff (V : (J → ℝ) →ₗ[ℝ] E) (B : E →ₗ[ℝ] E) :
134     (∀ x ∈ hull V, B x ∈ hull V) ↔
135       ∃ M : Matrix J J ℝ, (∀ i j, 0 ≤ M i j) ∧ B.comp V = V.comp M.mulVecLin := by
136   classical
137   constructor
138   · intro hi
139     have hg := (invariant_iff_generators V B).mp hi
140     choose a ha he using hg
141     let M : Matrix J J ℝ := fun i j => a j i
142     refine ⟨M,fun i j => ha j i, ?_⟩
143     apply LinearMap.ext
144     intro x
145     rw [vector_eq_sum_pointMass x]
146     simp only [map_sum,map_smul]
147     apply Finset.sum_congr rfl
148     intro j _
149     congr 1
150     have hm : M.mulVecLin (pointMass j) = a j := by
151       funext i
152       change (∑ k, a k i * pointMass j k) = a j i
153       simp [pointMass]
154     simpa only [LinearMap.comp_apply,hm,generator] using (he j).symm
155   · rintro ⟨M,hn,he⟩ x ⟨a,ha,rfl⟩
156     refine ⟨M.mulVec a, (PositivePackets.orthant_preserving_iff M).mpr hn a ha, ?_⟩
157     exact (congrArg (fun F : (J → ℝ) →ₗ[ℝ] E => F a) he).symm
158 
159 section Instruments
160 variable {A O : Type*} [Fintype O]
161 variable (B : A × O → E →ₗ[ℝ] E) (V : (J → ℝ) →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
162 variable (hn : l.comp V = mass) (hm : ∀ a x, ∑ o, l (B (a,o) x) = l x)
163 variable (M : A × O → Matrix J J ℝ)
164 variable (he : ∀ s, (B s).comp V = V.comp (M s).mulVecLin)
165 include hn hm he
166 
167 /-- Mass normalization is inherited by every nonnegative lift, even a redundant one. -/
168 theorem lifted_mass (a : A) (j : J) : ∑ o, ∑ i, M (a,o) i j = 1 := by
169   have hc : ∀ o, l (B (a,o) (generator V j)) = ∑ i, M (a,o) i j := by
170     intro o
171     have he' := congrArg (fun F : (J → ℝ) →ₗ[ℝ] E => F (pointMass j)) (he (a,o))
172     have hp : (M (a,o)).mulVecLin (pointMass j) = fun i => M (a,o) i j := by
173       funext i
174       change (∑ k, M (a,o) i k * pointMass j k) = M (a,o) i j
175       simp [pointMass]
176     change B (a,o) (generator V j) = V ((M (a,o)).mulVecLin (pointMass j)) at he'
177     rw [he',hp,normalized_mass V l hn]
178   calc
179     ∑ o, ∑ i, M (a,o) i j = ∑ o, l (B (a,o) (generator V j)) :=
180       Finset.sum_congr rfl (fun o _ => (hc o).symm)
181     _ = l (generator V j) := hm a _
182     _ = 1 := mass_generator V l hn j
183 
184 noncomputable def liftedInstrument (hp : ∀ s i j, 0 ≤ M s i j) : Instrument J A O where
185   matrix a o := M (a,o)
186   nonneg a o i j := hp (a,o) i j
187   mass_one := lifted_mass B V l hn hm M he
188 
189 omit hn hm [DecidableEq J] [Fintype O] in
190 theorem lifted_word (w : List (A × O)) (a : J → ℝ) :
191     wordAction B w (V a) = V (wordAction (fun s => (M s).mulVecLin) w a) := by
192   have hw := word_intertwining (fun s => (M s).mulVecLin) B V he w
193   exact congrArg (fun F : (J → ℝ) →ₗ[ℝ] E => F a) hw
194 
195 omit hm [DecidableEq J] [Fintype O] in
196 theorem lifted_word_probability (w : List (A × O)) (a : J → ℝ) :
197     l (wordAction B w (V a)) = mass (wordAction (fun s => (M s).mulVecLin) w a) := by
198   rw [lifted_word B V M he]
199   exact congrArg (fun F : (J → ℝ) →ₗ[ℝ] ℝ => F _) hn
200 
201 /-- All word probabilities are those of the constructed nonnegative instrument. -/
202 theorem finite_positive_lift_certificate (hp : ∀ s i j, 0 ≤ M s i j)
203     (a₀ : J → ℝ) (ha₀ : IsPrior a₀) :
204     (∀ a j, ∑ o, ∑ i, M (a,o) i j = 1) ∧
205     (∀ w, l (wordAction B w (V a₀)) =
206       mass (wordAction (liftedInstrument B V l hn hm M he hp).branch w a₀)) ∧
207     (∀ w, 0 ≤ l (wordAction B w (V a₀)) ∧ l (wordAction B w (V a₀)) ≤ 1) := by
208   refine ⟨lifted_mass B V l hn hm M he,?_,?_⟩
209   · intro w; exact lifted_word_probability B V l hn M he w a₀
210   · intro w
211     rw [lifted_word_probability B V l hn M he]
212     exact (liftedInstrument B V l hn hm M he hp).word_probability w a₀ ha₀
213 
214 end Instruments
215 end Komorebi.LSM.PositiveLift

Back to source controls