ConditionalHoeffding.lean

1 import KomorebiLSM.PredictableResidual
2 import KomorebiLSM.ConditionalBernoulli
3 import Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
4 
5 /-! Sharp conditional Hoeffding bounds from ordinary conditional expectations.
6 No conditional-distribution kernel or Standard Borel sample space is used. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM.ConditionalHoeffding
9 open MeasureTheory ProbabilityTheory Real
10 open scoped BigOperators NNReal
11 variable {Ω : Type*} [mΩ : MeasurableSpace Ω]
12 variable {μ : Measure Ω} [IsProbabilityMeasure μ]
13 
14 /-- The bounded test's actual centered exponential is integrable. -/
15 theorem centered_exp_integrable {m : MeasurableSpace Ω} (hm : m≤mΩ)
16     (X : Ω → ℝ) (hX : @Measurable Ω ℝ mΩ _ X) (hb : ∀ᵐ ω∂μ,X ω∈Set.Icc (0:ℝ) 1)
17     (θ : ℝ) : Integrable (fun ω => exp (θ*(X ω-(μ[X|m]) ω))) μ := by
18   let : MeasurableSpace Ω := mΩ
19   have hmean := PredictableResidual.conditional_mean_mem_Icc hm X hX hb
20   have hres : ∀ᵐ ω∂μ,X ω-(μ[X|m]) ω∈Set.Icc (-1:ℝ) 1 := by
21     filter_upwards [hb,hmean] with ω h h' using ⟨by linarith [h.1,h'.2],by linarith [h.2,h'.1]⟩
22   exact integrable_exp_mul_of_mem_Icc
23     ((hX.sub (stronglyMeasurable_condExp.measurable.mono hm le_rfl)).aemeasurable) hres
24 
25 /-- The actual conditional centered MGF is bounded on an arbitrary probability
26 space. The real parameter is fixed before the almost-everywhere conclusion. -/
27 theorem centered_condExp_le {m : MeasurableSpace Ω} (hm : m≤mΩ)
28     (X : Ω → ℝ) (hX : @Measurable Ω ℝ mΩ _ X) (hb : ∀ᵐ ω∂μ,X ω∈Set.Icc (0:ℝ) 1)
29     (θ : ℝ) :
30     (μ[fun ω => exp (θ*(X ω-(μ[X|m]) ω))|m])≤ᵐ[μ] fun _ => exp (θ^2/8) := by
31   let : MeasurableSpace Ω := mΩ
32   let M : Ω → ℝ := μ[X|m]
33   have hi : Integrable X μ := Integrable.of_mem_Icc (0:ℝ) 1 hX.aemeasurable hb
34   have hmean : ∀ᵐ ω∂μ,M ω∈Set.Icc (0:ℝ) 1 :=
35     PredictableResidual.conditional_mean_mem_Icc hm X hX hb
36   have hexp : Integrable (fun ω => exp (θ*X ω)) μ :=
37     integrable_exp_mul_of_mem_Icc hX.aemeasurable hb
38   have haff : Integrable (fun ω => (exp θ-1)*X ω+1) μ :=
39     (hi.const_mul (exp θ-1)).add (integrable_const 1)
40   have hsec : (fun ω => exp (θ*X ω))≤ᵐ[μ] fun ω => (exp θ-1)*X ω+1 := by
41     filter_upwards [hb] with ω hω
42     have he := ConditionalBernoulli.exp_secant θ (X ω) hω
43     nlinarith
44   have hmono := condExp_mono (m := m) hexp haff hsec
45   have haf : (fun ω => (exp θ-1)*M ω+1)=ᵐ[μ]
46       μ[fun ω => (exp θ-1)*X ω+1|m] := by
47     simpa only [smul_apply,ContinuousLinearMap.id_apply,smul_eq_mul] using
48       (ContinuousLinearMap.comp_condExp_add_const_comm hm hi
49         ((exp θ-1) • ContinuousLinearMap.id ℝ ℝ) (1:ℝ))
50   have hsm : StronglyMeasurable[m] (fun ω => exp (-θ*M ω)) :=
51     continuous_exp.comp_stronglyMeasurable (stronglyMeasurable_const.mul stronglyMeasurable_condExp)
52   have hbound : ∀ᵐ ω∂μ,‖exp (-θ*M ω)‖≤exp |θ| := by
53     filter_upwards [hmean] with ω hω
54     rw [Real.norm_eq_abs,abs_of_pos (exp_pos _)]
55     apply exp_le_exp.mpr
56     calc
57       -θ*M ω ≤ |-θ*M ω| := le_abs_self _
58       _ = |θ| * |M ω| := by rw [abs_mul,abs_neg]
59       _ ≤ |θ| *1 := mul_le_mul_of_nonneg_left (by simpa only [abs_of_nonneg hω.1] using hω.2) (abs_nonneg _)
60       _ = _ := mul_one _
61   have hpull := condExp_stronglyMeasurable_mul_of_bound hm hsm hexp (exp |θ|) hbound
62   have heq : (fun ω => exp (θ*(X ω-M ω)))=
63       (fun ω => exp (-θ*M ω))*(fun ω => exp (θ*X ω)) := by
64     funext ω
65     rw [Pi.mul_apply,← exp_add]
66     congr 1
67     ring
68   change (μ[fun ω => exp (θ*(X ω-M ω))|m])≤ᵐ[μ] fun _ => exp (θ^2/8)
69   rw [heq]
70   filter_upwards [hpull,hmono,haf,hmean] with ω hp hm' ha hM
71   simp only [Pi.mul_apply] at hp
72   calc
73     _ = exp (-θ*M ω)*(μ[fun ω => exp (θ*X ω)|m]) ω := hp
74     _ ≤ exp (-θ*M ω)*((exp θ-1)*M ω+1) :=
75       mul_le_mul_of_nonneg_left (hm'.trans_eq ha.symm) (exp_pos _).le
76     _ = exp (-θ*M ω)*((1-M ω)+M ω*exp θ) := by ring
77     _ ≤ _ := ConditionalBernoulli.centered_bernoulli_bound θ (M ω) hM
78 
79 end Komorebi.LSM.ConditionalHoeffding

Back to source controls