ResetCertificate.lean

1 import Mathlib.Probability.Moments.SubGaussian
2 import Mathlib.Analysis.CStarAlgebra.Matrix
3 
4 /-! The reset experiment concentration certificate. Trials for each experiment
5 are independent; experiments themselves may be arbitrarily dependent. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.ResetCertificate
8 open MeasureTheory ProbabilityTheory Real
9 open scoped BigOperators
10 
11 variable {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
12 
13 /-- Empirical probability of an experiment from its reset trials. -/
14 noncomputable def sampleMean {N : ℕ} (X : Fin N → Ω → ℝ) (ω : Ω) : ℝ :=
15   (∑ i, X i ω) / N
16 
17 /-- Hoeffding's lemma applies to every bounded reset indicator. -/
18 theorem centered_trial_subgaussian {X : Ω → ℝ} {p : ℝ}
19     (hm : AEMeasurable X μ) (hb : ∀ᵐ ω ∂μ, X ω ∈ Set.Icc (0:ℝ) 1)
20     (hp : ∫ ω, X ω ∂μ = p) :
21     HasSubgaussianMGF (fun ω ↦ X ω - p) (1/4 : NNReal) μ := by
22   have h := hasSubgaussianMGF_of_mem_Icc hm hb
23   rw [hp] at h
24   convert h using 1
25   norm_num
26 
27 /-- The centered sum of N independent reset trials has variance proxy N/4. -/
28 theorem centered_sum_subgaussian {N : ℕ} (X : Fin N → Ω → ℝ) (p : ℝ)
29     (hind : iIndepFun X μ) (hm : ∀ i, AEMeasurable (X i) μ)
30     (hb : ∀ i, ∀ᵐ ω ∂μ, X i ω ∈ Set.Icc (0:ℝ) 1)
31     (hp : ∀ i, ∫ ω, X i ω ∂μ = p) :
32     HasSubgaussianMGF (fun ω ↦ ∑ i, (X i ω-p)) ((N:NNReal)/4) μ := by
33   have hi : iIndepFun (fun i ω ↦ X i ω-p) μ :=
34     hind.comp (fun _ x ↦ x-p) (fun _ ↦ by fun_prop)
35   have hs := HasSubgaussianMGF.sum_of_iIndepFun hi
36     (s := Finset.univ) (c := fun _ ↦ (1/4:NNReal))
37     (fun i _ ↦ centered_trial_subgaussian (hm i) (hb i) (hp i))
38   simpa [div_eq_mul_inv] using hs
39 
40 omit [MeasurableSpace Ω] in
41 /-- The sample-mean error is the centered reset sum divided by N. -/
42 theorem centered_sum_eq {N : ℕ} (hN : 0<N) (X : Fin N → Ω → ℝ) (p : ℝ) (ω : Ω) :
43     (∑ i, (X i ω-p)) = (N:ℝ)*(sampleMean X ω-p) := by
44   have hn : (N:ℝ) ≠ 0 := by exact_mod_cast Nat.ne_of_gt hN
45   simp only [Finset.sum_sub_distrib, Finset.sum_const, Finset.card_univ,
46     Fintype.card_fin, nsmul_eq_mul, sampleMean]
47   field_simp
48 
49 /-- Two-sided Hoeffding bound for one reset experiment, with no assumption
50 beyond the declared independence, bounded indicators and common expectation. -/
51 theorem reset_error_bound {N : ℕ} (hN : 0<N) (X : Fin N → Ω → ℝ) (p ε : ℝ)
52     (hind : iIndepFun X μ) (hm : ∀ i, AEMeasurable (X i) μ)
53     (hb : ∀ i, ∀ᵐ ω ∂μ, X i ω ∈ Set.Icc (0:ℝ) 1)
54     (hp : ∀ i, ∫ ω, X i ω ∂μ = p) (hε : 0≤ε) :
55     μ.real {ω | ε ≤ |sampleMean X ω-p|} ≤ 2*exp (-2*N*ε^2) := by
56   have hn : (0:ℝ)<N := by exact_mod_cast hN
57   have hs := centered_sum_subgaussian X p hind hm hb hp
58   have hu := hs.measure_ge_le (mul_nonneg hn.le hε)
59   have hl := hs.neg.measure_ge_le (mul_nonneg hn.le hε)
60   have hexp : exp (-((N:ℝ)*ε)^2 / (2*((N:NNReal)/4:NNReal))) =
61       exp (-2*N*ε^2) := by
62     congr 1
63     push_cast
64     field_simp
65     ring
66   rw [hexp] at hu hl
67   have hevent : {ω | ε ≤ |sampleMean X ω-p|} ⊆
68       {ω | (N:ℝ)*ε ≤ ∑ i, (X i ω-p)} ∪
69       {ω | (N:ℝ)*ε ≤ -(∑ i, (X i ω-p))} := by
70     intro ω h
71     change ε ≤ |sampleMean X ω-p| at h
72     rw [le_abs] at h
73     rcases h with h|h
74     · exact Or.inl (by
75         change (N:ℝ)*ε ≤ ∑ i, (X i ω-p)
76         rw [centered_sum_eq hN]
77         nlinarith)
78     · exact Or.inr (by
79         change (N:ℝ)*ε ≤ -(∑ i, (X i ω-p))
80         rw [centered_sum_eq hN]
81         nlinarith)
82   calc
83     _ ≤ μ.real ({ω | (N:ℝ)*ε ≤ ∑ i, (X i ω-p)} ∪
84         {ω | (N:ℝ)*ε ≤ -(∑ i, (X i ω-p))}) := measureReal_mono hevent
85     _ ≤ _ := measureReal_union_le _ _
86     _ ≤ _ := by simpa only [Pi.neg_apply, two_mul] using add_le_add hu hl
87 
88 /-- Simultaneous reset estimates need no independence across experiments. -/
89 theorem simultaneous_error_bound {W : Type*} [Fintype W] {N : ℕ}
90     (hN : 0<N) (X : W → Fin N → Ω → ℝ) (p : W → ℝ) (ε : ℝ)
91     (hind : ∀ w, iIndepFun (X w) μ)
92     (hm : ∀ w i, AEMeasurable (X w i) μ)
93     (hb : ∀ w i, ∀ᵐ ω ∂μ, X w i ω ∈ Set.Icc (0:ℝ) 1)
94     (hp : ∀ w i, ∫ ω, X w i ω ∂μ = p w) (hε : 0≤ε) :
95     μ.real {ω | ∃ w, ε < |sampleMean (X w) ω-p w|} ≤
96       2*Fintype.card W*exp (-2*N*ε^2) := by
97   classical
98   have hset : {ω | ∃ w, ε < |sampleMean (X w) ω-p w|} ⊆
99       ⋃ w, {ω | ε ≤ |sampleMean (X w) ω-p w|} := by
100     rintro ω ⟨w, hw⟩
101     exact Set.mem_iUnion.mpr ⟨w, hw.le⟩
102   calc
103     _ ≤ μ.real (⋃ w, {ω | ε ≤ |sampleMean (X w) ω-p w|}) := measureReal_mono hset
104     _ ≤ ∑ w, μ.real {ω | ε ≤ |sampleMean (X w) ω-p w|} :=
105       measureReal_iUnion_fintype_le _
106     _ ≤ ∑ _w : W, 2*exp (-2*N*ε^2) := Finset.sum_le_sum (fun w _ ↦
107       reset_error_bound hN (X w) (p w) ε (hind w) (hm w) (hb w) (hp w) hε)
108     _ = _ := by simp; ring
109 
110 /-- The declared simultaneous confidence radius for M experiments and N trials. -/
111 noncomputable def radius (M N : ℕ) (δ : ℝ) : ℝ :=
112   sqrt (log (2*M/δ)/(2*N))
113 
114 omit [MeasurableSpace Ω] in
115 /-- The radius converts the finite union bound into the chosen confidence budget. -/
116 theorem radius_budget {M N : ℕ} (hM : 0<M) (hN : 0<N) {δ : ℝ}
117     (hδ : 0<δ) (hδ1 : δ<1) :
118     2*(M:ℝ)*exp (-2*N*(radius M N δ)^2)=δ := by
119   have hm : (1:ℝ) ≤ M := by exact_mod_cast hM
120   have hn : (0:ℝ) < N := by exact_mod_cast hN
121   have hratio : 0 < 2*(M:ℝ)/δ := by positivity
122   have hrat1 : 1 ≤ 2*(M:ℝ)/δ := (le_div_iff₀ hδ).mpr (by nlinarith)
123   have hlog : 0 ≤ log (2*(M:ℝ)/δ) := log_nonneg hrat1
124   rw [radius, sq_sqrt (div_nonneg hlog (by positivity))]
125   have he : -2*(N:ℝ)*(log (2*M/δ)/(2*N)) = -log (2*M/δ) := by
126     field_simp
127   rw [he, exp_neg, exp_log hratio]
128   field_simp
129 
130 /-- P35's confidence statement, for measurable bounded reset indicators. -/
131 theorem reset_probability_certificate {W : Type*} [Fintype W] [Nonempty W] {N : ℕ}
132     (hN : 0<N) (X : W → Fin N → Ω → ℝ) (p : W → ℝ) {δ : ℝ}
133     (hδ : 0<δ) (hδ1 : δ<1)
134     (hind : ∀ w, iIndepFun (X w) μ)
135     (hm : ∀ w i, Measurable (X w i))
136     (hb : ∀ w i, ∀ᵐ ω ∂μ, X w i ω ∈ Set.Icc (0:ℝ) 1)
137     (hp : ∀ w i, ∫ ω, X w i ω ∂μ = p w) :
138     1-δ ≤ μ.real {ω | ∀ w, |sampleMean (X w) ω-p w| ≤ radius (Fintype.card W) N δ} := by
139   have hbad := simultaneous_error_bound hN X p (radius (Fintype.card W) N δ)
140     hind (fun w i ↦ (hm w i).aemeasurable) hb hp (sqrt_nonneg _)
141   rw [radius_budget Fintype.card_pos hN hδ hδ1] at hbad
142   have hmeas : MeasurableSet {ω | ∃ w, radius (Fintype.card W) N δ <
143       |sampleMean (X w) ω-p w|} := by
144     simp only [Set.ofPred_exists]
145     apply MeasurableSet.iUnion
146     intro w
147     apply measurableSet_lt measurable_const
148     unfold sampleMean
149     fun_prop
150   have hcomp : {ω | ∀ w, |sampleMean (X w) ω-p w| ≤ radius (Fintype.card W) N δ} =
151       {ω | ∃ w, radius (Fintype.card W) N δ < |sampleMean (X w) ω-p w|}ᶜ := by
152     ext ω
153     simp
154   rw [hcomp, measureReal_compl hmeas]
155   simpa using sub_le_sub_left hbad 1
156 
157 /-- Entrywise probability error bounds the Euclidean initial-coordinate error. -/
158 theorem vector_norm_le {r : ℕ} (x : EuclideanSpace ℝ (Fin r)) (ε : ℝ)
159     (hε : 0≤ε) (hx : ∀ i, |x i|≤ε) : ‖x‖ ≤ sqrt r*ε := by
160   have hsum : ∑ i, ‖x i‖^2 ≤ (r:ℝ)*ε^2 := by
161     calc
162       _ ≤ ∑ _i : Fin r, ε^2 := Finset.sum_le_sum (fun i _ ↦
163         by simpa only [Real.norm_eq_abs] using pow_le_pow_left₀ (abs_nonneg _) (hx i) 2)
164       _ = _ := by simp
165   rw [← EuclideanSpace.norm_sq_eq] at hsum
166   have hs : (sqrt (r:ℝ))^2=(r:ℝ) := sq_sqrt (Nat.cast_nonneg r)
167   nlinarith [norm_nonneg x, sqrt_nonneg (r:ℝ), mul_nonneg (sqrt_nonneg (r:ℝ)) hε]
168 
169 set_option maxHeartbeats 800000 in
170 /-- Entrywise probability error bounds the actual spectral operator norm. -/
171 theorem matrix_opNorm_le {r : ℕ} (A : Matrix (Fin r) (Fin r) ℝ) (ε : ℝ)
172     (hε : 0≤ε) (hA : ∀ i j, |A i j|≤ε) :
173     ‖((A.toEuclideanLin.toContinuousLinearMap) : EuclideanSpace ℝ (Fin r) →L[ℝ] EuclideanSpace ℝ (Fin r))‖ ≤ (r:ℝ)*ε := by
174   apply ContinuousLinearMap.opNorm_le_bound _ (by positivity)
175   intro x
176   have hx : ∑ j : Fin r, (x j)^2 = ‖x‖^2 := by
177     simpa only [Real.norm_eq_abs, sq_abs] using (EuclideanSpace.norm_sq_eq x).symm
178   have hrow : ∀ i, ∑ j, (A i j)^2 ≤ (r:ℝ)*ε^2 := by
179     intro i
180     calc
181       _ ≤ ∑ _j : Fin r, ε^2 := Finset.sum_le_sum (fun j _ ↦
182         by simpa only [sq_abs] using pow_le_pow_left₀ (abs_nonneg _) (hA i j) 2)
183       _ = _ := by simp
184   have hi : ∀ i, ((((A.toEuclideanLin.toContinuousLinearMap) : EuclideanSpace ℝ (Fin r) →L[ℝ] EuclideanSpace ℝ (Fin r))) x i)^2 ≤ (r:ℝ)*ε^2*‖x‖^2 := by
185     intro i
186     calc
187       _ = (∑ j, A i j*x j)^2 := rfl
188       _ ≤ (∑ j, (A i j)^2)*(∑ j, (x j)^2) := by
189         simpa using Finset.sum_mul_sq_le_sq_mul_sq Finset.univ (fun j ↦ A i j) (fun j ↦ x j)
190       _ ≤ _ := by rw [hx]; exact mul_le_mul_of_nonneg_right (hrow i) (sq_nonneg _)
191   have hout : ‖(((A.toEuclideanLin.toContinuousLinearMap) : EuclideanSpace ℝ (Fin r) →L[ℝ] EuclideanSpace ℝ (Fin r))) x‖^2 ≤ ((r:ℝ)*ε*‖x‖)^2 := by
192     rw [EuclideanSpace.norm_sq_eq]
193     simp only [Real.norm_eq_abs, sq_abs]
194     calc
195       _ ≤ ∑ _i : Fin r, (r:ℝ)*ε^2*‖x‖^2 := Finset.sum_le_sum (fun i _ ↦ hi i)
196       _ = _ := by simp; ring
197   nlinarith [norm_nonneg ((((A.toEuclideanLin.toContinuousLinearMap) : EuclideanSpace ℝ (Fin r) →L[ℝ] EuclideanSpace ℝ (Fin r))) x),
198     mul_nonneg (mul_nonneg (Nat.cast_nonneg r) hε) (norm_nonneg x)]
199 
200 /-- Error in a probability table whose entries are covered by selected experiments. -/
201 noncomputable def tableError {W : Type*} {N r : ℕ}
202     (X : W → Fin N → Ω → ℝ) (p : W → ℝ)
203     (entry : Fin r → Fin r → W) (ω : Ω) : Matrix (Fin r) (Fin r) ℝ :=
204   fun i j ↦ sampleMean (X (entry i j)) ω-p (entry i j)
205 
206 /-- Error in initial coordinates covered by selected experiments. -/
207 noncomputable def initialError {W : Type*} {N r : ℕ}
208     (X : W → Fin N → Ω → ℝ) (p : W → ℝ)
209     (entry : Fin r → W) (ω : Ω) : EuclideanSpace ℝ (Fin r) :=
210   WithLp.toLp 2 (fun i ↦ sampleMean (X (entry i)) ω-p (entry i))
211 
212 /-- Full P35 endpoint: the same reset event controls H, every G_s and b₀,
213 using actual matrix spectral norms and the Euclidean initial-coordinate norm.
214 The coverage maps may repeat selected words; cross-word independence is absent. -/
215 theorem reset_table_probability_certificate {W S : Type*}
216     [Fintype W] [Nonempty W] [Fintype S] {N r : ℕ}
217     (hN : 0<N) (X : W → Fin N → Ω → ℝ) (p : W → ℝ) {δ : ℝ}
218     (hδ : 0<δ) (hδ1 : δ<1)
219     (hind : ∀ w, iIndepFun (X w) μ)
220     (hm : ∀ w i, Measurable (X w i))
221     (hb : ∀ w i, ∀ᵐ ω ∂μ, X w i ω ∈ Set.Icc (0:ℝ) 1)
222     (hp : ∀ w i, ∫ ω, X w i ω ∂μ = p w)
223     (Hentry : Fin r → Fin r → W) (Gentry : S → Fin r → Fin r → W)
224     (bentry : Fin r → W) :
225     1-δ ≤ μ.real {ω |
226       ‖((tableError X p Hentry ω).toEuclideanLin.toContinuousLinearMap :
227         EuclideanSpace ℝ (Fin r) →L[ℝ] EuclideanSpace ℝ (Fin r))‖ ≤
228         (r:ℝ)*radius (Fintype.card W) N δ ∧
229       (∀ s, ‖((tableError X p (Gentry s) ω).toEuclideanLin.toContinuousLinearMap :
230         EuclideanSpace ℝ (Fin r) →L[ℝ] EuclideanSpace ℝ (Fin r))‖ ≤
231         (r:ℝ)*radius (Fintype.card W) N δ) ∧
232       ‖initialError X p bentry ω‖ ≤ sqrt r*radius (Fintype.card W) N δ} := by
233   have hprob := reset_probability_certificate hN X p hδ hδ1 hind hm hb hp
234   apply hprob.trans (measureReal_mono ?_)
235   intro ω hω
236   change ∀ w, |sampleMean (X w) ω-p w| ≤ radius (Fintype.card W) N δ at hω
237   refine ⟨matrix_opNorm_le _ _ (sqrt_nonneg _) (fun i j ↦ hω (Hentry i j)), ?_, ?_⟩
238   · intro s
239     exact matrix_opNorm_le _ _ (sqrt_nonneg _) (fun i j ↦ hω (Gentry s i j))
240   · exact vector_norm_le _ _ (sqrt_nonneg _) (fun i ↦ hω (bentry i))
241 
242 end Komorebi.LSM.ResetCertificate

Back to source controls