Moments and moment generating function

Main definitions

• ProbabilityTheory.moment X p μ: pth moment of a real random variable X with respect to measure μ, μ[X^p]
• ProbabilityTheory.centralMoment X p μ:pth 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.

def ProbabilityTheory.moment {Ω : Type u_1} {m : MeasurableSpace Ω} (X : Ω → ℝ) (p : ℕ) (μ : MeasureTheory.Measure Ω) : ℝ

Moment of a real random variable, μ[X ^ p].

Equations

• ProbabilityTheory.moment X p μ = ∫ (x : Ω), (X ^ p) x ∂μ

def ProbabilityTheory.centralMoment {Ω : Type u_1} {m : MeasurableSpace Ω} (X : Ω → ℝ) (p : ℕ) (μ : MeasureTheory.Measure Ω) : ℝ

Central moment of a real random variable, μ[(X - μ[X]) ^ p].

Equations

• ProbabilityTheory.centralMoment X p μ = ∫ (x : Ω), ((X - fun (x : Ω) => ∫ (x : Ω), X x ∂μ) ^ p) x ∂μ

@[simp]

theorem ProbabilityTheory.moment_zero {Ω : Type u_1} {m : MeasurableSpace Ω} {p : ℕ} {μ : MeasureTheory.Measure Ω} (hp : p ≠ 0) : moment 0 p μ = 0

@[simp]

