ConditionalBernoulli.lean

1 import Mathlib.Probability.Moments.SubGaussian
2 import Mathlib.Probability.Distributions.Bernoulli
3 import Mathlib.Analysis.Convex.SpecificFunctions.Basic
4 import Mathlib.Tactic
5 
6 /-! Scalar exponential bounds used for a conditional Hoeffding argument.
7 The auxiliary Bernoulli measure is explicit and finite; no conditional law on
8 the sample space is assumed. -/
9 set_option autoImplicit false
10 namespace Komorebi.LSM.ConditionalBernoulli
11 open MeasureTheory ProbabilityTheory Real
12 
13 /-- The secant bound for the exponential holds for either sign of θ. -/
14 theorem exp_secant (θ x : ℝ) (hx : x∈Set.Icc (0:ℝ) 1) :
15     exp (θ*x)≤(1-x)+x*exp θ := by
16   have h := convexOn_exp.2 (Set.mem_univ (0:ℝ)) (Set.mem_univ θ)
17     (sub_nonneg.mpr hx.2) hx.1 (by ring : (1-x)+x=1)
18   have he : (1-x) • (0:ℝ)+x • θ=θ*x := by simp [smul_eq_mul,mul_comm]
19   rw [he] at h
20   simpa only [smul_eq_mul,exp_zero,mul_one] using h
21 
22 /-- The exact centered Bernoulli exponential envelope, proved from the
23 ordinary Hoeffding theorem on an actual two-point probability measure. -/
24 theorem centered_bernoulli_bound (θ p : ℝ) (hp : p∈Set.Icc (0:ℝ) 1) :
25     exp (-θ*p)*((1-p)+p*exp θ)≤exp (θ^2/8) := by
26   let ν : Measure Bool := bernoulliMeasure true false ⟨p,hp⟩
27   let X : Bool → ℝ := fun b => if b then 1 else 0
28   have hX : Measurable X := measurable_of_countable X
29   have hb : ∀ᵐ b∂ν,X b∈Set.Icc (0:ℝ) 1 := by
30     exact Filter.Eventually.of_forall (fun b => by cases b <;> norm_num [X])
31   have hm : (∫ b,X b∂ν)=p := by
32     change (∫ b,X b∂bernoulliMeasure true false ⟨p,hp⟩)=p
33     rw [integral_bernoulliMeasure]
34     simp [X,smul_eq_mul]
35   have hs := (hasSubgaussianMGF_of_mem_Icc (μ := ν) hX.aemeasurable hb).mgf_le θ
36   rw [hm] at hs
37   have hformula : mgf (fun b => X b-p) ν θ=
38       p*exp (θ*(1-p))+(1-p)*exp (θ*(0-p)) := by
39     change (∫ b,exp (θ*(X b-p))∂bernoulliMeasure true false ⟨p,hp⟩)=_
40     rw [integral_bernoulliMeasure]
41     simp [X,smul_eq_mul]
42   rw [hformula] at hs
43   have hconst : (((‖(1:ℝ)-0‖₊/2)^2 : NNReal):ℝ)=(1:ℝ)/4 := by norm_num
44   have hparam : (1/4:ℝ)*θ^2/2=θ^2/8 := by ring
45   rw [hconst,hparam] at hs
46   calc
47     _ = p*exp (θ*(1-p))+(1-p)*exp (θ*(0-p)) := by
48       rw [show θ*(1-p)=θ+(-θ*p) by ring,exp_add,
49         show θ*(0-p)=-θ*p by ring]
50       ring
51     _ ≤ _ := hs
52 
53 end Komorebi.LSM.ConditionalBernoulli

Back to source controls