measure_le_le_exp_mul_mgf — Mathlib

English

For finite μ and t ≤ 0, the probability that X is below ε is bounded by exp(-tε) times the mgf at t.

Русский

Для конечной меры μ и t ≤ 0 вероятность того, что X ≤ ε, не выше exp(-tε) · mgf(X; μ; t).

LaTeX

$$$\mu(\{\omega : X(\omega) \le ε\}) \le e^{-tε} \cdot \mathrm{mgf}(X, μ, t).$$$

Lean4

/-- **Chernoff bound** on the lower tail of a real random variable. -/
theorem measure_le_le_exp_mul_mgf [IsFiniteMeasure μ] (ε : ℝ) (ht : t ≤ 0)
    (h_int : Integrable (fun ω => exp (t * X ω)) μ) : μ.real {ω | X ω ≤ ε} ≤ exp (-t * ε) * mgf X μ t :=
  by
  rw [← neg_neg t, ← mgf_neg, neg_neg, ← neg_mul_neg (-t)]
  refine Eq.trans_le ?_ (measure_ge_le_exp_mul_mgf (-ε) (neg_nonneg.mpr ht) ?_)
  · simp only [Pi.neg_apply, neg_le_neg_iff]
  · simp_rw [Pi.neg_apply, neg_mul_neg]
    exact h_int

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