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 μ = let_fun m_1 := fun (x : Ω) => ∫ (x : Ω), X x ∂μ; ∫ (x : Ω), ((X - m_1) ^ p) x ∂μ

@[simp]

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

@[simp]

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

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

@[simp]

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

theorem ProbabilityTheory.centralMoment_two_eq_variance {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.Memℒp X 2 μ) : ProbabilityTheory.centralMoment X 2 μ = ProbabilityTheory.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 : ℝ} : ProbabilityTheory.mgf 0 μ t = (↑↑μ Set.univ).toReal

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem ProbabilityTheory.mgf_const {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} (c : ℝ) [MeasureTheory.IsProbabilityMeasure μ] : ProbabilityTheory.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 : ℝ) : ProbabilityTheory.cgf (fun (x : Ω) => c) μ t = Real.log (↑↑μ Set.univ).toReal + t * c

@[simp]

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

@[simp]

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

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

@[simp]

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

theorem ProbabilityTheory.cgf_zero {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] : ProbabilityTheory.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 ω)) μ) : ProbabilityTheory.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 ω)) μ) : ProbabilityTheory.cgf X μ t = 0

theorem ProbabilityTheory.mgf_nonneg {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} : 0 ≤ ProbabilityTheory.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 < ProbabilityTheory.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 < ProbabilityTheory.mgf X μ t

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

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

theorem ProbabilityTheory.IndepFun.exp_mul {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {Y : Ω → ℝ} (h_indep : ProbabilityTheory.IndepFun X Y μ) (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 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X : Ω → ℝ} {Y : Ω → ℝ} (h_indep : ProbabilityTheory.IndepFun X Y μ) (hX : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * X ω)) μ) (hY : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * Y ω)) μ) : ProbabilityTheory.mgf (X + Y) μ t = ProbabilityTheory.mgf X μ t * ProbabilityTheory.mgf Y μ t

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

theorem ProbabilityTheory.IndepFun.cgf_add {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X : Ω → ℝ} {Y : Ω → ℝ} (h_indep : ProbabilityTheory.IndepFun X Y μ) (h_int_X : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) (h_int_Y : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * Y ω)) μ) : ProbabilityTheory.cgf (X + Y) μ t = ProbabilityTheory.cgf X μ t + ProbabilityTheory.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 * Finset.sum s (fun (i : ι) => X i) ω)) μ

theorem ProbabilityTheory.IndepFun.integrable_exp_mul_add {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X : Ω → ℝ} {Y : Ω → ℝ} (h_indep : ProbabilityTheory.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.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} (h_indep : ProbabilityTheory.iIndepFun (fun (i : ι) => inferInstance) 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 * Finset.sum s (fun (i : ι) => X i) ω)) μ

theorem ProbabilityTheory.iIndepFun.mgf_sum {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} (h_indep : ProbabilityTheory.iIndepFun (fun (i : ι) => inferInstance) X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (s : Finset ι) : 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 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} (h_indep : ProbabilityTheory.iIndepFun (fun (i : ι) => inferInstance) X μ) (h_meas : ∀ (i : ι), Measurable (X i)) {s : Finset ι} (h_int : ∀ i ∈ s, 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 : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} [MeasureTheory.IsFiniteMeasure μ] (ε : ℝ) (ht : 0 ≤ t) (h_int : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : (↑↑μ {ω : Ω | ε ≤ X ω}).toReal ≤ Real.exp (-t * ε) * ProbabilityTheory.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 ω)) μ) : (↑↑μ {ω : Ω | X ω ≤ ε}).toReal ≤ Real.exp (-t * ε) * ProbabilityTheory.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 ω)) μ) : (↑↑μ {ω : Ω | ε ≤ X ω}).toReal ≤ Real.exp (-t * ε + ProbabilityTheory.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 ω)) μ) : (↑↑μ {ω : Ω | X ω ≤ ε}).toReal ≤ Real.exp (-t * ε + ProbabilityTheory.cgf X μ t)

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