PredictableResidual.lean

1 import KomorebiLSM.SequentialConfidence
2 import Mathlib.Probability.Moments.SubGaussian
3 import Mathlib.Topology.Algebra.InfiniteSum.ENNReal
4 
5 /-! Predictable residual concentration from actual conditional expectations. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.PredictableResidual
8 open MeasureTheory ProbabilityTheory Real
9 open scoped BigOperators NNReal ENNReal
10 variable {Ω : Type*} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω]
11 variable {μ : Measure Ω} [IsProbabilityMeasure μ]
12 
13 /-- A function measurable before an observation is conditionally constant. -/
14 theorem predictable_kernel_constant {m : MeasurableSpace Ω} (hm : m≤mΩ)
15     (g : Ω → ℝ) (hg : Measurable[m] g) :
16     ∀ᵐ ω' ∂μ.trim hm, ∀ᵐ ω ∂condExpKernel (mΩ:=mΩ) μ m ω', g ω=g ω' := by
17   let : MeasurableSpace Ω := mΩ
18   apply @Measure.ae_ae_of_ae_compProd Ω Ω m mΩ (μ.trim hm)
19     (condExpKernel (mΩ:=mΩ) μ m) _ _ (fun q : Ω×Ω ↦ g q.2=g q.1)
20   rw [compProd_trim_condExpKernel hm]
21   have hdiag : @Measurable Ω (Ω×Ω) mΩ (m.prod mΩ) Function.diag :=
22     (measurable_id'' hm).prodMk measurable_id
23   apply (@ae_map_iff Ω (Ω×Ω) mΩ (m.prod mΩ) μ Function.diag
24     (@Measurable.aemeasurable Ω (Ω×Ω) mΩ (m.prod mΩ) Function.diag μ hdiag)
25     (fun q : Ω×Ω ↦ g q.2=g q.1) ?_).mpr
26   · exact ae_of_all _ (fun _ ↦ rfl)
27   · exact measurableSet_eq_fun (hg.mono hm le_rfl |>.comp measurable_snd)
28       (hg.comp measurable_fst)
29 
30 omit [StandardBorelSpace Ω] in
31 /-- The true conditional mean of a bounded test remains in its probability range. -/
32 theorem conditional_mean_mem_Icc {m : MeasurableSpace Ω} (hm : m≤mΩ)
33     (X : Ω → ℝ) (hX : @Measurable Ω ℝ mΩ _ X)
34     (hb : ∀ᵐ ω ∂μ, X ω ∈ Set.Icc (0:ℝ) 1) :
35     ∀ᵐ ω ∂μ, (μ[X | m]) ω ∈ Set.Icc (0:ℝ) 1 := by
36   let : MeasurableSpace Ω := mΩ
37   have hi := Integrable.of_mem_Icc (0:ℝ) 1 hX.aemeasurable hb
38   have hlo := condExp_nonneg (m:=m) (hb.mono fun _ h ↦ h.1)
39   have hhi := condExp_mono (m:=m) hi (integrable_const (1:ℝ)) (hb.mono fun _ h ↦ h.2)
40   rw [condExp_const hm] at hhi
41   filter_upwards [hlo,hhi] with ω hlo hhi using ⟨hlo,hhi⟩
42 
43 /-- Conditional Hoeffding's lemma derived for the actual conditional mean.
44 This formal kernel route assumes a standard Borel sample space. -/
45 theorem conditional_centered_subgaussian {m : MeasurableSpace Ω} (hm : m≤mΩ)
46     (X : Ω → ℝ) (hX : @Measurable Ω ℝ mΩ _ X)
47     (hb : ∀ᵐ ω ∂μ, X ω ∈ Set.Icc (0:ℝ) 1) :
48     HasCondSubgaussianMGF m hm (fun ω ↦ X ω-(μ[X | m]) ω) (1/4:NNReal) μ := by
49   let : MeasurableSpace Ω := mΩ
50   have hi := Integrable.of_mem_Icc (0:ℝ) 1 hX.aemeasurable hb
51   have hmean := conditional_mean_mem_Icc hm X hX hb
52   have hres : ∀ᵐ ω ∂μ, X ω-(μ[X | m]) ω ∈ Set.Icc (-1:ℝ) 1 := by
53     filter_upwards [hb,hmean] with ω h h' using ⟨by linarith [h.1,h'.2], by linarith [h.2,h'.1]⟩
54   have hresmeas : Measurable (fun ω ↦ X ω-(μ[X | m]) ω) :=
55     hX.sub (stronglyMeasurable_condExp.measurable.mono hm le_rfl)
56   refine ⟨?_,?_⟩
57   · intro t
58     rw [condExpKernel_comp_trim hm]
59     exact integrable_exp_mul_of_mem_Icc hresmeas.aemeasurable hres
60   · have hbound : ∀ᵐ ω' ∂μ.trim hm, ∀ᵐ ω ∂condExpKernel (mΩ:=mΩ) μ m ω', X ω∈Set.Icc (0:ℝ) 1 := by
61       apply Measure.ae_ae_of_ae_comp
62       rwa [condExpKernel_comp_trim hm]
63     have hconstant := predictable_kernel_constant (μ:=μ) hm (μ[X | m]) stronglyMeasurable_condExp.measurable
64     have hintegral := condExp_ae_eq_trim_integral_condExpKernel hm hi
65     filter_upwards [hbound,hconstant,hintegral] with ω' hbound hconstant hintegral
66     have hs := hasSubgaussianMGF_of_mem_Icc hX.aemeasurable hbound
67     rw [← hintegral] at hs
68     have heq : (fun ω ↦ X ω-(μ[X | m]) ω') =ᵐ[condExpKernel (mΩ:=mΩ) μ m ω']
69         (fun ω ↦ X ω-(μ[X | m]) ω) := hconstant.mono fun ω h ↦ by dsimp; rw [h]
70     have hs' : HasSubgaussianMGF (fun ω ↦ X ω-(μ[X | m]) ω) (1/4:NNReal)
71         (condExpKernel (mΩ:=mΩ) μ m ω') := by
72       convert hs.congr heq using 1
73       norm_num
74     exact hs'.mgf_le
75 
76 /-- Actual accumulated centered test error for times 1 through n. -/
77 noncomputable def centeredSum (ℱ : Filtration ℕ mΩ) (X : ℕ → Ω → ℝ) (n : ℕ) (ω : Ω) : ℝ :=
78   ∑ i ∈ Finset.range n, (X i ω-(μ[X i | ℱ i]) ω)
79 
80 /-- Conditional Hoeffding iterates along the actual filtration, without independence. -/
81 theorem predictable_sum_subgaussian (ℱ : Filtration ℕ mΩ) (X : ℕ → Ω → ℝ)
82     (hX : ∀ i, Measurable[ℱ (i+1)] (X i))
83     (hb : ∀ i, ∀ᵐ ω ∂μ, X i ω∈Set.Icc (0:ℝ) 1) (n : ℕ) :
84     HasSubgaussianMGF (centeredSum (μ:=μ) ℱ X n) ((n:NNReal)/4) μ := by
85   induction n with
86   | zero =>
87     simp only [Nat.cast_zero,zero_div]
88     exact HasSubgaussianMGF.fun_zero
89   | succ n ih =>
90     have hsmeas : Measurable[ℱ n] (centeredSum (μ:=μ) ℱ X n) := by
91       apply Finset.measurable_fun_sum
92       intro i hi
93       have hin : i+1≤n := by simpa using Finset.mem_range.mp hi
94       exact ((hX i).mono (ℱ.mono hin) le_rfl).sub
95         (stronglyMeasurable_condExp.measurable.mono (ℱ.mono (by omega)) le_rfl)
96     have hc := conditional_centered_subgaussian (ℱ.le n) (X n)
97       ((hX n).mono (ℱ.le (n+1)) le_rfl) (hb n)
98     have ha := HasSubgaussianMGF.add_of_hasCondSubgaussianMGF (ℱ.le n)
99       (ih.trim (ℱ.le n) hsmeas) hc
100     convert ha using 1
101     · funext ω
102       simp only [centeredSum, Finset.sum_range_succ, Pi.add_apply]
103     · push_cast
104       ring
105 
106 /-- The fixed-time two-sided martingale error, derived from bounded tests. -/
107 theorem predictable_sum_tail (ℱ : Filtration ℕ mΩ) (X : ℕ → Ω → ℝ)
108     (hX : ∀ i, Measurable[ℱ (i+1)] (X i))
109     (hb : ∀ i, ∀ᵐ ω ∂μ, X i ω∈Set.Icc (0:ℝ) 1)
110     {n : ℕ} (hn : 0<n) (b : ℝ) (hbn : 0≤b) :
111     μ.real {ω | b ≤ |centeredSum (μ:=μ) ℱ X n ω|} ≤ 2*exp (-2*b^2/n) := by
112   have hs := predictable_sum_subgaussian ℱ X hX hb n
113   have hu := hs.measure_ge_le hbn
114   have hl := hs.neg.measure_ge_le hbn
115   have hexp : exp (-b^2/(2*((n:NNReal)/4:NNReal)))=exp (-2*b^2/n) := by
116     congr 1
117     push_cast
118     field_simp
119     ring
120   rw [hexp] at hu hl
121   have hevent : {ω | b≤|centeredSum (μ:=μ) ℱ X n ω|} =
122       {ω | b≤centeredSum (μ:=μ) ℱ X n ω} ∪
123       {ω | b≤ -centeredSum (μ:=μ) ℱ X n ω} := by
124     ext ω
125     simp only [Set.mem_ofPred_eq,Set.mem_union,le_abs]
126   rw [hevent]
127   exact (measureReal_union_le _ _).trans (by simpa only [Pi.neg_apply,two_mul] using add_le_add hu hl)
128 
129 /-- The elementary time-union boundary at a positive time. -/
130 noncomputable def boundary (n : ℕ) (α : ℝ) : ℝ :=
131   sqrt ((n:ℝ)/2*log (2*n*(n+1)/α))
132 
133 omit [MeasurableSpace Ω] [StandardBorelSpace Ω] in
134 /-- The declared boundary spends α/[n(n+1)] at time n. -/
135 theorem boundary_budget {n : ℕ} (hn : 0<n) {α : ℝ} (hα : 0<α) (hα1 : α≤1) :
136     2*exp (-2*(boundary n α)^2/n)=α/(n*(n+1)) := by
137   have hn0 : (0:ℝ)<n := by exact_mod_cast hn
138   have hn1 : (1:ℝ)≤n := by exact_mod_cast hn
139   have hr : 0<2*(n:ℝ)*(n+1)/α := by positivity
140   have hr1 : 1≤2*(n:ℝ)*(n+1)/α := (le_div_iff₀ hα).mpr (by nlinarith)
141   have hlog : 0≤log (2*(n:ℝ)*(n+1)/α) := log_nonneg hr1
142   rw [boundary,sq_sqrt (mul_nonneg (by positivity) hlog)]
143   have he : -2*((n:ℝ)/2*log (2*n*(n+1)/α))/n = -log (2*n*(n+1)/α) := by
144     field_simp
145   rw [he,exp_neg,exp_log hr]
146   field_simp
147 
148 omit [MeasurableSpace Ω] [StandardBorelSpace Ω] in
149 /-- Finite telescoping proves the complete time budget. -/
150 theorem time_partial_budget (N : ℕ) :
151     (∑ n ∈ Finset.range N, (1:ℝ)/(((n:ℝ)+1)*(n+2)))=1-1/((N:ℝ)+1) := by
152   induction N with
153   | zero => norm_num
154   | succ N ih =>
155     rw [Finset.sum_range_succ,ih]
156     push_cast
157     field_simp
158     ring
159 
160 noncomputable def timeWeight (n : ℕ) : NNReal := 1/(((n:NNReal)+1)*(n+2))
161 
162 omit [MeasurableSpace Ω] [StandardBorelSpace Ω] in
163 /-- The countable time-union weights have total at most one. -/
164 theorem time_partial_le (N : ℕ) : ∑ n ∈ Finset.range N, timeWeight n ≤ 1 := by
165   have h : (∑ n ∈ Finset.range N, (1:ℝ)/(((n:ℝ)+1)*(n+2)))≤1 := by
166     rw [time_partial_budget]
167     exact sub_le_self _ (by positivity)
168   apply NNReal.coe_le_coe.mp
169   simpa [timeWeight] using h
170 
171 omit [MeasurableSpace Ω] [StandardBorelSpace Ω] in
172 theorem time_summable : Summable timeWeight :=
173   NNReal.summable_of_sum_range_le time_partial_le
174 
175 omit [MeasurableSpace Ω] [StandardBorelSpace Ω] in
176 theorem time_budget : ∑' n, timeWeight n ≤ 1 :=
177   NNReal.tsum_le_of_sum_range_le time_partial_le
178 
179 omit [StandardBorelSpace Ω] [IsProbabilityMeasure μ] in
180 /-- Each finite accumulated conditional residual is measurable. -/
181 theorem centeredSum_measurable (ℱ : Filtration ℕ mΩ) (X : ℕ → Ω → ℝ)
182     (hX : ∀ i, Measurable[ℱ (i+1)] (X i)) (n : ℕ) :
183     Measurable (centeredSum (μ:=μ) ℱ X n) := by
184   apply Finset.measurable_fun_sum
185   intro i _
186   exact ((hX i).mono (ℱ.le (i+1)) le_rfl).sub
187     (stronglyMeasurable_condExp.measurable.mono (ℱ.le i) le_rfl)
188 
189 /-- One predictable rule has the declared simultaneous boundary at every positive time. -/
190 theorem time_uniform_one (ℱ : Filtration ℕ mΩ) (X : ℕ → Ω → ℝ)
191     (hX : ∀ i, Measurable[ℱ (i+1)] (X i))
192     (hb : ∀ i, ∀ᵐ ω ∂μ, X i ω∈Set.Icc (0:ℝ) 1)
193     (α : NNReal) (hα : 0<α) (hα1 : α≤1) :
194     1-(α:ℝ) ≤ μ.real {ω | ∀ n, |centeredSum (μ:=μ) ℱ X (n+1) ω|≤boundary (n+1) α} := by
195   let F : ℕ → Set Ω := fun n ↦ {ω | boundary (n+1) α < |centeredSum (μ:=μ) ℱ X (n+1) ω|}
196   have hF : ∀ n, MeasurableSet (F n) := by
197     intro n
198     apply measurableSet_lt measurable_const
199     exact (centeredSum_measurable ℱ X hX (n+1)).norm
200   have hweights : Summable (fun n ↦ α*timeWeight n) := time_summable.mul_left α
201   have hbudget : ∑' n, α*timeWeight n ≤ α := by
202     rw [tsum_mul_left]
203     simpa using mul_le_mul_of_nonneg_left time_budget α.coe_nonneg
204   have hf : ∀ n, μ.real (F n) ≤ (α*timeWeight n:NNReal) := by
205     intro n
206     have ht := predictable_sum_tail ℱ X hX hb (by omega : 0<n+1)
207       (boundary (n+1) α) (sqrt_nonneg _)
208     rw [boundary_budget (by omega) (by exact_mod_cast hα) (by exact_mod_cast hα1)] at ht
209     apply (measureReal_mono (by
210       intro ω h
211       exact (show boundary (n+1) α < |centeredSum (μ:=μ) ℱ X (n+1) ω| from h).le)).trans
212       (ht.trans_eq ?_)
213     simp only [timeWeight,NNReal.coe_mul,NNReal.coe_div,NNReal.coe_one,NNReal.coe_add,NNReal.coe_natCast]
214     push_cast
215     field_simp
216     ring
217   have hprob := SequentialConfidence.simultaneous_coverage F hF
218     (fun n ↦ α*timeWeight n) hweights α hbudget hf
219   convert hprob using 1
220   congr 1
221   ext ω
222   simp [F]
223 
224 /-- All prospectively registered countably many rules share one all-time event. -/
225 theorem time_uniform_rules (ℱ : Filtration ℕ mΩ) (X : ℕ → ℕ → Ω → ℝ)
226     (hX : ∀ j i, Measurable[ℱ (i+1)] (X j i))
227     (hb : ∀ j i, ∀ᵐ ω ∂μ, X j i ω∈Set.Icc (0:ℝ) 1)
228     (α : ℕ → NNReal) (hα : ∀ j, 0<α j) (hs : Summable α)
229     (δ : NNReal) (hbudget : ∑' j, α j ≤ δ) (hδ1 : δ≤1) :
230     1-(δ:ℝ) ≤ μ.real {ω | ∀ j n,
231       |centeredSum (μ:=μ) ℱ (X j) (n+1) ω|≤boundary (n+1) (α j)} := by
232   let F : ℕ → Set Ω := fun j ↦ {ω | ∃ n,
233     boundary (n+1) (α j) < |centeredSum (μ:=μ) ℱ (X j) (n+1) ω|}
234   have hF : ∀ j, MeasurableSet (F j) := by
235     intro j
236     simp only [F,Set.ofPred_exists]
237     apply MeasurableSet.iUnion
238     intro n
239     apply measurableSet_lt measurable_const
240     exact (centeredSum_measurable ℱ (X j) (hX j) (n+1)).norm
241   have hf : ∀ j, μ.real (F j)≤(α j:ℝ) := by
242     intro j
243     have hj : α j≤1 := (hs.le_tsum j (fun _ _ ↦ by positivity)).trans (hbudget.trans hδ1)
244     have ht := time_uniform_one ℱ (X j) (hX j) (hb j) (α j) (hα j) hj
245     have he : {ω | ∀ n, |centeredSum (μ:=μ) ℱ (X j) (n+1) ω|≤boundary (n+1) (α j)} =
246         (F j)ᶜ := by ext ω; simp [F]
247     rw [he,measureReal_compl (hF j)] at ht
248     simp only [probReal_univ] at ht
249     linarith
250   have hprob := SequentialConfidence.simultaneous_coverage F hF α hs δ hbudget hf
251   convert hprob using 1
252   congr 1
253   ext ω
254   simp [F]
255 
256 /-- Accumulated observed residual against a possibly changing model prediction. -/
257 noncomputable def observedResidual (X p : ℕ → Ω → ℝ) (n : ℕ) (ω : Ω) : ℝ :=
258   ∑ i ∈ Finset.range n, (X i ω-p i ω)
259 
260 /-- Accumulated true conditional predictive drift. -/
261 noncomputable def conditionalDrift (ℱ : Filtration ℕ mΩ) (X p : ℕ → Ω → ℝ)
262     (n : ℕ) (ω : Ω) : ℝ := ∑ i ∈ Finset.range n, ((μ[X i | ℱ i]) ω-p i ω)
263 
264 omit [StandardBorelSpace Ω] [IsProbabilityMeasure μ] in
265 /-- Model predictions cancel exactly, so no independence of prediction errors is used. -/
266 theorem residual_sub_drift (ℱ : Filtration ℕ mΩ) (X p : ℕ → Ω → ℝ) (n : ℕ) (ω : Ω) :
267     observedResidual X p n ω-conditionalDrift (μ:=μ) ℱ X p n ω =
268       centeredSum (μ:=μ) ℱ X n ω := by
269   simp only [observedResidual,conditionalDrift,centeredSum,← Finset.sum_sub_distrib]
270   apply Finset.sum_congr rfl
271   intro i _
272   ring
273 
274 /-- P66's residual/drift conclusion in the bounded, standard Borel sector. -/
275 theorem predictable_residual_certificate (ℱ : Filtration ℕ mΩ)
276     (X p : ℕ → ℕ → Ω → ℝ)
277     (hX : ∀ j i, Measurable[ℱ (i+1)] (X j i))
278     (hb : ∀ j i, ∀ᵐ ω ∂μ, X j i ω∈Set.Icc (0:ℝ) 1)
279     (α : ℕ → NNReal) (hα : ∀ j, 0<α j) (hs : Summable α)
280     (δ : NNReal) (hbudget : ∑' j, α j ≤ δ) (hδ1 : δ≤1) :
281     1-(δ:ℝ) ≤ μ.real {ω | ∀ j n,
282       |observedResidual (X j) (p j) (n+1) ω-
283         conditionalDrift (μ:=μ) ℱ (X j) (p j) (n+1) ω|≤boundary (n+1) (α j)} := by
284   simpa only [residual_sub_drift] using time_uniform_rules ℱ X hX hb α hα hs δ hbudget hδ1
285 
286 omit [MeasurableSpace Ω] [StandardBorelSpace Ω] in
287 /-- A simultaneous event survives every selected time and rule, and scalar range scaling. -/
288 theorem scaled_selected_bound (S : ℕ → ℕ → Ω → ℝ) (α : ℕ → NNReal)
289     (ω : Ω) (hall : ∀ j n, |S j (n+1) ω|≤boundary (n+1) (α j))
290     (c : ℝ) (hc : 0≤c) (time rule : Ω → ℕ) :
291     |c*S (rule ω) (time ω+1) ω|≤c*boundary (time ω+1) (α (rule ω)) := by
292   rw [abs_mul,abs_of_nonneg hc]
293   exact mul_le_mul_of_nonneg_left (hall (rule ω) (time ω)) hc
294 
295 end Komorebi.LSM.PredictableResidual

Back to source controls