English
For finite μ and t ≥ 0, the probability that X exceeds ε is bounded by exp(-tε) times the mgf at t.
Русский
Для конечной меры μ и t ≥ 0 вероятность того, что X превышает ε, не выше exp(-tε) · mgf(X; μ; t).
LaTeX
$$$\mu(\{\omega : ε \le X(\omega)\}) \le e^{-t\,ε} \cdot \mathrm{mgf}(X, μ, t).$$$
Lean4
/-- **Chernoff bound** on the upper tail of a real random variable. -/
theorem measure_ge_le_exp_mul_mgf [IsFiniteMeasure μ] (ε : ℝ) (ht : 0 ≤ t)
(h_int : Integrable (fun ω => exp (t * X ω)) μ) : μ.real {ω | ε ≤ X ω} ≤ exp (-t * ε) * mgf X μ t :=
by
rcases ht.eq_or_lt with ht_zero_eq | ht_pos
· rw [ht_zero_eq.symm]
simp only [neg_zero, zero_mul, exp_zero, mgf_zero', one_mul]
gcongr
exacts [measure_ne_top _ _, Set.subset_univ _]
calc
μ.real {ω | ε ≤ X ω} = μ.real {ω | exp (t * ε) ≤ exp (t * X ω)} :=
by
congr 1 with ω
simp only [Set.mem_setOf_eq, exp_le_exp]
exact ⟨fun h => mul_le_mul_of_nonneg_left h ht_pos.le, fun h => le_of_mul_le_mul_left h ht_pos⟩
_ ≤ (exp (t * ε))⁻¹ * μ[fun ω => exp (t * X ω)] :=
by
have : exp (t * ε) * μ.real {ω | exp (t * ε) ≤ exp (t * X ω)} ≤ μ[fun ω => exp (t * X ω)] :=
mul_meas_ge_le_integral_of_nonneg (ae_of_all _ fun x => (exp_pos _).le) h_int _
rwa [mul_comm (exp (t * ε))⁻¹, ← div_eq_mul_inv, le_div_iff₀' (exp_pos _)]
_ = exp (-t * ε) * mgf X μ t := by rw [neg_mul, exp_neg]; rfl
