GrammarAccounting.lean

1 import Mathlib.Topology.Algebra.InfiniteSum.Real
2 import Mathlib.Tactic
3 
4 
5 set_option autoImplicit false
6 
7 /-!
8 # Exact accounting for an enumerated grammar
9 
10 The weight `w g` is the whole-record unnormalized evidence `π(g) L_g(D)`.
11 Infinite sums are required to be summable; the active set is finite.
12 -/
13 namespace Komorebi.LSM.GrammarAccounting
14 
15 noncomputable section
16 
17 open scoped BigOperators
18 
19 variable {G : Type*} [DecidableEq G]
20 
21 def evidence (w : G → ℝ) : ℝ := ∑' g, w g
22 
23 def activeEvidence (A : Finset G) (w : G → ℝ) : ℝ := ∑ g ∈ A, w g
24 
25 def posterior (w : G → ℝ) (g : G) : ℝ := w g / evidence w
26 
27 def activePosterior (A : Finset G) (w : G → ℝ) (g : G) : ℝ :=
28   if g ∈ A then w g / activeEvidence A w else 0
29 
30 def retainedPosterior (A : Finset G) (w : G → ℝ) (g : G) : ℝ :=
31   if g ∈ A then posterior w g else 0
32 
33 def totalVariation (p q : G → ℝ) : ℝ := (1 / 2 : ℝ) * ∑' g, |p g - q g|
34 
35 theorem finite_ite_sum (A : Finset G) (f : G → ℝ) :
36     (∑' g, if g ∈ A then f g else 0) = ∑ g ∈ A, f g := by
37   rw [tsum_eq_sum (s := A) (by intro g hg; simp [hg])]
38   exact Finset.sum_congr rfl (fun g hg => ite_eq_left hg)
39 
40 theorem finite_ite_summable (A : Finset G) (f : G → ℝ) :
41     Summable (fun g => if g ∈ A then f g else 0) := by
42   exact summable_of_ne_finset_zero (s := A) (by intro g hg; simp [hg])
43 
44 omit [DecidableEq G] in
45 theorem activeEvidence_le (A : Finset G) (w : G → ℝ)
46     (hw : ∀ g, 0 ≤ w g) (hs : Summable w) : activeEvidence A w ≤ evidence w := by
47   exact hs.sum_le_tsum A (fun g _ => hw g)
48 
49 omit [DecidableEq G] in
50 omit [DecidableEq G] in
51 theorem posterior_summable (w : G → ℝ) (hs : Summable w) : Summable (posterior w) :=
52   hs.div_const _
53 
54 omit [DecidableEq G] in
55 theorem posterior_sum (w : G → ℝ) (hZ : 0 < evidence w) :
56     (∑' g, posterior w g) = 1 := by
57   simp only [posterior, tsum_div_const]
58   exact div_self (ne_of_gt hZ)
59 
60 theorem activePosterior_sum (A : Finset G) (w : G → ℝ)
61     (hA : 0 < activeEvidence A w) : (∑' g, activePosterior A w g) = 1 := by
62   simp only [activePosterior]
63   rw [finite_ite_sum, ← Finset.sum_div]
64   exact div_self (ne_of_gt hA)
65 
66 theorem retainedPosterior_sum (A : Finset G) (w : G → ℝ) :
67     (∑' g, retainedPosterior A w g) = activeEvidence A w / evidence w := by
68   simp only [retainedPosterior]
69   rw [finite_ite_sum]
70   exact (Finset.sum_div A w (evidence w)).symm
71 
72 theorem abs_posterior_difference (A : Finset G) (w : G → ℝ)
73     (hw : ∀ g, 0 ≤ w g) (hs : Summable w)
74     (hA : 0 < activeEvidence A w) (g : G) :
75     |posterior w g - activePosterior A w g| =
76       posterior w g + activePosterior A w g - 2 * retainedPosterior A w g := by
77   have hle := activeEvidence_le A w hw hs
78   have hZ : 0 < evidence w := lt_of_lt_of_le hA hle
79   by_cases hg : g ∈ A
80   · simp only [activePosterior, retainedPosterior, ite_eq_left hg]
81     have hpq : posterior w g ≤ w g / activeEvidence A w :=
82       div_le_div_of_nonneg_left (hw g) hA hle
83     rw [abs_of_nonpos (sub_nonpos.mpr hpq)]
84     ring
85   · simp only [activePosterior, retainedPosterior, ite_eq_right hg, sub_zero, add_zero, mul_zero]
86     exact abs_of_nonneg (div_nonneg (hw g) (le_of_lt hZ))
87 
88 /-- The active posterior loses exactly the omitted posterior mass, even for an infinite grammar. -/
89 theorem exact_posterior_tv (A : Finset G) (w : G → ℝ)
90     (hw : ∀ g, 0 ≤ w g) (hs : Summable w) (hA : 0 < activeEvidence A w) :
91     totalVariation (posterior w) (activePosterior A w) =
92       1 - activeEvidence A w / evidence w := by
93   have hp := posterior_summable w hs
94   have hq : Summable (activePosterior A w) := finite_ite_summable A _
95   have hr : Summable (retainedPosterior A w) := finite_ite_summable A _
96   have hZ : 0 < evidence w := lt_of_lt_of_le hA (activeEvidence_le A w hw hs)
97   unfold totalVariation
98   simp_rw [abs_posterior_difference A w hw hs hA]
99   rw [(hp.add hq).tsum_sub (hr.mul_left 2), hp.tsum_add hq, tsum_mul_left,
100     posterior_sum w hZ, activePosterior_sum A w hA, retainedPosterior_sum]
101   ring
102 
103 /-- An event in a predictive kernel has probability between zero and one. -/
104 def predictiveEvent (p kernel : G → ℝ) : ℝ := ∑' g, p g * kernel g
105 
106 omit [DecidableEq G] in
107 theorem weighted_summable (p kernel : G → ℝ) (hp : ∀ g, 0 ≤ p g)
108     (hs : Summable p) (hk0 : ∀ g, 0 ≤ kernel g) (hk1 : ∀ g, kernel g ≤ 1) :
109     Summable (fun g => p g * kernel g) := by
110   exact Summable.of_nonneg_of_le (fun g => mul_nonneg (hp g) (hk0 g))
111     (fun g => by simpa using mul_le_mul_of_nonneg_left (hk1 g) (hp g)) hs
112 
113 omit [DecidableEq G] in
114 /-- A common probability kernel cannot increase total variation, event by event. -/
115 theorem predictive_event_contraction (p q kernel : G → ℝ)
116     (hp0 : ∀ g, 0 ≤ p g) (hq0 : ∀ g, 0 ≤ q g)
117     (hp : Summable p) (hq : Summable q)
118     (hpsum : ∑' g, p g = 1) (hqsum : ∑' g, q g = 1)
119     (hk0 : ∀ g, 0 ≤ kernel g) (hk1 : ∀ g, kernel g ≤ 1) :
120     |predictiveEvent p kernel - predictiveEvent q kernel| ≤ totalVariation p q := by
121   have hpk := weighted_summable p kernel hp0 hp hk0 hk1
122   have hqk := weighted_summable q kernel hq0 hq hk0 hk1
123   have hd := hp.sub hq
124   have habs : Summable (fun g => |p g - q g|) := by
125     apply Summable.of_nonneg_of_le (fun g => abs_nonneg (p g - q g)) _ (hp.add hq)
126     intro g
127     exact abs_le.mpr ⟨by linarith [hp0 g], by linarith [hq0 g]⟩
128   have hl : ∀ g, ((p g - q g) - |p g - q g|) / 2 ≤
129       p g * kernel g - q g * kernel g := by
130     intro g
131     by_cases h : 0 ≤ p g - q g
132     · rw [abs_of_nonneg h]
133       nlinarith [mul_nonneg h (hk0 g)]
134     · have hn := le_of_not_ge h
135       rw [abs_of_nonpos hn]
136       nlinarith [mul_nonpos_of_nonpos_of_nonneg hn (sub_nonneg.mpr (hk1 g))]
137   have hu : ∀ g, p g * kernel g - q g * kernel g ≤
138       ((p g - q g) + |p g - q g|) / 2 := by
139     intro g
140     by_cases h : 0 ≤ p g - q g
141     · rw [abs_of_nonneg h]
142       nlinarith [mul_nonneg h (sub_nonneg.mpr (hk1 g))]
143     · have hn := le_of_not_ge h
144       rw [abs_of_nonpos hn]
145       nlinarith [mul_nonpos_of_nonpos_of_nonneg hn (hk0 g)]
146   have hlow := ((hd.sub habs).div_const 2).tsum_le_tsum hl (hpk.sub hqk)
147   have hupp := (hpk.sub hqk).tsum_le_tsum hu ((hd.add habs).div_const 2)
148   rw [tsum_div_const, hd.tsum_sub habs, hp.tsum_sub hq,
149     hpsum, hqsum, hpk.tsum_sub hqk] at hlow
150   rw [tsum_div_const, hd.tsum_add habs, hp.tsum_sub hq,
151     hpsum, hqsum, hpk.tsum_sub hqk] at hupp
152   exact abs_le.mpr ⟨by dsimp [predictiveEvent, totalVariation]; linarith,
153     by dsimp [predictiveEvent, totalVariation]; linarith⟩
154 
155 /-- Any candidate predictive probability kernels retain the same omitted-mass bound. -/
156 theorem active_predictive_event_bound (A : Finset G) (w kernel : G → ℝ)
157     (hw : ∀ g, 0 ≤ w g) (hs : Summable w) (hA : 0 < activeEvidence A w)
158     (hk0 : ∀ g, 0 ≤ kernel g) (hk1 : ∀ g, kernel g ≤ 1) :
159     |predictiveEvent (posterior w) kernel - predictiveEvent (activePosterior A w) kernel| ≤
160       1 - activeEvidence A w / evidence w := by
161   have hZ : 0 < evidence w := lt_of_lt_of_le hA (activeEvidence_le A w hw hs)
162   rw [← exact_posterior_tv A w hw hs hA]
163   apply predictive_event_contraction
164   · exact fun g => div_nonneg (hw g) (le_of_lt hZ)
165   · intro g
166     simp only [activePosterior]
167     split_ifs
168     · exact div_nonneg (hw g) (le_of_lt hA)
169     · exact le_rfl
170   · exact posterior_summable w hs
171   · exact finite_ite_summable A _
172   · exact posterior_sum w hZ
173   · exact activePosterior_sum A w hA
174   · exact hk0
175   · exact hk1
176 
177 /-- The actual omitted unnormalized evidence. -/
178 def omittedEvidence (A : Finset G) (w : G → ℝ) : ℝ :=
179   ∑' g, if g ∈ A then 0 else w g
180 
181 theorem omittedEvidence_eq (A : Finset G) (w : G → ℝ) (hs : Summable w) :
182     omittedEvidence A w = evidence w - activeEvidence A w := by
183   have hr := finite_ite_summable A w
184   calc
185     omittedEvidence A w = ∑' g, (w g - if g ∈ A then w g else 0) := by
186       apply tsum_congr
187       intro g
188       by_cases hg : g ∈ A <;> simp [hg]
189     _ = (∑' g, w g) - ∑' g, if g ∈ A then w g else 0 := hs.tsum_sub hr
190     _ = evidence w - activeEvidence A w := by rw [finite_ite_sum]; rfl
191 
192 /-- A certified omitted-evidence bound yields the sharpened posterior tail bound. -/
193 theorem omitted_evidence_bound (A : Finset G) (w : G → ℝ) (bound : ℝ)
194     (hw : ∀ g, 0 ≤ w g) (hs : Summable w) (hA : 0 < activeEvidence A w)
195     (hb : omittedEvidence A w ≤ bound) :
196     1 - activeEvidence A w / evidence w ≤ bound / (activeEvidence A w + bound) := by
197   have hle := activeEvidence_le A w hw hs
198   have hZ : 0 < evidence w := lt_of_lt_of_le hA hle
199   rw [omittedEvidence_eq A w hs] at hb
200   have hbound : 0 ≤ bound := le_trans (sub_nonneg.mpr hle) hb
201   have hden : 0 < activeEvidence A w + bound := add_pos_of_pos_of_nonneg hA hbound
202   rw [show 1 - activeEvidence A w / evidence w =
203       (evidence w - activeEvidence A w) / evidence w by field_simp]
204   apply (div_le_div_iff₀ hZ hden).mpr
205   nlinarith
206 
207 omit [DecidableEq G] in
208 /-- An increasing exhaustive active-set sequence tends cofinally to all finite subsets. -/
209 theorem activeSets_cofinal (A : ℕ → Finset G) (hmono : Monotone A)
210     (hexhaust : ∀ g, ∃ n, g ∈ A n) :
211     Filter.Tendsto A Filter.atTop Filter.atTop := by
212   exact hmono.tendsto_atTop_finset hexhaust
213 
214 omit [DecidableEq G] in
215 /-- Exhaustion recovers the full normalizer; no finite-prefix rank assumption is used. -/
216 theorem active_evidence_tendsto (A : ℕ → Finset G) (w : G → ℝ) (hs : Summable w)
217     (hmono : Monotone A) (hexhaust : ∀ g, ∃ n, g ∈ A n) :
218     Filter.Tendsto (fun n => activeEvidence (A n) w) Filter.atTop (nhds (evidence w)) := by
219   exact hs.hasSum.comp (activeSets_cofinal A hmono hexhaust)
220 
221 omit [DecidableEq G] in
222 /-- The exact omitted posterior fraction tends to zero along every exhaustive sequence. -/
223 theorem posterior_tail_tendsto_zero (A : ℕ → Finset G) (w : G → ℝ)
224     (hs : Summable w) (hZ : 0 < evidence w)
225     (hmono : Monotone A) (hexhaust : ∀ g, ∃ n, g ∈ A n) :
226     Filter.Tendsto (fun n => 1 - activeEvidence (A n) w / evidence w)
227       Filter.atTop (nhds 0) := by
228   have ht := (active_evidence_tendsto A w hs hmono hexhaust).div_const (evidence w)
229   have ht' := (tendsto_const_nhds (x := (1 : ℝ)) (f := Filter.atTop)).sub ht
230   simpa only [div_self (ne_of_gt hZ), sub_self] using ht'
231 
232 omit [DecidableEq G] in
233 /-- Nonnegative whole-record evidence increases with the active set. -/
234 theorem active_evidence_monotone (A : ℕ → Finset G) (w : G → ℝ)
235     (hw : ∀ g, 0 ≤ w g) (hmono : Monotone A) :
236     Monotone (fun n => activeEvidence (A n) w) := by
237   intro n m hnm
238   exact Finset.sum_le_sum_of_subset_of_nonneg (hmono hnm) (fun g _ _ => hw g)
239 
240 omit [DecidableEq G] in
241 /-- Consequently the omitted posterior fraction decreases. -/
242 theorem posterior_tail_antitone (A : ℕ → Finset G) (w : G → ℝ)
243     (hw : ∀ g, 0 ≤ w g) (hZ : 0 < evidence w) (hmono : Monotone A) :
244     Antitone (fun n => 1 - activeEvidence (A n) w / evidence w) := by
245   intro n m hnm
246   have hle := (active_evidence_monotone A w hw hmono) hnm
247   have hdiv := div_le_div_of_nonneg_right hle (le_of_lt hZ)
248   linarith
249 
250 /-- The predictive assertion simultaneously covers every event of any output event family. -/
251 theorem predictive_event_family_bound {E : Type*} (A : Finset G) (w : G → ℝ)
252     (kernel : G → E → ℝ) (hw : ∀ g, 0 ≤ w g) (hs : Summable w)
253     (hA : 0 < activeEvidence A w)
254     (hk0 : ∀ g e, 0 ≤ kernel g e) (hk1 : ∀ g e, kernel g e ≤ 1) :
255     ∀ e, |predictiveEvent (posterior w) (fun g => kernel g e) -
256       predictiveEvent (activePosterior A w) (fun g => kernel g e)| ≤
257         1 - activeEvidence A w / evidence w := by
258   intro e
259   exact active_predictive_event_bound A w (fun g => kernel g e) hw hs hA
260     (fun g => hk0 g e) (fun g => hk1 g e)
261 
262 /-- Proposition 23: exact posterior error, all-event predictive control and evidence bound. -/
263 theorem enumerated_grammar_accounting {E : Type*} (A : Finset G) (w : G → ℝ)
264     (kernel : G → E → ℝ) (bound : ℝ)
265     (hw : ∀ g, 0 ≤ w g) (hs : Summable w) (hA : 0 < activeEvidence A w)
266     (hk0 : ∀ g e, 0 ≤ kernel g e) (hk1 : ∀ g e, kernel g e ≤ 1)
267     (hb : omittedEvidence A w ≤ bound) :
268     (totalVariation (posterior w) (activePosterior A w) =
269       1 - activeEvidence A w / evidence w) ∧
270     (∀ e, |predictiveEvent (posterior w) (fun g => kernel g e) -
271       predictiveEvent (activePosterior A w) (fun g => kernel g e)| ≤
272         1 - activeEvidence A w / evidence w) ∧
273     (1 - activeEvidence A w / evidence w ≤ bound / (activeEvidence A w + bound)) := by
274   exact ⟨exact_posterior_tv A w hw hs hA,
275     predictive_event_family_bound A w kernel hw hs hA hk0 hk1,
276     omitted_evidence_bound A w bound hw hs hA hb⟩
277 
278 omit [DecidableEq G] in
279 /-- Positive full evidence ensures every sufficiently late active posterior is defined. -/
280 theorem active_evidence_eventually_positive (A : ℕ → Finset G) (w : G → ℝ)
281     (hs : Summable w) (hZ : 0 < evidence w)
282     (hmono : Monotone A) (hexhaust : ∀ g, ∃ n, g ∈ A n) :
283     ∀ᶠ n in Filter.atTop, 0 < activeEvidence (A n) w := by
284   exact (active_evidence_tendsto A w hs hmono hexhaust).eventually (Ioi_mem_nhds hZ)
285 
286 /-- The actual posterior TV error tends to zero, including arbitrary early zero-evidence stages. -/
287 theorem active_posterior_tv_tendsto_zero (A : ℕ → Finset G) (w : G → ℝ)
288     (hw : ∀ g, 0 ≤ w g) (hs : Summable w) (hZ : 0 < evidence w)
289     (hmono : Monotone A) (hexhaust : ∀ g, ∃ n, g ∈ A n) :
290     Filter.Tendsto (fun n => totalVariation (posterior w) (activePosterior (A n) w))
291       Filter.atTop (nhds 0) := by
292   have heq : (fun n => 1 - activeEvidence (A n) w / evidence w) =ᶠ[Filter.atTop]
293       (fun n => totalVariation (posterior w) (activePosterior (A n) w)) := by
294     filter_upwards [active_evidence_eventually_positive A w hs hZ hmono hexhaust] with n hn
295     exact (exact_posterior_tv (A n) w hw hs hn).symm
296   exact (posterior_tail_tendsto_zero A w hs hZ hmono hexhaust).congr' heq
297 
298 /-- A small unnormalized tail may still be half the posterior mass. -/
299 theorem two_program_tail_example :
300     totalVariation (posterior (fun _ : Bool => (1 / 100 : ℝ)))
301       (activePosterior {false} (fun _ : Bool => (1 / 100 : ℝ))) = 1 / 2 := by
302   norm_num [totalVariation, posterior, activePosterior, evidence, activeEvidence, tsum_fintype]
303 
304 end
305 end Komorebi.LSM.GrammarAccounting

Back to source controls