# 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 : } (X : Ω) (p : ) (μ : ) :

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

Equations
• = ∫ (x : Ω), (X ^ p) xμ
Instances For
def ProbabilityTheory.centralMoment {Ω : Type u_1} {m : } (X : Ω) (p : ) (μ : ) :

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

Equations
• = let_fun m_1 := fun (x : Ω) => ∫ (x : Ω), X xμ; ∫ (x : Ω), ((X - m_1) ^ p) xμ
Instances For
@[simp]
theorem ProbabilityTheory.moment_zero {Ω : Type u_1} {m : } {p : } {μ : } (hp : p 0) :
= 0
@[simp]
theorem ProbabilityTheory.centralMoment_zero {Ω : Type u_1} {m : } {p : } {μ : } (hp : p 0) :
theorem ProbabilityTheory.centralMoment_one' {Ω : Type u_1} {m : } {X : Ω} {μ : } (h_int : ) :
= (1 - (μ Set.univ).toReal) * ∫ (x : Ω), X xμ
@[simp]
theorem ProbabilityTheory.centralMoment_one {Ω : Type u_1} {m : } {X : Ω} {μ : } :
theorem ProbabilityTheory.centralMoment_two_eq_variance {Ω : Type u_1} {m : } {X : Ω} {μ : } (hX : ) :
def ProbabilityTheory.mgf {Ω : Type u_1} {m : } (X : Ω) (μ : ) (t : ) :

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

Equations
• = ∫ (x : Ω), (fun (ω : Ω) => Real.exp (t * X ω)) xμ
Instances For
def ProbabilityTheory.cgf {Ω : Type u_1} {m : } (X : Ω) (μ : ) (t : ) :

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