theorem ProbabilityTheory.moment_zero_measure {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {p : ℕ} : moment X p 0 = 0

@[simp]

theorem ProbabilityTheory.centralMoment_zero {Ω : Type u_1} {m : MeasurableSpace Ω} {p : ℕ} {μ : MeasureTheory.Measure Ω} (hp : p ≠ 0) : centralMoment 0 p μ = 0

@[simp]

theorem ProbabilityTheory.centralMoment_zero_measure {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {p : ℕ} : centralMoment X p 0 = 0

theorem ProbabilityTheory.centralMoment_one' {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (h_int : MeasureTheory.Integrable X μ) : centralMoment X 1 μ = (1 - μ.real Set.univ) * ∫ (x : Ω), X x ∂μ

@[simp]

theorem ProbabilityTheory.centralMoment_one {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsZeroOrProbabilityMeasure μ] : centralMoment X 1 μ = 0

theorem ProbabilityTheory.centralMoment_two_eq_variance {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (hX : AEMeasurable X μ) : centralMoment X 2 μ = variance X μ

def ProbabilityTheory.mgf {Ω : Type u_1} {m : MeasurableSpace Ω} (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) (t : ℝ) : ℝ

Moment generating function of a real random variable X: fun t => μ[exp(t*X)].

Equations

• ProbabilityTheory.mgf X μ t = ∫ (x : Ω), (fun (ω : Ω) => Real.exp (t * X ω)) x ∂μ

def ProbabilityTheory.cgf {Ω : Type u_1} {m : MeasurableSpace Ω} (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) (t : ℝ) : ℝ

Cumulant generating function of a real random variable X: fun t => log μ[exp(t*X)].

Equations

• ProbabilityTheory.cgf X μ t = Real.log (ProbabilityTheory.mgf X μ t)

@[simp]

theorem ProbabilityTheory.mgf_zero_fun {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} : mgf 0 μ t = μ.real Set.univ

@[simp]

theorem ProbabilityTheory.cgf_zero_fun {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} : cgf 0 μ t = Real.log (μ.real Set.univ)

@[simp]

theorem ProbabilityTheory.mgf_zero_measure {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} : mgf X 0 = 0

@[simp]

theorem ProbabilityTheory.cgf_zero_measure {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} : cgf X 0 = 0

@[simp]

theorem ProbabilityTheory.mgf_const' {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} (c : ℝ) : mgf (fun (x : Ω) => c) μ t = μ.real Set.univ * Real.exp (t * c)

theorem ProbabilityTheory.mgf_const {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} (c : ℝ) [MeasureTheory.IsProbabilityMeasure μ] : mgf (fun (x : Ω) => c) μ t = Real.exp (t * c)

@[simp]

theorem ProbabilityTheory.cgf_const' {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hμ : μ ≠ 0) (c : ℝ) : cgf (fun (x : Ω) => c) μ t = Real.log (μ.real Set.univ) + t * c

@[simp]

theorem ProbabilityTheory.cgf_const {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (c : ℝ) : cgf (fun (x : Ω) => c) μ t = t * c

@[simp]

theorem ProbabilityTheory.mgf_zero' {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} : mgf X μ 0 = μ.real Set.univ

theorem ProbabilityTheory.mgf_zero {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] : mgf X μ 0 = 1

theorem ProbabilityTheory.cgf_zero' {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} : cgf X μ 0 = Real.log (μ.real Set.univ)

@[simp]

theorem ProbabilityTheory.cgf_zero {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsZeroOrProbabilityMeasure μ] : cgf X μ 0 = 0

theorem ProbabilityTheory.mgf_undef {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (hX : ¬MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : mgf X μ t = 0

theorem ProbabilityTheory.cgf_undef {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (hX : ¬MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : cgf X μ t = 0

theorem ProbabilityTheory.mgf_nonneg {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} : 0 ≤ mgf X μ t

theorem ProbabilityTheory.mgf_pos' {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (hμ : μ ≠ 0) (h_int_X : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : 0 < mgf X μ t

theorem ProbabilityTheory.mgf_pos {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (h_int_X : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : 0 < mgf X μ t

theorem ProbabilityTheory.mgf_pos_iff {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} [hμ : NeZero μ] : 0 < mgf X μ t ↔ MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ

theorem ProbabilityTheory.exp_cgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} [hμ : NeZero μ] (hX : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : Real.exp (cgf X μ t) = mgf X μ t

@[deprecated ProbabilityTheory.exp_cgf (since := "2025-03-08")]

theorem ProbabilityTheory.exp_cgf_of_neZero {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} [hμ : NeZero μ] (hX : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : Real.exp (cgf X μ t) = mgf X μ t

Alias of ProbabilityTheory.exp_cgf.

theorem ProbabilityTheory.mgf_map {Ω : Type u_1} {m : MeasurableSpace Ω} {Ω' : Type u_3} {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω'} {Y : Ω' → Ω} {X : Ω → ℝ} (hY : AEMeasurable Y μ) {t : ℝ} (hX : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * X ω)) (MeasureTheory.Measure.map Y μ)) : mgf X (MeasureTheory.Measure.map Y μ) t = mgf (X ∘ Y) μ t

theorem ProbabilityTheory.mgf_id_map {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (hX : AEMeasurable X μ) : mgf id (MeasureTheory.Measure.map X μ) = mgf X μ

theorem ProbabilityTheory.mgf_congr {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} {Y : Ω → ℝ} (h : X =ᵐ[μ] Y) : mgf X μ t = mgf Y μ t

theorem ProbabilityTheory.mgf_congr_identDistrib {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {Ω' : Type u_3} {mΩ' : MeasurableSpace Ω'} {μ' : MeasureTheory.Measure Ω'} {Y : Ω' → ℝ} (h : IdentDistrib X Y μ μ') : mgf X μ = mgf Y μ'

theorem ProbabilityTheory.mgf_neg {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} : mgf (-X) μ t = mgf X μ (-t)

theorem ProbabilityTheory.cgf_neg {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} : cgf (-X) μ t = cgf X μ (-t)

theorem ProbabilityTheory.mgf_smul_left {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (α : ℝ) : mgf (α • X) μ t = mgf X μ (α * t)

theorem ProbabilityTheory.mgf_const_add {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (α : ℝ) : mgf (fun (ω : Ω) => α + X ω) μ t = Real.exp (t * α) * mgf X μ t

theorem ProbabilityTheory.mgf_add_const {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (α : ℝ) : mgf (fun (ω : Ω) => X ω + α) μ t = mgf X μ t * Real.exp (t * α)

theorem ProbabilityTheory.mgf_add_measure {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} {ν : MeasureTheory.Measure Ω} (hμ : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) (hν : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) ν) : mgf X (μ + ν) t = mgf X μ t + mgf X ν t

theorem ProbabilityTheory.mgf_sum_measure {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {t : ℝ} {ι : Type u_3} {μ : ι → MeasureTheory.Measure Ω} (hμ : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) (MeasureTheory.Measure.sum μ)) : mgf X (MeasureTheory.Measure.sum μ) t = ∑' (i : ι), mgf X (μ i) t

theorem ProbabilityTheory.mgf_smul_measure {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (c : ENNReal) : mgf X (c • μ) t = c.toReal * mgf X μ t

theorem ProbabilityTheory.mgf_mono_of_nonneg {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} {Y : Ω → ℝ} (hXY : X ≤ᵐ[μ] Y) (ht : 0 ≤ t) (htY : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * Y ω)) μ) : mgf X μ t ≤ mgf Y μ t

The moment generating function is monotone in the random variable for t ≥ 0.

theorem ProbabilityTheory.mgf_anti_of_nonpos {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} {Y : Ω → ℝ} (hXY : X ≤ᵐ[μ] Y) (ht : t ≤ 0) (htX : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : mgf Y μ t ≤ mgf X μ t

The moment generating function is antitone in the random variable for t ≤ 0.

theorem ProbabilityTheory.IndepFun.exp_mul {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ) (s t : ℝ) : IndepFun (fun (ω : Ω) => Real.exp (s * X ω)) (fun (ω : Ω) => Real.exp (t * Y ω)) μ

This is a trivial application of IndepFun.comp but it will come up frequently.

theorem ProbabilityTheory.IndepFun.mgf_add {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ) (hX : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * X ω)) μ) (hY : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * Y ω)) μ) : mgf (X + Y) μ t = mgf X μ t * mgf Y μ t

theorem ProbabilityTheory.IndepFun.mgf_add' {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ) (hX : MeasureTheory.AEStronglyMeasurable X μ) (hY : MeasureTheory.AEStronglyMeasurable Y μ) : mgf (X + Y) μ t = mgf X μ t * mgf Y μ t

theorem ProbabilityTheory.IndepFun.cgf_add {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ) (h_int_X : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) (h_int_Y : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * Y ω)) μ) : cgf (X + Y) μ t = cgf X μ t + cgf Y μ t

theorem ProbabilityTheory.aestronglyMeasurable_exp_mul_add {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X Y : Ω → ℝ} (h_int_X : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * X ω)) μ) (h_int_Y : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * Y ω)) μ) : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * (X + Y) ω)) μ

theorem ProbabilityTheory.aestronglyMeasurable_exp_mul_sum {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X : ι → Ω → ℝ} {s : Finset ι} (h_int : ∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * X i ω)) μ) : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * (∑ i ∈ s, X i) ω)) μ

theorem ProbabilityTheory.IndepFun.integrable_exp_mul_add {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ) (h_int_X : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) (h_int_Y : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * Y ω)) μ) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * (X + Y) ω)) μ

