BernoulliRecordSeparation.lean

1 import KomorebiLSM.MarkovMinorization
2 import KomorebiLSM.MarkovMarginals
3 import Mathlib.Probability.Distributions.Bernoulli
4 import Mathlib.Probability.Moments.SubGaussian
5 import Mathlib.Probability.Independence.Basic
6 import Mathlib.MeasureTheory.Constructions.Pi
7 
8 /-! Actual nondegenerate Bernoulli full-record laws separate in total variation,
9 even though every one-time marginal has a fixed small gap and the constant
10 transition kernels share a strictly positive minorization. -/
11 set_option autoImplicit false
12 namespace Komorebi.LSM.MarkovStability.BernoulliSeparation
13 open MeasureTheory ProbabilityTheory Matrix SequentialLowerCertificate MeasureTVCalculus Filter
14 open scoped BigOperators ENNReal NNReal Topology
15 
16 /-- The actual two-point law, with true meaning value one. -/
17 noncomputable def coin (p : unitInterval) : Measure Bool := bernoulliMeasure true false p
18 instance coin_probability (p : unitInterval) : IsProbabilityMeasure (coin p) := by
19   unfold coin
20   infer_instance
21 
22 def bit (b : Bool) : ℝ := if b then 1 else 0
23 
24 theorem bit_measurable : Measurable bit := measurable_of_countable _
25 theorem bit_mem_unit (b : Bool) : bit b∈Set.Icc (0:ℝ) 1 := by cases b <;> norm_num [bit]
26 
27 theorem integral_bit (p : unitInterval) : (∫ b,bit b∂coin p)=(p:ℝ) := by
28   rw [coin,integral_bernoulliMeasure]
29   simp [bit,smul_eq_mul]
30 
31 /-- A complete record of n transitions contains n+1 independent observations. -/
32 noncomputable def iidLaw (p : unitInterval) (n : ℕ) : Measure (Fin (n+1) → Bool) :=
33   Measure.pi (fun _ => coin p)
34 instance iidLaw_probability (p : unitInterval) (n : ℕ) : IsProbabilityMeasure (iidLaw p n) := by
35   unfold iidLaw
36   infer_instance
37 
38 /-- Every actual coordinate marginal equals the declared Bernoulli law. -/
39 theorem iidLaw_coordinate (p : unitInterval) (n : ℕ) (i : Fin (n+1)) :
40     (iidLaw p n).map (fun w => w i)=coin p :=
41   (measurePreserving_eval (fun _ : Fin (n+1) => coin p) i).map_eq
42 
43 theorem coordinate_mean (p : unitInterval) (n : ℕ) (i : Fin (n+1)) :
44     (∫ w,bit (w i)∂iidLaw p n)=(p:ℝ) := by
45   rw [← integral_map (measurable_pi_apply i).aemeasurable bit_measurable.aestronglyMeasurable,
46     iidLaw_coordinate,integral_bit]
47 
48 /-- Independence is derived from the literal finite product measure. -/
49 theorem centered_coordinates_independent (p : unitInterval) (n : ℕ) :
50     iIndepFun (fun i (w : Fin (n+1) → Bool) => bit (w i)-(p:ℝ)) (iidLaw p n) := by
51   exact iIndepFun_pi (μ := fun _ : Fin (n+1) => coin p)
52     (X := fun _ b => bit b-(p:ℝ)) (fun _ => (bit_measurable.sub_const _).aemeasurable)
53 
54 /-- Ordinary bounded-variable Hoeffding applies to the actual coordinate mean. -/
55 theorem centered_coordinate_subgaussian (p : unitInterval) (n : ℕ) (i : Fin (n+1)) :
56     HasSubgaussianMGF (fun w => bit (w i)-(p:ℝ)) (1/4) (iidLaw p n) := by
57   have hm : Measurable (fun w : Fin (n+1) → Bool => bit (w i)) :=
58     bit_measurable.comp (measurable_pi_apply i)
59   have hb : ∀ᵐ w∂iidLaw p n,bit (w i)∈Set.Icc (0:ℝ) 1 :=
60     ae_of_all _ (fun w => bit_mem_unit (w i))
61   have h := hasSubgaussianMGF_of_mem_Icc hm.aemeasurable hb
62   rw [coordinate_mean p n i] at h
63   convert h using 1; norm_num
64 
65 noncomputable def sumBits (n : ℕ) (w : Fin (n+1) → Bool) : ℝ := ∑ i,bit (w i)
66 noncomputable def centeredSum (p : unitInterval) (n : ℕ) (w : Fin (n+1) → Bool) : ℝ :=
67   ∑ i,(bit (w i)-(p:ℝ))
68 
69 theorem centeredSum_eq (p : unitInterval) (n : ℕ) (w : Fin (n+1) → Bool) :
70     centeredSum p n w=sumBits n w-((n:ℝ)+1)*(p:ℝ) := by
71   simp [centeredSum,sumBits,Finset.sum_sub_distrib]
72 
73 theorem centeredSum_subgaussian (p : unitInterval) (n : ℕ) :
74     HasSubgaussianMGF (centeredSum p n) (((n:NNReal)+1)/4) (iidLaw p n) := by
75   unfold centeredSum
76   have h := HasSubgaussianMGF.sum_of_iIndepFun (centered_coordinates_independent p n)
77     (s := Finset.univ) (c := fun _ => (1/4:NNReal))
78     (fun i _ => centered_coordinate_subgaussian p n i)
79   simpa [div_eq_mul_inv] using h
80 
81 /-- Exponential error bound for a fixed positive empirical-mean gap. -/
82 theorem centered_upper_tail (p : unitInterval) (n : ℕ) (d : ℝ) (hd : 0≤d) :
83     (iidLaw p n).real {w | (((n:ℝ)+1)*d)≤centeredSum p n w}≤
84       Real.exp (-2*((n:ℝ)+1)*d^2) := by
85   have h := (centeredSum_subgaussian p n).measure_ge_le
86     (mul_nonneg (by positivity : 0≤(n:ℝ)+1) hd)
87   have hn : (n:ℝ)+1≠0 := ne_of_gt (by positivity)
88   push_cast at h
89   have he : -((((n:ℝ)+1)*d)^2)/(2*(((n:ℝ)+1)/4)) = -2*((n:ℝ)+1)*d^2 := by
90     field_simp [hn]
91     ring
92   simpa only [he] using h
93 
94 /-- The opposite tail uses the actual negative centered sum. -/
95 theorem centered_lower_tail (p : unitInterval) (n : ℕ) (d : ℝ) (hd : 0≤d) :
96     (iidLaw p n).real {w | (((n:ℝ)+1)*d)≤-centeredSum p n w}≤
97       Real.exp (-2*((n:ℝ)+1)*d^2) := by
98   have h := (centeredSum_subgaussian p n).neg.measure_ge_le
99     (mul_nonneg (by positivity : 0≤(n:ℝ)+1) hd)
100   have hn : (n:ℝ)+1≠0 := ne_of_gt (by positivity)
101   push_cast at h
102   have he : -((((n:ℝ)+1)*d)^2)/(2*(((n:ℝ)+1)/4)) = -2*((n:ℝ)+1)*d^2 := by
103     field_simp [hn]
104     ring
105   simpa only [he,Pi.neg_apply] using h
106 
107 noncomputable def empiricalMean (n : ℕ) (w : Fin (n+1) → Bool) : ℝ :=
108   sumBits n w/((n:ℝ)+1)
109 
110 /-- The actual midpoint empirical-mean test of the source. -/
111 def aboveMidpoint (p q : unitInterval) (n : ℕ) : Set (Fin (n+1) → Bool) :=
112   {w | ((n:ℝ)+1)*((p:ℝ)+(q:ℝ))/2≤sumBits n w}
113 
114 theorem aboveMidpoint_measurable (p q : unitInterval) (n : ℕ) :
115     MeasurableSet (aboveMidpoint p q n) := by
116   apply measurableSet_le measurable_const
117   exact Finset.measurable_sum _ (fun i _ => bit_measurable.comp (measurable_pi_apply i))
118 
119 theorem aboveMidpoint_iff (p q : unitInterval) (n : ℕ) (w : Fin (n+1) → Bool) :
120     w∈aboveMidpoint p q n ↔ ((p:ℝ)+(q:ℝ))/2≤empiricalMean n w := by
121   unfold aboveMidpoint empiricalMean
122   rw [le_div_iff₀ (by positivity : 0<(n:ℝ)+1)]
123   simp only [Set.mem_ofPred_eq]
124   constructor <;> intro h <;> nlinarith
125 
126 noncomputable def separationError (p q : unitInterval) (n : ℕ) : ℝ :=
127   Real.exp (-2*((n:ℝ)+1)*(((q:ℝ)-(p:ℝ))/2)^2)
128 
129 /-- Both empirical-mean classification errors have a proved exponential bound. -/
130 theorem midpoint_error_bounds (p q : unitInterval) (hpq : (p:ℝ)<(q:ℝ)) (n : ℕ) :
131     (iidLaw p n).real (aboveMidpoint p q n)≤separationError p q n ∧
132       (iidLaw q n).real (aboveMidpoint p q n)ᶜ≤separationError p q n := by
133   let d : ℝ := ((q:ℝ)-(p:ℝ))/2
134   have hd : 0≤d := (div_pos (sub_pos.mpr hpq) (by norm_num)).le
135   constructor
136   · have hs : aboveMidpoint p q n⊆{w | ((n:ℝ)+1)*d≤centeredSum p n w} := by
137       intro w hw
138       change ((n:ℝ)+1)*((p:ℝ)+(q:ℝ))/2≤sumBits n w at hw
139       change ((n:ℝ)+1)*d≤centeredSum p n w
140       rw [centeredSum_eq]
141       dsimp [d]
142       nlinarith
143     exact (ENNReal.toReal_mono (measure_ne_top _ _) (measure_mono hs)).trans
144       (centered_upper_tail p n d hd)
145   · have hs : (aboveMidpoint p q n)ᶜ⊆{w | ((n:ℝ)+1)*d≤-centeredSum q n w} := by
146       intro w hw
147       have hl : sumBits n w<((n:ℝ)+1)*((p:ℝ)+(q:ℝ))/2 := lt_of_not_ge hw
148       change ((n:ℝ)+1)*d≤-centeredSum q n w
149       rw [centeredSum_eq]
150       dsimp [d]
151       nlinarith
152     exact (ENNReal.toReal_mono (measure_ne_top _ _) (measure_mono hs)).trans
153       (centered_lower_tail q n d hd)
154 
155 /-- A literal measurable event gives a lower bound for the actual probability
156 convention of total variation. -/
157 theorem event_gap_le {X : Type*} [MeasurableSpace X] (P Q : Measure X)
158     [IsProbabilityMeasure P] [IsProbabilityMeasure Q] (E : Set X) (hE : MeasurableSet E) :
159     Q.real E-P.real E≤lawTV P Q := by
160   let f : X → ℝ := E.indicator (fun _ => 1)
161   have hf : Measurable f := measurable_const.indicator hE
162   have h0 : ∀ x,0≤f x := fun x => by by_cases hx : x∈E <;> simp [f,hx]
163   have h1 : ∀ x,f x≤1 := fun x => by by_cases hx : x∈E <;> simp [f,hx]
164   have h := bounded_test_integral_le_tv P Q f hf h0 h1
165   have hi (ν : Measure X) : (∫ x,f x∂ν)=ν.real E := by simp [f,integral_indicator hE]
166   rw [hi P,hi Q,abs_sub_comm] at h
167   exact (le_abs_self _).trans h
168 
169 /-- The midpoint test proves actual full-record TV approaches its maximal value. -/
170 theorem iidLaw_tv_lower (p q : unitInterval) (hpq : (p:ℝ)<(q:ℝ)) (n : ℕ) :
171     1-2*separationError p q n≤lawTV (iidLaw p n) (iidLaw q n) := by
172   have he := midpoint_error_bounds p q hpq n
173   have hq := he.2
174   rw [measureReal_compl (aboveMidpoint_measurable p q n)] at hq
175   simp only [probReal_univ] at hq
176   have hgap := event_gap_le (iidLaw p n) (iidLaw q n) (aboveMidpoint p q n)
177     (aboveMidpoint_measurable p q n)
178   linarith [he.1]
179 
180 /-- The explicit record measures are consistent under dropping the last observation. -/
181 theorem iidLaw_prefix (p : unitInterval) (n : ℕ) :
182     (iidLaw p (n+1)).map (fun w (i : Fin (n+1)) => w i.castSucc)=iidLaw p n := by
183   have hfull : iIndepFun (fun j (w : Fin (n+1+1) → Bool) => w j) (iidLaw p (n+1)) :=
184     iIndepFun_pi (μ := fun _ : Fin (n+1+1) => coin p)
185       (X := fun _ b => b) (fun _ => measurable_id.aemeasurable)
186   have hsmall := hfull.precomp (Fin.castSucc_injective (n+1))
187   have hmap := hsmall.map_fun_eq_pi_map
188     (fun i => (measurable_pi_apply i.castSucc).aemeasurable)
189   calc
190     _ = Measure.pi (fun i : Fin (n+1) =>
191         (iidLaw p (n+1)).map (fun w => w i.castSucc)) := hmap
192     _ = iidLaw p n := by simp only [iidLaw_coordinate]; rfl
193 
194 /-- Actual total variation tends to one; the limit is not assumed from a
195 numerical or asymptotic proxy. -/
196 theorem iidLaw_tv_tendsto_one (p q : unitInterval) (hpq : (p:ℝ)<(q:ℝ)) :
197     Tendsto (fun n => lawTV (iidLaw p n) (iidLaw q n)) atTop (𝓝 1) := by
198   let d : ℝ := ((q:ℝ)-(p:ℝ))/2
199   have hd : 0<d := div_pos (sub_pos.mpr hpq) (by norm_num)
200   have hN : Tendsto (fun n : ℕ => (n:ℝ)+1) atTop atTop := by
201     exact tendsto_atTop_add_const_right atTop 1 (tendsto_natCast_atTop_atTop (R := ℝ))
202   have hc : -2*d^2<0 := mul_neg_of_neg_of_pos (by norm_num) (sq_pos_of_pos hd)
203   have he : Tendsto (separationError p q) atTop (𝓝 0) := by
204     have ht := Real.tendsto_exp_atBot.comp (hN.const_mul_atTop_of_neg hc)
205     convert ht using 1
206     funext n
207     unfold separationError
208     congr 1
209     dsimp [d]
210     ring
211   have hl : Tendsto (fun n => 1-2*separationError p q n) atTop (𝓝 1) := by
212     simpa using tendsto_const_nhds.sub (he.const_mul 2)
213   exact tendsto_of_tendsto_of_tendsto_of_le_of_le hl tendsto_const_nhds
214     (iidLaw_tv_lower p q hpq) (fun n => lawTV_le_one (iidLaw p n) (iidLaw q n))
215 
216 /-- The exact one-time distance is the parameter gap. -/
217 theorem coin_tv (p q : unitInterval) : lawTV (coin p) (coin q)=|(p:ℝ)-(q:ℝ)| := by
218   apply le_antisymm
219   · apply lawTV_le_of_bounded_tests
220     intro f hf h0 h1
221     have hi (r : unitInterval) : (∫ b,f b∂coin r)=
222         (r:ℝ)*f true+(1-(r:ℝ))*f false := by
223       rw [coin,integral_bernoulliMeasure]
224       simp [smul_eq_mul]
225     rw [hi p,hi q]
226     have he : (p:ℝ)*f true+(1-(p:ℝ))*f false-((q:ℝ)*f true+(1-(q:ℝ))*f false)=
227         ((p:ℝ)-(q:ℝ))*(f true-f false) := by ring
228     rw [he,abs_mul]
229     apply mul_le_of_le_one_right (abs_nonneg _)
230     exact abs_le.2 ⟨by linarith [h0 true,h1 false],by linarith [h1 true,h0 false]⟩
231   · have h := bounded_test_integral_le_tv (coin p) (coin q) bit bit_measurable
232       (fun b => (bit_mem_unit b).1) (fun b => (bit_mem_unit b).2)
233     simpa only [integral_bit] using h
234 
235 noncomputable def coinKernel (p : unitInterval) : Kernel Bool Bool := Kernel.const Bool (coin p)
236 instance coinKernel_markov (p : unitInterval) : IsMarkovKernel (coinKernel p) := by
237   unfold coinKernel
238   infer_instance
239 
240 theorem coinKernel_comp (p : unitInterval) (ν : Measure Bool) [IsProbabilityMeasure ν] :
241     coinKernel p ∘ₘ ν=coin p := by
242   rw [coinKernel,Measure.const_comp,measure_univ,one_smul]
243 
244 theorem marginal_coin (p : unitInterval) (n : ℕ) :
245     marginal (coinKernel p) (coin p) n=coin p := by
246   induction n with
247   | zero => rfl
248   | succ n ih => rw [marginal,ih,coinKernel_comp]
249 
250 /-- A positive amount of the false atom is an actual common minorization. -/
251 theorem coinKernel_minorized (p : unitInterval) (ρ : ℝ) (hρ : ρ≤1-(p:ℝ)) :
252     Minorized (coinKernel p) ρ (Measure.dirac false) := by
253   intro x
254   change ENNReal.ofReal ρ • Measure.dirac false≤coin p
255   have hfalse : (coin p).real {false}=1-(p:ℝ) := by
256     exact bernoulliMeasure_real_apply_of_notMem_of_mem p (measurableSet_singleton false)
257       (by simp) (by simp)
258   have hcost : ENNReal.ofReal ρ≤coin p {false} := by
259     have h := ENNReal.ofReal_le_ofReal hρ
260     rwa [← hfalse,Measure.real,ENNReal.ofReal_toReal (measure_ne_top _ _)] at h
261   intro E
262   have hE : MeasurableSet E := (Set.toFinite E).countable.measurableSet
263   by_cases hf : false∈E
264   · simpa [Measure.smul_apply,Measure.dirac_apply' _ hE,hf,smul_eq_mul] using
265       hcost.trans (measure_mono (Set.singleton_subset_iff.2 hf))
266   · simp [Measure.smul_apply,Measure.dirac_apply' _ hE,hf]
267 
268 /-- The source's counterexample uses two strictly interior Bernoulli
269 parameters, not a degenerate zero-probability law. -/
270 theorem interior_bernoulli_record_separation (p q : unitInterval)
271     (hp : 0<(p:ℝ)) (hpq : (p:ℝ)<(q:ℝ)) (hq : (q:ℝ)<1) :
272     0<1-(q:ℝ) ∧ 1-(q:ℝ)≤1 ∧
273     Minorized (coinKernel p) (1-(q:ℝ)) (Measure.dirac false) ∧
274     Minorized (coinKernel q) (1-(q:ℝ)) (Measure.dirac false) ∧
275     (∀ n,lawTV (marginal (coinKernel p) (coin p) n)
276       (marginal (coinKernel q) (coin q) n)=(q:ℝ)-(p:ℝ)) ∧
277     (∀ x,lawTV (coinKernel p x) (coinKernel q x)=(q:ℝ)-(p:ℝ)) ∧
278     Tendsto (fun n => lawTV (iidLaw p n) (iidLaw q n)) atTop (𝓝 1) := by
279   have hgap : |(p:ℝ)-(q:ℝ)|=(q:ℝ)-(p:ℝ) := by rw [abs_of_neg (sub_neg.mpr hpq)]; ring
280   refine ⟨by linarith,by linarith,coinKernel_minorized p _ (by linarith),
281     coinKernel_minorized q _ le_rfl,?_,?_,iidLaw_tv_tendsto_one p q hpq⟩
282   · intro n
283     simpa only [marginal_coin] using (coin_tv p q).trans hgap
284   · intro x
285     change lawTV (coin p) (coin q)=(q:ℝ)-(p:ℝ)
286     rw [coin_tv,hgap]
287 
288 noncomputable def halfParameter : unitInterval := ⟨1/2,by constructor <;> norm_num⟩
289 noncomputable def closeParameter (ε : ℝ) (hε : 0<ε) (hε1 : ε<1) : unitInterval :=
290   ⟨1/2+ε/4,by constructor <;> linarith⟩
291 
292 /-- The marginal gap can be made arbitrarily small while keeping the same
293 strictly positive minorization one quarter and full-record TV limit one. -/
294 theorem arbitrarily_small_marginal_gap (ε : ℝ) (hε : 0<ε) (hε1 : ε<1) :
295     let p := halfParameter
296     let q := closeParameter ε hε hε1
297     (0<(p:ℝ) ∧ (p:ℝ)<(q:ℝ) ∧ (q:ℝ)<1) ∧
298     (0<ε/4 ∧ ε/4<ε) ∧
299     Minorized (coinKernel p) (1/4) (Measure.dirac false) ∧
300     Minorized (coinKernel q) (1/4) (Measure.dirac false) ∧
301     (∀ n,lawTV (marginal (coinKernel p) (coin p) n)
302       (marginal (coinKernel q) (coin q) n)=ε/4) ∧
303     Tendsto (fun n => lawTV (iidLaw p n) (iidLaw q n)) atTop (𝓝 1) := by
304   dsimp only
305   have hp : 0<(halfParameter:ℝ) := by norm_num [halfParameter]
306   have hpq : (halfParameter:ℝ)<(closeParameter ε hε hε1:ℝ) := by
307     dsimp [halfParameter,closeParameter]
308     linarith
309   have hq : (closeParameter ε hε hε1:ℝ)<1 := by dsimp [closeParameter]; linarith
310   have hi := interior_bernoulli_record_separation halfParameter (closeParameter ε hε hε1) hp hpq hq
311   refine ⟨⟨hp,hpq,hq⟩,⟨by linarith,by linarith⟩,
312     coinKernel_minorized _ _ (by norm_num [halfParameter]),
313     coinKernel_minorized _ _ (by dsimp [closeParameter]; linarith),?_,hi.2.2.2.2.2.2⟩
314   intro n
315   have h := hi.2.2.2.2.1 n
316   simpa [halfParameter,closeParameter] using h
317 
318 end Komorebi.LSM.MarkovStability.BernoulliSeparation

Back to source controls