Equations
Instances For
@[simp]
theorem ProbabilityTheory.mgf_zero_fun {Ω : Type u_1} {m : } {μ : } {t : } :
= (μ Set.univ).toReal
@[simp]
theorem ProbabilityTheory.cgf_zero_fun {Ω : Type u_1} {m : } {μ : } {t : } :
= Real.log (μ Set.univ).toReal
@[simp]
theorem ProbabilityTheory.mgf_zero_measure {Ω : Type u_1} {m : } {X : Ω} {t : } :
= 0
@[simp]
theorem ProbabilityTheory.cgf_zero_measure {Ω : Type u_1} {m : } {X : Ω} {t : } :
= 0
@[simp]
theorem ProbabilityTheory.mgf_const' {Ω : Type u_1} {m : } {μ : } {t : } (c : ) :
ProbabilityTheory.mgf (fun (x : Ω) => c) μ t = (μ Set.univ).toReal * Real.exp (t * c)
theorem ProbabilityTheory.mgf_const {Ω : Type u_1} {m : } {μ : } {t : } (c : ) :
ProbabilityTheory.mgf (fun (x : Ω) => c) μ t = Real.exp (t * c)
@[simp]
theorem ProbabilityTheory.cgf_const' {Ω : Type u_1} {m : } {μ : } {t : } (hμ : μ 0) (c : ) :
ProbabilityTheory.cgf (fun (x : Ω) => c) μ t = Real.log (μ Set.univ).toReal + t * c
@[simp]
theorem ProbabilityTheory.cgf_const {Ω : Type u_1} {m : } {μ : } {t : } (c : ) :
ProbabilityTheory.cgf (fun (x : Ω) => c) μ t = t * c
@[simp]
theorem ProbabilityTheory.mgf_zero' {Ω : Type u_1} {m : } {X : Ω} {μ : } :
= (μ Set.univ).toReal
theorem ProbabilityTheory.mgf_zero {Ω : Type u_1} {m : } {X : Ω} {μ : } :
= 1
@[simp]
theorem ProbabilityTheory.cgf_zero' {Ω : Type u_1} {m : } {X : Ω} {μ : } :
= Real.log (μ Set.univ).toReal
theorem ProbabilityTheory.cgf_zero {Ω : Type u_1} {m : } {X : Ω} {μ : } :
= 0
theorem ProbabilityTheory.mgf_undef {Ω : Type u_1} {m : } {X : Ω} {μ : } {t : } (hX : ¬MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) :
= 0
theorem ProbabilityTheory.cgf_undef {Ω : Type u_1} {m : } {X : Ω} {μ : } {t : } (hX : ¬MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) :
= 0
theorem ProbabilityTheory.mgf_nonneg {Ω : Type u_1} {m : } {X : Ω} {μ : } {t : } :
0
theorem ProbabilityTheory.mgf_pos' {Ω : Type u_1} {m : } {X : Ω} {μ : } {t : } (hμ : μ 0) (h_int_X : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) :
0 <
theorem ProbabilityTheory.mgf_pos {Ω : Type u_1} {m : } {X : Ω} {μ : } {t : } (h_int_X : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) :
0 <
theorem ProbabilityTheory.mgf_neg {Ω : Type u_1} {m : } {X : Ω} {μ : } {t : } :
=
theorem ProbabilityTheory.cgf_neg {Ω : Type u_1} {m : } {X : Ω} {μ : } {t : } :
=
theorem ProbabilityTheory.IndepFun.exp_mul {Ω : Type u_1} {m : } {μ : } {X : Ω} {Y : Ω} (h_indep : ) (s : ) (t : ) :
ProbabilityTheory.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 : } {μ : } {t : } {X : Ω} {Y : Ω} (h_indep : ) (hX : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * X ω)) μ) (hY : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * Y ω)) μ) :
theorem ProbabilityTheory.IndepFun.mgf_add' {Ω : Type u_1} {m : } {μ : } {t : } {X : Ω} {Y : Ω} (h_indep : ) (hX : ) (hY : ) :
theorem ProbabilityTheory.IndepFun.cgf_add {Ω : Type u_1} {m : } {μ : } {t : } {X : Ω} {Y : Ω} (h_indep : ) (h_int_X : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) (h_int_Y : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * Y ω)) μ) :
theorem ProbabilityTheory.aestronglyMeasurable_exp_mul_add {Ω : Type u_1} {m : } {μ : } {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 : } {μ : } {t : } {X : ιΩ} {s : } (h_int : is, MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * X i ω)) μ) :
MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * Finset.sum s (fun (i : ι) => X i) ω)) μ
theorem ProbabilityTheory.IndepFun.integrable_exp_mul_add {Ω : Type u_1} {m : } {μ : } {t : } {X : Ω} {Y : Ω} (h_indep : ) (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 : } {μ : } {t : } {X : ιΩ} (h_indep : ProbabilityTheory.iIndepFun (fun (i : ι) => inferInstance) X μ) (h_meas : ∀ (i : ι), Measurable (X i)) {s : } (h_int : is, MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X i ω)) μ) :
MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * Finset.sum s (fun (i : ι) => X i) ω)) μ
theorem ProbabilityTheory.iIndepFun.mgf_sum {Ω : Type u_1} {ι : Type u_2} {m : } {μ : } {t : } {X : ιΩ} (h_indep : ProbabilityTheory.iIndepFun (fun (i : ι) => inferInstance) X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (s : ) :
ProbabilityTheory.mgf (Finset.sum s fun (i : ι) => X i) μ t = Finset.prod s fun (i : ι) => ProbabilityTheory.mgf (X i) μ t
theorem ProbabilityTheory.iIndepFun.cgf_sum {Ω : Type u_1} {ι : Type u_2} {m : } {μ : } {t : } {X : ιΩ} (h_indep : ProbabilityTheory.iIndepFun (fun (i : ι) => inferInstance) X μ) (h_meas : ∀ (i : ι), Measurable (X i)) {s : } (h_int : is, MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X i ω)) μ) :
ProbabilityTheory.cgf (Finset.sum s fun (i : ι) => X i) μ t = Finset.sum s fun (i : ι) => ProbabilityTheory.cgf (X i) μ t
theorem ProbabilityTheory.measure_ge_le_exp_mul_mgf {Ω : Type u_1} {m : } {X : Ω} {μ : } {t : } (ε : ) (ht : 0 t) (h_int : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) :
(μ {ω : Ω | ε X ω}).toReal Real.exp (-t * ε) *

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

theorem ProbabilityTheory.measure_le_le_exp_mul_mgf {Ω : Type u_1} {m : } {X : Ω} {μ : } {t : } (ε : ) (ht : t 0) (h_int : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) :
(μ {ω : Ω | X ω ε}).toReal Real.exp (-t * ε) *

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

theorem ProbabilityTheory.measure_ge_le_exp_cgf {Ω : Type u_1} {m : } {X : Ω} {μ : } {t : } (ε : ) (ht : 0 t) (h_int : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) :
(μ {ω : Ω | ε X ω}).toReal Real.exp (-t * ε + )

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

theorem ProbabilityTheory.measure_le_le_exp_cgf {Ω : Type u_1} {m : } {X : Ω} {μ : } {t : } (ε : ) (ht : t 0) (h_int : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) :
(μ {ω : Ω | X ω ε}).toReal Real.exp (-t * ε + )

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