mathlib3documentation

probability.moments

Moments and moment generating function #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

• probability_theory.moment X p μ: pth moment of a real random variable X with respect to measure μ, μ[X^p]
• probability_theory.central_moment X p μ:pth central moment of X with respect to measure μ, μ[(X - μ[X])^p]
• probability_theory.mgf X μ t: moment generating function of X with respect to measure μ, μ[exp(t*X)]
• probability_theory.cgf X μ t: cumulant generating function, logarithm of the moment generating function

Main results #

• probability_theory.indep_fun.mgf_add: if two real random variables X and Y are independent and their mgf are defined at t, then mgf (X + Y) μ t = mgf X μ t * mgf Y μ t
• probability_theory.indep_fun.cgf_add: if two real random variables X and Y are independent and their mgf are defined at t, then cgf (X + Y) μ t = cgf X μ t + cgf Y μ t
• probability_theory.measure_ge_le_exp_cgf and probability_theory.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 probability_theory.measure_ge_le_exp_mul_mgf and probability_theory.measure_le_le_exp_mul_mgf for versions of these results using mgf instead of cgf.
noncomputable def probability_theory.moment {Ω : Type u_1} {m : measurable_space Ω} (X : Ω ) (p : ) (μ : measure_theory.measure Ω) :

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

Equations
noncomputable def probability_theory.central_moment {Ω : Type u_1} {m : measurable_space Ω} (X : Ω ) (p : ) (μ : measure_theory.measure Ω) :

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

