From 1cc9f3628ea90b5146e3703c2c697dabdbc77a58 Mon Sep 17 00:00:00 2001 From: Jeremy Tan Jie Rui Date: Wed, 21 Jun 2023 09:25:40 +0000 Subject: [PATCH] feat: port Probability.Moments (#5338) This PR completes the port of the **entire** `Probability` folder to mathlib4. --- Mathlib.lean | 1 + Mathlib/Probability/Moments.lean | 386 +++++++++++++++++++++++++++++++ 2 files changed, 387 insertions(+) create mode 100644 Mathlib/Probability/Moments.lean diff --git a/Mathlib.lean b/Mathlib.lean index b7767f475cbfba..f2e0ff0e76a057 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2476,6 +2476,7 @@ import Mathlib.Probability.Martingale.Convergence import Mathlib.Probability.Martingale.OptionalSampling import Mathlib.Probability.Martingale.OptionalStopping import Mathlib.Probability.Martingale.Upcrossing +import Mathlib.Probability.Moments import Mathlib.Probability.Notation import Mathlib.Probability.ProbabilityMassFunction.Basic import Mathlib.Probability.ProbabilityMassFunction.Constructions diff --git a/Mathlib/Probability/Moments.lean b/Mathlib/Probability/Moments.lean new file mode 100644 index 00000000000000..7b2420d66abfad --- /dev/null +++ b/Mathlib/Probability/Moments.lean @@ -0,0 +1,386 @@ +/- +Copyright (c) 2022 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne + +! This file was ported from Lean 3 source module probability.moments +! leanprover-community/mathlib commit 85453a2a14be8da64caf15ca50930cf4c6e5d8de +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.Probability.Variance + +/-! +# Moments and moment generating function + +## Main definitions + +* `ProbabilityTheory.moment X p μ`: `p`th moment of a real random variable `X` with respect to + measure `μ`, `μ[X^p]` +* `ProbabilityTheory.centralMoment X p μ`:`p`th central moment of `X` with respect to measure `μ`, + `μ[(X - μ[X])^p]` +* `ProbabilityTheory.mgf X μ t`: moment generating function of `X` with respect to measure `μ`, + `μ[exp(t*X)]` +* `ProbabilityTheory.cgf X μ t`: cumulant generating function, logarithm of the moment generating + function + +## Main results + +* `ProbabilityTheory.IndepFun.mgf_add`: if two real random variables `X` and `Y` are independent + and their mgfs are defined at `t`, then `mgf (X + Y) μ t = mgf X μ t * mgf Y μ t` +* `ProbabilityTheory.IndepFun.cgf_add`: if two real random variables `X` and `Y` are independent + and their cgfs are defined at `t`, then `cgf (X + Y) μ t = cgf X μ t + cgf Y μ t` +* `ProbabilityTheory.measure_ge_le_exp_cgf` and `ProbabilityTheory.measure_le_le_exp_cgf`: + Chernoff bound on the upper (resp. lower) tail of a random variable. For `t` nonnegative such that + the cgf exists, `ℙ(ε ≤ X) ≤ exp(- t*ε + cgf X ℙ t)`. See also + `ProbabilityTheory.measure_ge_le_exp_mul_mgf` and + `ProbabilityTheory.measure_le_le_exp_mul_mgf` for versions of these results using `mgf` instead + of `cgf`. + +-/ + + +open MeasureTheory Filter Finset Real + +noncomputable section + +open scoped BigOperators MeasureTheory ProbabilityTheory ENNReal NNReal + +namespace ProbabilityTheory + +variable {Ω ι : Type _} {m : MeasurableSpace Ω} {X : Ω → ℝ} {p : ℕ} {μ : Measure Ω} + +/-- Moment of a real random variable, `μ[X ^ p]`. -/ +def moment (X : Ω → ℝ) (p : ℕ) (μ : Measure Ω) : ℝ := + μ[X ^ p] +#align probability_theory.moment ProbabilityTheory.moment + +/-- Central moment of a real random variable, `μ[(X - μ[X]) ^ p]`. -/ +def centralMoment (X : Ω → ℝ) (p : ℕ) (μ : Measure Ω) : ℝ := by + have m := fun (x : Ω) => μ[X] -- Porting note: Lean deems `μ[(X - fun x => μ[X]) ^ p]` ambiguous + exact μ[(X - m) ^ p] +#align probability_theory.central_moment ProbabilityTheory.centralMoment + +@[simp] +theorem moment_zero (hp : p ≠ 0) : moment 0 p μ = 0 := by + simp only [moment, hp, zero_pow', Ne.def, not_false_iff, Pi.zero_apply, integral_const, + smul_eq_mul, mul_zero] +#align probability_theory.moment_zero ProbabilityTheory.moment_zero + +@[simp] +theorem centralMoment_zero (hp : p ≠ 0) : centralMoment 0 p μ = 0 := by + simp only [centralMoment, hp, Pi.zero_apply, integral_const, smul_eq_mul, + mul_zero, zero_sub, Pi.pow_apply, Pi.neg_apply, neg_zero, zero_pow', Ne.def, not_false_iff] +#align probability_theory.central_moment_zero ProbabilityTheory.centralMoment_zero + +theorem centralMoment_one' [IsFiniteMeasure μ] (h_int : Integrable X μ) : + centralMoment X 1 μ = (1 - (μ Set.univ).toReal) * μ[X] := by + simp only [centralMoment, Pi.sub_apply, pow_one] + rw [integral_sub h_int (integrable_const _)] + simp only [sub_mul, integral_const, smul_eq_mul, one_mul] +#align probability_theory.central_moment_one' ProbabilityTheory.centralMoment_one' + +@[simp] +theorem centralMoment_one [IsProbabilityMeasure μ] : centralMoment X 1 μ = 0 := by + by_cases h_int : Integrable X μ + · rw [centralMoment_one' h_int] + simp only [measure_univ, ENNReal.one_toReal, sub_self, zero_mul] + · simp only [centralMoment, Pi.sub_apply, pow_one] + have : ¬Integrable (fun x => X x - integral μ X) μ := by + refine' fun h_sub => h_int _ + have h_add : X = (fun x => X x - integral μ X) + fun _ => integral μ X := by ext1 x; simp + rw [h_add] + exact h_sub.add (integrable_const _) + rw [integral_undef this] +#align probability_theory.central_moment_one ProbabilityTheory.centralMoment_one + +theorem centralMoment_two_eq_variance [IsFiniteMeasure μ] (hX : Memℒp X 2 μ) : + centralMoment X 2 μ = variance X μ := by rw [hX.variance_eq]; rfl +#align probability_theory.central_moment_two_eq_variance ProbabilityTheory.centralMoment_two_eq_variance + +section MomentGeneratingFunction + +variable {t : ℝ} + +/-- Moment generating function of a real random variable `X`: `fun t => μ[exp(t*X)]`. -/ +def mgf (X : Ω → ℝ) (μ : Measure Ω) (t : ℝ) : ℝ := + μ[fun ω => exp (t * X ω)] +#align probability_theory.mgf ProbabilityTheory.mgf + +/-- Cumulant generating function of a real random variable `X`: `fun t => log μ[exp(t*X)]`. -/ +def cgf (X : Ω → ℝ) (μ : Measure Ω) (t : ℝ) : ℝ := + log (mgf X μ t) +#align probability_theory.cgf ProbabilityTheory.cgf + +@[simp] +theorem mgf_zero_fun : mgf 0 μ t = (μ Set.univ).toReal := by + simp only [mgf, Pi.zero_apply, mul_zero, exp_zero, integral_const, smul_eq_mul, mul_one] +#align probability_theory.mgf_zero_fun ProbabilityTheory.mgf_zero_fun + +@[simp] +theorem cgf_zero_fun : cgf 0 μ t = log (μ Set.univ).toReal := by simp only [cgf, mgf_zero_fun] +#align probability_theory.cgf_zero_fun ProbabilityTheory.cgf_zero_fun + +@[simp] +theorem mgf_zero_measure : mgf X (0 : Measure Ω) t = 0 := by simp only [mgf, integral_zero_measure] +#align probability_theory.mgf_zero_measure ProbabilityTheory.mgf_zero_measure + +@[simp] +theorem cgf_zero_measure : cgf X (0 : Measure Ω) t = 0 := by + simp only [cgf, log_zero, mgf_zero_measure] +#align probability_theory.cgf_zero_measure ProbabilityTheory.cgf_zero_measure + +@[simp] +theorem mgf_const' (c : ℝ) : mgf (fun _ => c) μ t = (μ Set.univ).toReal * exp (t * c) := by + simp only [mgf, integral_const, smul_eq_mul] +#align probability_theory.mgf_const' ProbabilityTheory.mgf_const' + +-- @[simp] -- Porting note: `simp only` already proves this +theorem mgf_const (c : ℝ) [IsProbabilityMeasure μ] : mgf (fun _ => c) μ t = exp (t * c) := by + simp only [mgf_const', measure_univ, ENNReal.one_toReal, one_mul] +#align probability_theory.mgf_const ProbabilityTheory.mgf_const + +@[simp] +theorem cgf_const' [IsFiniteMeasure μ] (hμ : μ ≠ 0) (c : ℝ) : + cgf (fun _ => c) μ t = log (μ Set.univ).toReal + t * c := by + simp only [cgf, mgf_const'] + rw [log_mul _ (exp_pos _).ne'] + · rw [log_exp _] + · rw [Ne.def, ENNReal.toReal_eq_zero_iff, Measure.measure_univ_eq_zero] + simp only [hμ, measure_ne_top μ Set.univ, or_self_iff, not_false_iff] +#align probability_theory.cgf_const' ProbabilityTheory.cgf_const' + +@[simp] +theorem cgf_const [IsProbabilityMeasure μ] (c : ℝ) : cgf (fun _ => c) μ t = t * c := by + simp only [cgf, mgf_const, log_exp] +#align probability_theory.cgf_const ProbabilityTheory.cgf_const + +@[simp] +theorem mgf_zero' : mgf X μ 0 = (μ Set.univ).toReal := by + simp only [mgf, zero_mul, exp_zero, integral_const, smul_eq_mul, mul_one] +#align probability_theory.mgf_zero' ProbabilityTheory.mgf_zero' + +-- @[simp] -- Porting note: `simp only` already proves this +theorem mgf_zero [IsProbabilityMeasure μ] : mgf X μ 0 = 1 := by + simp only [mgf_zero', measure_univ, ENNReal.one_toReal] +#align probability_theory.mgf_zero ProbabilityTheory.mgf_zero + +@[simp] +theorem cgf_zero' : cgf X μ 0 = log (μ Set.univ).toReal := by simp only [cgf, mgf_zero'] +#align probability_theory.cgf_zero' ProbabilityTheory.cgf_zero' + +-- @[simp] -- Porting note: `simp only` already proves this +theorem cgf_zero [IsProbabilityMeasure μ] : cgf X μ 0 = 0 := by + simp only [cgf_zero', measure_univ, ENNReal.one_toReal, log_one] +#align probability_theory.cgf_zero ProbabilityTheory.cgf_zero + +theorem mgf_undef (hX : ¬Integrable (fun ω => exp (t * X ω)) μ) : mgf X μ t = 0 := by + simp only [mgf, integral_undef hX] +#align probability_theory.mgf_undef ProbabilityTheory.mgf_undef + +theorem cgf_undef (hX : ¬Integrable (fun ω => exp (t * X ω)) μ) : cgf X μ t = 0 := by + simp only [cgf, mgf_undef hX, log_zero] +#align probability_theory.cgf_undef ProbabilityTheory.cgf_undef + +theorem mgf_nonneg : 0 ≤ mgf X μ t := by + refine' integral_nonneg _ + intro ω + simp only [Pi.zero_apply] + exact (exp_pos _).le +#align probability_theory.mgf_nonneg ProbabilityTheory.mgf_nonneg + +theorem mgf_pos' (hμ : μ ≠ 0) (h_int_X : Integrable (fun ω => exp (t * X ω)) μ) : + 0 < mgf X μ t := by + simp_rw [mgf] + have : ∫ x : Ω, exp (t * X x) ∂μ = ∫ x : Ω in Set.univ, exp (t * X x) ∂μ := by + simp only [Measure.restrict_univ] + rw [this, set_integral_pos_iff_support_of_nonneg_ae _ _] + · have h_eq_univ : (Function.support fun x : Ω => exp (t * X x)) = Set.univ := by + ext1 x + simp only [Function.mem_support, Set.mem_univ, iff_true_iff] + exact (exp_pos _).ne' + rw [h_eq_univ, Set.inter_univ _] + refine' Ne.bot_lt _ + simp only [hμ, ENNReal.bot_eq_zero, Ne.def, Measure.measure_univ_eq_zero, not_false_iff] + · refine' eventually_of_forall fun x => _ + rw [Pi.zero_apply] + exact (exp_pos _).le + · rwa [integrableOn_univ] +#align probability_theory.mgf_pos' ProbabilityTheory.mgf_pos' + +theorem mgf_pos [IsProbabilityMeasure μ] (h_int_X : Integrable (fun ω => exp (t * X ω)) μ) : + 0 < mgf X μ t := + mgf_pos' (IsProbabilityMeasure.ne_zero μ) h_int_X +#align probability_theory.mgf_pos ProbabilityTheory.mgf_pos + +theorem mgf_neg : mgf (-X) μ t = mgf X μ (-t) := by simp_rw [mgf, Pi.neg_apply, mul_neg, neg_mul] +#align probability_theory.mgf_neg ProbabilityTheory.mgf_neg + +theorem cgf_neg : cgf (-X) μ t = cgf X μ (-t) := by simp_rw [cgf, mgf_neg] +#align probability_theory.cgf_neg ProbabilityTheory.cgf_neg + +/-- This is a trivial application of `IndepFun.comp` but it will come up frequently. -/ +theorem IndepFun.exp_mul {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ) (s t : ℝ) : + IndepFun (fun ω => exp (s * X ω)) (fun ω => exp (t * Y ω)) μ := by + have h_meas : ∀ t, Measurable fun x => exp (t * x) := fun t => (measurable_id'.const_mul t).exp + change IndepFun ((fun x => exp (s * x)) ∘ X) ((fun x => exp (t * x)) ∘ Y) μ + exact IndepFun.comp h_indep (h_meas s) (h_meas t) +#align probability_theory.indep_fun.exp_mul ProbabilityTheory.IndepFun.exp_mul + +theorem IndepFun.mgf_add {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ) + (hX : AEStronglyMeasurable (fun ω => exp (t * X ω)) μ) + (hY : AEStronglyMeasurable (fun ω => exp (t * Y ω)) μ) : + mgf (X + Y) μ t = mgf X μ t * mgf Y μ t := by + simp_rw [mgf, Pi.add_apply, mul_add, exp_add] + exact (h_indep.exp_mul t t).integral_mul hX hY +#align probability_theory.indep_fun.mgf_add ProbabilityTheory.IndepFun.mgf_add + +theorem IndepFun.mgf_add' {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ) (hX : AEStronglyMeasurable X μ) + (hY : AEStronglyMeasurable Y μ) : mgf (X + Y) μ t = mgf X μ t * mgf Y μ t := by + have A : Continuous fun x : ℝ => exp (t * x) := by continuity + have h'X : AEStronglyMeasurable (fun ω => exp (t * X ω)) μ := + A.aestronglyMeasurable.comp_aemeasurable hX.aemeasurable + have h'Y : AEStronglyMeasurable (fun ω => exp (t * Y ω)) μ := + A.aestronglyMeasurable.comp_aemeasurable hY.aemeasurable + exact h_indep.mgf_add h'X h'Y +#align probability_theory.indep_fun.mgf_add' ProbabilityTheory.IndepFun.mgf_add' + +theorem IndepFun.cgf_add {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ) + (h_int_X : Integrable (fun ω => exp (t * X ω)) μ) + (h_int_Y : Integrable (fun ω => exp (t * Y ω)) μ) : + cgf (X + Y) μ t = cgf X μ t + cgf Y μ t := by + by_cases hμ : μ = 0 + · simp [hμ] + simp only [cgf, h_indep.mgf_add h_int_X.aestronglyMeasurable h_int_Y.aestronglyMeasurable] + exact log_mul (mgf_pos' hμ h_int_X).ne' (mgf_pos' hμ h_int_Y).ne' +#align probability_theory.indep_fun.cgf_add ProbabilityTheory.IndepFun.cgf_add + +theorem aestronglyMeasurable_exp_mul_add {X Y : Ω → ℝ} + (h_int_X : AEStronglyMeasurable (fun ω => exp (t * X ω)) μ) + (h_int_Y : AEStronglyMeasurable (fun ω => exp (t * Y ω)) μ) : + AEStronglyMeasurable (fun ω => exp (t * (X + Y) ω)) μ := by + simp_rw [Pi.add_apply, mul_add, exp_add] + exact AEStronglyMeasurable.mul h_int_X h_int_Y +#align probability_theory.ae_strongly_measurable_exp_mul_add ProbabilityTheory.aestronglyMeasurable_exp_mul_add + +theorem aestronglyMeasurable_exp_mul_sum {X : ι → Ω → ℝ} {s : Finset ι} + (h_int : ∀ i ∈ s, AEStronglyMeasurable (fun ω => exp (t * X i ω)) μ) : + AEStronglyMeasurable (fun ω => exp (t * (∑ i in s, X i) ω)) μ := by + classical + induction' s using Finset.induction_on with i s hi_notin_s h_rec h_int + · simp only [Pi.zero_apply, sum_apply, sum_empty, mul_zero, exp_zero] + exact aestronglyMeasurable_const + · have : ∀ i : ι, i ∈ s → AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i hi => + h_int i (mem_insert_of_mem hi) + specialize h_rec this + rw [sum_insert hi_notin_s] + apply aestronglyMeasurable_exp_mul_add (h_int i (mem_insert_self _ _)) h_rec +#align probability_theory.ae_strongly_measurable_exp_mul_sum ProbabilityTheory.aestronglyMeasurable_exp_mul_sum + +theorem IndepFun.integrable_exp_mul_add {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ) + (h_int_X : Integrable (fun ω => exp (t * X ω)) μ) + (h_int_Y : Integrable (fun ω => exp (t * Y ω)) μ) : + Integrable (fun ω => exp (t * (X + Y) ω)) μ := by + simp_rw [Pi.add_apply, mul_add, exp_add] + exact (h_indep.exp_mul t t).integrable_mul h_int_X h_int_Y +#align probability_theory.indep_fun.integrable_exp_mul_add ProbabilityTheory.IndepFun.integrable_exp_mul_add + +theorem iIndepFun.integrable_exp_mul_sum [IsProbabilityMeasure μ] {X : ι → Ω → ℝ} + (h_indep : iIndepFun (fun i => inferInstance) X μ) (h_meas : ∀ i, Measurable (X i)) + {s : Finset ι} (h_int : ∀ i ∈ s, Integrable (fun ω => exp (t * X i ω)) μ) : + Integrable (fun ω => exp (t * (∑ i in s, X i) ω)) μ := by + classical + induction' s using Finset.induction_on with i s hi_notin_s h_rec h_int + · simp only [Pi.zero_apply, sum_apply, sum_empty, mul_zero, exp_zero] + exact integrable_const _ + · have : ∀ i : ι, i ∈ s → Integrable (fun ω : Ω => exp (t * X i ω)) μ := fun i hi => + h_int i (mem_insert_of_mem hi) + specialize h_rec this + rw [sum_insert hi_notin_s] + refine' IndepFun.integrable_exp_mul_add _ (h_int i (mem_insert_self _ _)) h_rec + exact (h_indep.indepFun_finset_sum_of_not_mem h_meas hi_notin_s).symm +set_option linter.uppercaseLean3 false in +#align probability_theory.Indep_fun.integrable_exp_mul_sum ProbabilityTheory.iIndepFun.integrable_exp_mul_sum + +theorem iIndepFun.mgf_sum [IsProbabilityMeasure μ] {X : ι → Ω → ℝ} + (h_indep : iIndepFun (fun i => inferInstance) X μ) (h_meas : ∀ i, Measurable (X i)) + (s : Finset ι) : mgf (∑ i in s, X i) μ t = ∏ i in s, mgf (X i) μ t := by + classical + induction' s using Finset.induction_on with i s hi_notin_s h_rec h_int + · simp only [sum_empty, mgf_zero_fun, measure_univ, ENNReal.one_toReal, prod_empty] + · have h_int' : ∀ i : ι, AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i => + ((h_meas i).const_mul t).exp.aestronglyMeasurable + rw [sum_insert hi_notin_s, + IndepFun.mgf_add (h_indep.indepFun_finset_sum_of_not_mem h_meas hi_notin_s).symm (h_int' i) + (aestronglyMeasurable_exp_mul_sum fun i _ => h_int' i), + h_rec, prod_insert hi_notin_s] +set_option linter.uppercaseLean3 false in +#align probability_theory.Indep_fun.mgf_sum ProbabilityTheory.iIndepFun.mgf_sum + +theorem iIndepFun.cgf_sum [IsProbabilityMeasure μ] {X : ι → Ω → ℝ} + (h_indep : iIndepFun (fun i => inferInstance) X μ) (h_meas : ∀ i, Measurable (X i)) + {s : Finset ι} (h_int : ∀ i ∈ s, Integrable (fun ω => exp (t * X i ω)) μ) : + cgf (∑ i in s, X i) μ t = ∑ i in s, cgf (X i) μ t := by + simp_rw [cgf] + rw [← log_prod _ _ fun j hj => ?_] + · rw [h_indep.mgf_sum h_meas] + · exact (mgf_pos (h_int j hj)).ne' +set_option linter.uppercaseLean3 false in +#align probability_theory.Indep_fun.cgf_sum ProbabilityTheory.iIndepFun.cgf_sum + +/-- **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 ω)) μ) : + (μ {ω | ε ≤ X ω}).toReal ≤ exp (-t * ε) * mgf X μ t := by + cases' 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] + rw [ENNReal.toReal_le_toReal (measure_ne_top μ _) (measure_ne_top μ _)] + exact measure_mono (Set.subset_univ _) + calc + (μ {ω | ε ≤ X ω}).toReal = (μ {ω | exp (t * ε) ≤ exp (t * X ω)}).toReal := by + congr with ω + simp only [Set.mem_setOf_eq, exp_le_exp, gt_iff_lt] + 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 * ε) * (μ {ω | exp (t * ε) ≤ exp (t * X ω)}).toReal ≤ + μ[fun ω => exp (t * X ω)] := + mul_meas_ge_le_integral_of_nonneg (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 +#align probability_theory.measure_ge_le_exp_mul_mgf ProbabilityTheory.measure_ge_le_exp_mul_mgf + +/-- **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 ω)) μ) : + (μ {ω | X ω ≤ ε}).toReal ≤ 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) _) + · congr with ω + simp only [Pi.neg_apply, neg_le_neg_iff] + · simp_rw [Pi.neg_apply, neg_mul_neg] + exact h_int +#align probability_theory.measure_le_le_exp_mul_mgf ProbabilityTheory.measure_le_le_exp_mul_mgf + +/-- **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 ω)) μ) : + (μ {ω | ε ≤ X ω}).toReal ≤ 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 +#align probability_theory.measure_ge_le_exp_cgf ProbabilityTheory.measure_ge_le_exp_cgf + +/-- **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 ω)) μ) : + (μ {ω | X ω ≤ ε}).toReal ≤ 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 +#align probability_theory.measure_le_le_exp_cgf ProbabilityTheory.measure_le_le_exp_cgf + +end MomentGeneratingFunction + +end ProbabilityTheory