LeanMachineLearning exposition

ProbabilityTheory.HasSubgaussianMGF.measure_le_le🔗

Minimal Lean file

measure_le_le🔗

LemmaProbabilityTheory.HasSubgaussianMGF.measure_le_le
Details

Chernoff bound on the left tail of a sub-Gaussian random variable.

🔗theorem
ProbabilityTheory.HasSubgaussianMGF.measure_le_le.{u_1} {Ω : Type u_1}
  {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ}
  {c : NNReal} (h : HasSubgaussianMGF X c μ) {ε : ℝ} (hε : 0 ≤ ε) :
  MeasureTheory.Measure.real μ {ω | X ω ≤ -ε} ≤
    Real.exp (-ε ^ 2 / (2 * ↑c))
ProbabilityTheory.HasSubgaussianMGF.measure_le_le.{u_1}
  {Ω : Type u_1} {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω}
  {X : Ω → ℝ} {c : NNReal}
  (h : HasSubgaussianMGF X c μ) {ε : ℝ}
  (hε : 0 ≤ ε) :
  MeasureTheory.Measure.real μ
      {ω | X ω ≤ -ε} ≤
    Real.exp (-ε ^ 2 / (2 * ↑c))

Code

lemma measure_le_le (h : HasSubgaussianMGF X c μ) {ε : ℝ} (hε : 0 ≤ ε) :
    μ.real {ω | X ω ≤ -ε} ≤ exp (-ε ^ 2 / (2 * c))

Actions: Source · Open Issue

Proof
by
  simp_rw [le_neg (b := ε), ← Pi.neg_apply]
  exact h.neg.measure_ge_le hε