measure_le_le_exp_cgf — Mathlib

English

For finite μ and t ≤ 0, the lower tail bound is μ({X ≤ ε}) ≤ exp(-tε + cgf(X; μ; t)).

Русский

Для конечной меры μ и t ≤ 0, μ({X ≤ ε}) ≤ exp(-tε + cgf(X; μ; t)).

LaTeX

$$$\mu(\{ω : X(ω) \le ε\}) \le \exp(-tε + \mathrm{cgf}(X, μ, t)).$$$

Lean4

/-- **Chernoff bound** on the lower tail of a real random variable. -/
theorem measure_le_le_exp_cgf [IsFiniteMeasure μ] (ε : ℝ) (ht : t ≤ 0) (h_int : Integrable (fun ω => exp (t * X ω)) μ) :
    μ.real {ω | X ω ≤ ε} ≤ exp (-t * ε + cgf X μ t) :=
  by
  refine (measure_le_le_exp_mul_mgf ε ht h_int).trans ?_
  rw [exp_add]
  exact mul_le_mul le_rfl (le_exp_log _) mgf_nonneg (exp_pos _).le

Похожие утверждения