Equations
@[simp]
theorem probability_theory.moment_zero {Ω : Type u_1} {m : measurable_space Ω} {p : } {μ : measure_theory.measure Ω} (hp : p 0) :
= 0
@[simp]
theorem probability_theory.central_moment_zero {Ω : Type u_1} {m : measurable_space Ω} {p : } {μ : measure_theory.measure Ω} (hp : p 0) :
theorem probability_theory.central_moment_one' {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {μ : measure_theory.measure Ω} (h_int : μ) :
= (1 - (μ set.univ).to_real) * (x : Ω), X x μ
@[simp]
theorem probability_theory.central_moment_one {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {μ : measure_theory.measure Ω}  :
noncomputable def probability_theory.mgf {Ω : Type u_1} {m : measurable_space Ω} (X : Ω ) (μ : measure_theory.measure Ω) (t : ) :

Moment generating function of a real random variable X: λ t, μ[exp(t*X)].

Equations
noncomputable def probability_theory.cgf {Ω : Type u_1} {m : measurable_space Ω} (X : Ω ) (μ : measure_theory.measure Ω) (t : ) :

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

Equations
@[simp]
@[simp]
theorem probability_theory.cgf_zero_fun {Ω : Type u_1} {m : measurable_space Ω} {μ : measure_theory.measure Ω} {t : } :
=
@[simp]
theorem probability_theory.mgf_zero_measure {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {t : } :
= 0
@[simp]
theorem probability_theory.cgf_zero_measure {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {t : } :
= 0
@[simp]
theorem probability_theory.mgf_const' {Ω : Type u_1} {m : measurable_space Ω} {μ : measure_theory.measure Ω} {t : } (c : ) :
probability_theory.mgf (λ (_x : Ω), c) μ t = (μ set.univ).to_real * rexp (t * c)
@[simp]
theorem probability_theory.mgf_const {Ω : Type u_1} {m : measurable_space Ω} {μ : measure_theory.measure Ω} {t : } (c : )  :
probability_theory.mgf (λ (_x : Ω), c) μ t = rexp (t * c)
@[simp]
theorem probability_theory.cgf_const' {Ω : Type u_1} {m : measurable_space Ω} {μ : measure_theory.measure Ω} {t : } (hμ : μ 0) (c : ) :
probability_theory.cgf (λ (_x : Ω), c) μ t = + t * c
@[simp]
theorem probability_theory.cgf_const {Ω : Type u_1} {m : measurable_space Ω} {μ : measure_theory.measure Ω} {t : } (c : ) :
probability_theory.cgf (λ (_x : Ω), c) μ t = t * c
@[simp]
theorem probability_theory.mgf_zero' {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {μ : measure_theory.measure Ω} :
@[simp]
theorem probability_theory.mgf_zero {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {μ : measure_theory.measure Ω}  :
= 1
@[simp]
theorem probability_theory.cgf_zero' {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {μ : measure_theory.measure Ω} :
=
@[simp]
theorem probability_theory.cgf_zero {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {μ : measure_theory.measure Ω}  :
= 0
theorem probability_theory.mgf_undef {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {μ : measure_theory.measure Ω} {t : } (hX : ¬measure_theory.integrable (λ (ω : Ω), rexp (t * X ω)) μ) :
= 0
theorem probability_theory.cgf_undef {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {μ : measure_theory.measure Ω} {t : } (hX : ¬measure_theory.integrable (λ (ω : Ω), rexp (t * X ω)) μ) :
= 0
theorem probability_theory.mgf_nonneg {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {μ : measure_theory.measure Ω} {t : } :
0
theorem probability_theory.mgf_pos' {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {μ : measure_theory.measure Ω} {t : } (hμ : μ 0) (h_int_X : measure_theory.integrable (λ (ω : Ω), rexp (t * X ω)) μ) :
0 <
theorem probability_theory.mgf_pos {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {μ : measure_theory.measure Ω} {t : } (h_int_X : measure_theory.integrable (λ (ω : Ω), rexp (t * X ω)) μ) :
0 <
theorem probability_theory.mgf_neg {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {μ : measure_theory.measure Ω} {t : } :
t = (-t)
theorem probability_theory.cgf_neg {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {μ : measure_theory.measure Ω} {t : } :
t = (-t)
theorem probability_theory.indep_fun.exp_mul {Ω : Type u_1} {m : measurable_space Ω} {μ : measure_theory.measure Ω} {X Y : Ω } (h_indep : μ) (s t : ) :
probability_theory.indep_fun (λ (ω : Ω), rexp (s * X ω)) (λ (ω : Ω), rexp (t * Y ω)) μ

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

theorem probability_theory.indep_fun.mgf_add {Ω : Type u_1} {m : measurable_space Ω} {μ : measure_theory.measure Ω} {t : } {X Y : Ω } (h_indep : μ) (hX : measure_theory.ae_strongly_measurable (λ (ω : Ω), rexp (t * X ω)) μ) (hY : measure_theory.ae_strongly_measurable (λ (ω : Ω), rexp (t * Y ω)) μ) :
theorem probability_theory.indep_fun.mgf_add' {Ω : Type u_1} {m : measurable_space Ω} {μ : measure_theory.measure Ω} {t : } {X Y : Ω } (h_indep : μ)  :
theorem probability_theory.indep_fun.cgf_add {Ω : Type u_1} {m : measurable_space Ω} {μ : measure_theory.measure Ω} {t : } {X Y : Ω } (h_indep : μ) (h_int_X : measure_theory.integrable (λ (ω : Ω), rexp (t * X ω)) μ) (h_int_Y : measure_theory.integrable (λ (ω : Ω), rexp (t * Y ω)) μ) :
theorem probability_theory.ae_strongly_measurable_exp_mul_add {Ω : Type u_1} {m : measurable_space Ω} {μ : measure_theory.measure Ω} {t : } {X Y : Ω } (h_int_X : measure_theory.ae_strongly_measurable (λ (ω : Ω), rexp (t * X ω)) μ) (h_int_Y : measure_theory.ae_strongly_measurable (λ (ω : Ω), rexp (t * Y ω)) μ) :
measure_theory.ae_strongly_measurable (λ (ω : Ω), rexp (t * (X + Y) ω)) μ
theorem probability_theory.ae_strongly_measurable_exp_mul_sum {Ω : Type u_1} {ι : Type u_2} {m : measurable_space Ω} {μ : measure_theory.measure Ω} {t : } {X : ι Ω } {s : finset ι} (h_int : (i : ι), i s measure_theory.ae_strongly_measurable (λ (ω : Ω), rexp (t * X i ω)) μ) :
measure_theory.ae_strongly_measurable (λ (ω : Ω), rexp (t * s.sum (λ (i : ι), X i) ω)) μ
theorem probability_theory.indep_fun.integrable_exp_mul_add {Ω : Type u_1} {m : measurable_space Ω} {μ : measure_theory.measure Ω} {t : } {X Y : Ω } (h_indep : μ) (h_int_X : measure_theory.integrable (λ (ω : Ω), rexp (t * X ω)) μ) (h_int_Y : measure_theory.integrable (λ (ω : Ω), rexp (t * Y ω)) μ) :
measure_theory.integrable (λ (ω : Ω), rexp (t * (X + Y) ω)) μ
theorem probability_theory.Indep_fun.integrable_exp_mul_sum {Ω : Type u_1} {ι : Type u_2} {m : measurable_space Ω} {μ : measure_theory.measure Ω} {t : } {X : ι Ω } (h_indep : probability_theory.Indep_fun (λ (i : ι), infer_instance) X μ) (h_meas : (i : ι), measurable (X i)) {s : finset ι} (h_int : (i : ι), i s measure_theory.integrable (λ (ω : Ω), rexp (t * X i ω)) μ) :
measure_theory.integrable (λ (ω : Ω), rexp (t * s.sum (λ (i : ι), X i) ω)) μ
theorem probability_theory.Indep_fun.mgf_sum {Ω : Type u_1} {ι : Type u_2} {m : measurable_space Ω} {μ : measure_theory.measure Ω} {t : } {X : ι Ω } (h_indep : probability_theory.Indep_fun (λ (i : ι), infer_instance) X μ) (h_meas : (i : ι), measurable (X i)) (s : finset ι) :
probability_theory.mgf (s.sum (λ (i : ι), X i)) μ t = s.prod (λ (i : ι), μ t)
theorem probability_theory.Indep_fun.cgf_sum {Ω : Type u_1} {ι : Type u_2} {m : measurable_space Ω} {μ : measure_theory.measure Ω} {t : } {X : ι Ω } (h_indep : probability_theory.Indep_fun (λ (i : ι), infer_instance) X μ) (h_meas : (i : ι), measurable (X i)) {s : finset ι} (h_int : (i : ι), i s measure_theory.integrable (λ (ω : Ω), rexp (t * X i ω)) μ) :
probability_theory.cgf (s.sum (λ (i : ι), X i)) μ t = s.sum (λ (i : ι), μ t)
theorem probability_theory.measure_ge_le_exp_mul_mgf {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {μ : measure_theory.measure Ω} {t : } (ε : ) (ht : 0 t) (h_int : measure_theory.integrable (λ (ω : Ω), rexp (t * X ω)) μ) :
(μ {ω : Ω | ε X ω}).to_real rexp (-t * ε) *

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

theorem probability_theory.measure_le_le_exp_mul_mgf {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {μ : measure_theory.measure Ω} {t : } (ε : ) (ht : t 0) (h_int : measure_theory.integrable (λ (ω : Ω), rexp (t * X ω)) μ) :
(μ {ω : Ω | X ω ε}).to_real rexp (-t * ε) *

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

theorem probability_theory.measure_ge_le_exp_cgf {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {μ : measure_theory.measure Ω} {t : } (ε : ) (ht : 0 t) (h_int : measure_theory.integrable (λ (ω : Ω), rexp (t * X ω)) μ) :
(μ {ω : Ω | ε X ω}).to_real rexp (-t * ε + t)

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

theorem probability_theory.measure_le_le_exp_cgf {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {μ : measure_theory.measure Ω} {t : } (ε : ) (ht : t 0) (h_int : measure_theory.integrable (λ (ω : Ω), rexp (t * X ω)) μ) :
(μ {ω : Ω | X ω ε}).to_real rexp (-t * ε + t)

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