PredictableResidualGeneral.lean

1 import KomorebiLSM.ConditionalHoeffding
2 import KomorebiLSM.CountableConfidence
3 
4 /-! P66 without a topological assumption on the sample space. Conditional
5 exponentials and their filtration iteration are derived from actual bounded
6 adapted tests and ordinary conditional expectation. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM.PredictableResidualGeneral
9 open MeasureTheory ProbabilityTheory Real PredictableResidual
10 open scoped BigOperators NNReal ENNReal
11 variable {Ω : Type*} [mΩ : MeasurableSpace Ω]
12 variable {μ : Measure Ω} [IsProbabilityMeasure μ]
13 
14 /-- A unit-range test minus its actual conditional mean lies in [-1,1]. -/
15 theorem increment_mem_Icc (ℱ : Filtration ℕ mΩ) (X : ℕ → Ω → ℝ)
16     (hX : ∀ i,Measurable[ℱ (i+1)] (X i))
17     (hb : ∀ i,∀ᵐ ω∂μ,X i ω∈Set.Icc (0:ℝ) 1) (i : ℕ) :
18     ∀ᵐ ω∂μ,X i ω-(μ[X i|ℱ i]) ω∈Set.Icc (-1:ℝ) 1 := by
19   have hm := conditional_mean_mem_Icc (ℱ.le i) (X i)
20     ((hX i).mono (ℱ.le (i+1)) le_rfl) (hb i)
21   filter_upwards [hb i,hm] with ω h h' using ⟨by linarith [h.1,h'.2],by linarith [h.2,h'.1]⟩
22 
23 /-- Every finite centered sum has an actual bounded range. -/
24 theorem sum_mem_Icc (ℱ : Filtration ℕ mΩ) (X : ℕ → Ω → ℝ)
25     (hX : ∀ i,Measurable[ℱ (i+1)] (X i))
26     (hb : ∀ i,∀ᵐ ω∂μ,X i ω∈Set.Icc (0:ℝ) 1) : (n : ℕ) →
27     ∀ᵐ ω∂μ,centeredSum (μ:=μ) ℱ X n ω∈Set.Icc (-(n:ℝ)) n
28   | 0 => by simp [centeredSum]
29   | n+1 => by
30     filter_upwards [sum_mem_Icc ℱ X hX hb n,increment_mem_Icc ℱ X hX hb n] with ω hs hi
31     have he : centeredSum (μ:=μ) ℱ X (n+1) ω=
32         centeredSum (μ:=μ) ℱ X n ω+(X n ω-(μ[X n|ℱ n]) ω) := by
33       simp only [centeredSum,Finset.sum_range_succ]
34     rw [he]
35     constructor <;> push_cast <;> linarith [hs.1,hs.2,hi.1,hi.2]
36 
37 omit [IsProbabilityMeasure μ] in
38 /-- The previous centered sum is measurable before the next test. -/
39 theorem sum_adapted (ℱ : Filtration ℕ mΩ) (X : ℕ → Ω → ℝ)
40     (hX : ∀ i,Measurable[ℱ (i+1)] (X i)) (n : ℕ) :
41     Measurable[ℱ n] (centeredSum (μ:=μ) ℱ X n) := by
42   apply Finset.measurable_fun_sum
43   intro i hi
44   have hin : i+1≤n := by simpa using Finset.mem_range.mp hi
45   exact ((hX i).mono (ℱ.mono hin) le_rfl).sub
46     (stronglyMeasurable_condExp.measurable.mono (ℱ.mono (by omega)) le_rfl)
47 
48 theorem sum_exp_integrable (ℱ : Filtration ℕ mΩ) (X : ℕ → Ω → ℝ)
49     (hX : ∀ i,Measurable[ℱ (i+1)] (X i))
50     (hb : ∀ i,∀ᵐ ω∂μ,X i ω∈Set.Icc (0:ℝ) 1) (n : ℕ) (θ : ℝ) :
51     Integrable (fun ω => exp (θ*centeredSum (μ:=μ) ℱ X n ω)) μ :=
52   integrable_exp_mul_of_mem_Icc (centeredSum_measurable ℱ X hX n).aemeasurable
53     (sum_mem_Icc ℱ X hX hb n)
54 
55 /-- Direct total-expectation iteration of the true conditional exponential
56 bound, with no independence or conditional-distribution construction. -/
57 theorem sum_exp_bound (ℱ : Filtration ℕ mΩ) (X : ℕ → Ω → ℝ)
58     (hX : ∀ i,Measurable[ℱ (i+1)] (X i))
59     (hb : ∀ i,∀ᵐ ω∂μ,X i ω∈Set.Icc (0:ℝ) 1) (θ : ℝ) : (n : ℕ) →
60     (∫ ω,exp (θ*centeredSum (μ:=μ) ℱ X n ω)∂μ)≤exp ((n:ℝ)*θ^2/8)
61   | 0 => by simp [centeredSum]
62   | n+1 => by
63     let S : Ω → ℝ := centeredSum (μ:=μ) ℱ X n
64     let Y : Ω → ℝ := fun ω => X n ω-(μ[X n|ℱ n]) ω
65     have hF : StronglyMeasurable[ℱ n] (fun ω => exp (θ*S ω)) :=
66       continuous_exp.comp_stronglyMeasurable
67         (stronglyMeasurable_const.mul (sum_adapted ℱ X hX n).stronglyMeasurable)
68     have hFbound : ∀ᵐ ω∂μ,‖exp (θ*S ω)‖≤exp (|θ| *(n:ℝ)) := by
69       filter_upwards [sum_mem_Icc ℱ X hX hb n] with ω hs
70       rw [Real.norm_eq_abs,abs_of_pos (exp_pos _)]
71       apply exp_le_exp.mpr
72       calc
73         θ*S ω ≤ |θ*S ω| := le_abs_self _
74         _ = |θ| * |S ω| := abs_mul _ _
75         _ ≤ |θ| *(n:ℝ) := mul_le_mul_of_nonneg_left (abs_le.mpr hs) (abs_nonneg _)
76     have hYint : Integrable (fun ω => exp (θ*Y ω)) μ :=
77       ConditionalHoeffding.centered_exp_integrable (ℱ.le n) (X n)
78         ((hX n).mono (ℱ.le (n+1)) le_rfl) (hb n) θ
79     have hYmgf := ConditionalHoeffding.centered_condExp_le (ℱ.le n) (X n)
80       ((hX n).mono (ℱ.le (n+1)) le_rfl) (hb n) θ
81     have hpull := condExp_stronglyMeasurable_mul_of_bound (ℱ.le n) hF hYint
82       (exp (|θ| *(n:ℝ))) hFbound
83     have hstep : μ[(fun ω => exp (θ*S ω))*(fun ω => exp (θ*Y ω))|ℱ n]≤ᵐ[μ]
84         fun ω => exp (θ*S ω)*exp (θ^2/8) := by
85       filter_upwards [hpull,hYmgf] with ω hp hy
86       simp only [Pi.mul_apply] at hp
87       exact hp.le.trans (mul_le_mul_of_nonneg_left hy (exp_pos _).le)
88     have hi := integral_mono_ae (integrable_condExp :
89         Integrable (μ[(fun ω => exp (θ*S ω))*(fun ω => exp (θ*Y ω))|ℱ n]) μ)
90       ((sum_exp_integrable ℱ X hX hb n θ).mul_const (exp (θ^2/8))) hstep
91     rw [integral_condExp (ℱ.le n)] at hi
92     have heq : (fun ω => exp (θ*centeredSum (μ:=μ) ℱ X (n+1) ω))=
93         (fun ω => exp (θ*S ω))*(fun ω => exp (θ*Y ω)) := by
94       funext ω
95       simp only [S,Y,centeredSum,Finset.sum_range_succ,Pi.mul_apply,mul_add,exp_add]
96     calc
97       _ = ∫ ω,((fun ω => exp (θ*S ω))*(fun ω => exp (θ*Y ω))) ω∂μ := by rw [heq]
98       _ ≤ (∫ ω,exp (θ*S ω)∂μ)*exp (θ^2/8) := by simpa only [integral_mul_const] using hi
99       _ ≤ exp ((n:ℝ)*θ^2/8)*exp (θ^2/8) :=
100         mul_le_mul_of_nonneg_right (sum_exp_bound ℱ X hX hb θ n) (exp_pos _).le
101       _ = _ := by rw [← exp_add];congr 1;push_cast;ring
102 
103 /-- The usual ordinary subgaussian MGF is derived from the direct filtration
104 proof and is available on every probability sample space. -/
105 theorem predictable_sum_subgaussian (ℱ : Filtration ℕ mΩ) (X : ℕ → Ω → ℝ)
106     (hX : ∀ i,Measurable[ℱ (i+1)] (X i))
107     (hb : ∀ i,∀ᵐ ω∂μ,X i ω∈Set.Icc (0:ℝ) 1) (n : ℕ) :
108     HasSubgaussianMGF (centeredSum (μ:=μ) ℱ X n) ((n:NNReal)/4) μ where
109   integrable_exp_mul := sum_exp_integrable ℱ X hX hb n
110   mgf_le θ := by
111     have he : (((n:NNReal)/4:NNReal):ℝ)*θ^2/2=(n:ℝ)*θ^2/8 := by
112       push_cast
113       ring
114     change (∫ ω,exp (θ*centeredSum (μ:=μ) ℱ X n ω)∂μ)≤
115       exp ((((n:NNReal)/4:NNReal):ℝ)*θ^2/2)
116     rw [he]
117     exact sum_exp_bound ℱ X hX hb θ n
118 
119 /-- The sharp fixed-time two-sided bound now has no Standard Borel hypothesis. -/
120 theorem predictable_sum_tail (ℱ : Filtration ℕ mΩ) (X : ℕ → Ω → ℝ)
121     (hX : ∀ i,Measurable[ℱ (i+1)] (X i))
122     (hb : ∀ i,∀ᵐ ω∂μ,X i ω∈Set.Icc (0:ℝ) 1)
123     {n : ℕ} (hn : 0<n) (b : ℝ) (hbn : 0≤b) :
124     μ.real {ω | b≤|centeredSum (μ:=μ) ℱ X n ω|}≤2*exp (-2*b^2/n) := by
125   have hs := predictable_sum_subgaussian ℱ X hX hb n
126   have hu := hs.measure_ge_le hbn
127   have hl := hs.neg.measure_ge_le hbn
128   have hexp : exp (-b^2/(2*((n:NNReal)/4:NNReal)))=exp (-2*b^2/n) := by
129     congr 1
130     push_cast
131     field_simp
132     ring
133   rw [hexp] at hu hl
134   have hevent : {ω | b≤|centeredSum (μ:=μ) ℱ X n ω|}=
135       {ω | b≤centeredSum (μ:=μ) ℱ X n ω}∪{ω | b≤ -centeredSum (μ:=μ) ℱ X n ω} := by
136     ext ω
137     simp only [Set.mem_ofPred_eq,Set.mem_union,le_abs]
138   rw [hevent]
139   exact (measureReal_union_le _ _).trans
140     (by simpa only [Pi.neg_apply,two_mul] using add_le_add hu hl)
141 
142 end Komorebi.LSM.PredictableResidualGeneral

Back to source controls