theorem ProbabilityTheory.iIndepFun.integrable_exp_mul_sum {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) {s : Finset ι} (h_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X i ω)) μ) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * (∑ i ∈ s, X i) ω)) μ

theorem ProbabilityTheory.iIndepFun.mgf_sum {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (s : Finset ι) : mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t

theorem ProbabilityTheory.iIndepFun.cgf_sum {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) {s : Finset ι} (h_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X i ω)) μ) : cgf (∑ i ∈ s, X i) μ t = ∑ i ∈ s, cgf (X i) μ t

theorem ProbabilityTheory.mgf_congr_of_identDistrib {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (X : Ω → ℝ) {Ω' : Type u_3} {m' : MeasurableSpace Ω'} {μ' : MeasureTheory.Measure Ω'} (X' : Ω' → ℝ) (hident : IdentDistrib X X' μ μ') (t : ℝ) : mgf X μ t = mgf X' μ' t

theorem ProbabilityTheory.mgf_sum_of_identDistrib {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {s : Finset ι} {j : ι} (h_meas : ∀ (i : ι), Measurable (X i)) (h_indep : iIndepFun X μ) (hident : ∀ i ∈ s, ∀ j ∈ s, IdentDistrib (X i) (X j) μ μ) (hj : j ∈ s) (t : ℝ) : mgf (∑ i ∈ s, X i) μ t = mgf (X j) μ t ^ s.card

theorem ProbabilityTheory.measure_ge_le_exp_mul_mgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} [MeasureTheory.IsFiniteMeasure μ] (ε : ℝ) (ht : 0 ≤ t) (h_int : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : μ.real {ω : Ω | ε ≤ X ω} ≤ Real.exp (-t * ε) * mgf X μ t

Chernoff bound on the upper tail of a real random variable.

theorem ProbabilityTheory.measure_le_le_exp_mul_mgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} [MeasureTheory.IsFiniteMeasure μ] (ε : ℝ) (ht : t ≤ 0) (h_int : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : μ.real {ω : Ω | X ω ≤ ε} ≤ Real.exp (-t * ε) * mgf X μ t

Chernoff bound on the lower tail of a real random variable.

theorem ProbabilityTheory.measure_ge_le_exp_cgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} [MeasureTheory.IsFiniteMeasure μ] (ε : ℝ) (ht : 0 ≤ t) (h_int : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : μ.real {ω : Ω | ε ≤ X ω} ≤ Real.exp (-t * ε + cgf X μ t)

Chernoff bound on the upper tail of a real random variable.

theorem ProbabilityTheory.measure_le_le_exp_cgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} [MeasureTheory.IsFiniteMeasure μ] (ε : ℝ) (ht : t ≤ 0) (h_int : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : μ.real {ω : Ω | X ω ≤ ε} ≤ Real.exp (-t * ε + cgf X μ t)

Chernoff bound on the lower tail of a real random variable.

theorem ProbabilityTheory.mgf_dirac {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {x : ℝ} (hX : MeasureTheory.Measure.map X μ = MeasureTheory.Measure.dirac x) (t : ℝ) : mgf X μ t = Real.exp (x * t)

theorem ProbabilityTheory.mgf_dirac' {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {t : ℝ} [MeasurableSingletonClass Ω] {ω : Ω} : mgf X (MeasureTheory.Measure.dirac ω) t = Real.exp (t * X ω)

theorem ProbabilityTheory.aemeasurable_exp_mul {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (t : ℝ) (hX : AEMeasurable X μ) : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * X ω)) μ

theorem ProbabilityTheory.integrable_exp_mul_of_le {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} (t b : ℝ) (ht : 0 ≤ t) (hX : AEMeasurable X μ) (hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