measure_ge_le_exp_cgf — Mathlib

English

For finite μ and t ≥ 0, the upper tail bound can be expressed as a bound with the cumulant generating function: μ({ε ≤ X}) ≤ exp(-tε + cgf(X; μ; t)).

Русский

Для конечной меры μ и t ≥ 0 верхняя граница хвоста выражается через к CGF: μ({ε ≤ X}) ≤ exp(-tε + cgf(X; μ; t)).

LaTeX

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

Lean4

/-- **Chernoff bound** on the upper tail of a real random variable. -/
theorem measure_ge_le_exp_cgf [IsFiniteMeasure μ] (ε : ℝ) (ht : 0 ≤ t) (h_int : Integrable (fun ω => exp (t * X ω)) μ) :
    μ.real {ω | ε ≤ X ω} ≤ exp (-t * ε + cgf X μ t) :=
  by
  refine (measure_ge_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

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