Theorems · Theorem · probability
ProbabilityTheory.measure_le_le_exp_cgf
∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ}
[MeasureTheory.IsFiniteMeasure μ] (ε : ℝ),
t ≤ 0 →
MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ →
μ.real {ω | X ω ≤ ε} ≤ Real.exp (-t * ε + ProbabilityTheory.cgf X μ t)Chernoff bound on the lower tail of a real random variable.
- Defined in
- Mathlib.Probability.Moments.Basic
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 259 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites19
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- Set.ofPredstatement · cited by 6,101
- LE.le.transproof · cited by 3,151
- LT.lt.leproof · cited by 2,189
- le_rflproof · cited by 1,558
- MeasureTheory.Integrablestatement and proof · cited by 1,367
- MeasureTheory.IsFiniteMeasurestatement and proof · cited by 1,078
- Real.expstatement and proof · cited by 871
- MeasureTheory.Measure.realstatement · cited by 530
- Real.exp_posproof · cited by 169
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.