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 variableXwith respect to measureμ,μ[X^p]probability_theory.central_moment X p μ:pth central moment ofXwith respect to measureμ,μ[(X - μ[X])^p]probability_theory.mgf X μ t: moment generating function ofXwith 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 variablesXandYare independent and their mgf are defined att, thenmgf (X + Y) μ t = mgf X μ t * mgf Y μ tprobability_theory.indep_fun.cgf_add: if two real random variablesXandYare independent and their mgf are defined att, thencgf (X + Y) μ t = cgf X μ t + cgf Y μ tprobability_theory.measure_ge_le_exp_cgfandprobability_theory.measure_le_le_exp_cgf: Chernoff bound on the upper (resp. lower) tail of a random variable. Fortnonnegative such that the cgf exists,ℙ(ε ≤ X) ≤ exp(- t*ε + cgf X ℙ t). See alsoprobability_theory.measure_ge_le_exp_mul_mgfandprobability_theory.measure_le_le_exp_mul_mgffor versions of these results usingmgfinstead ofcgf.
noncomputable
def
probability_theory.moment
{Ω : Type u_1}
{m : measurable_space Ω}
(X : Ω → ℝ)
(p : ℕ)
(μ : measure_theory.measure Ω) :
Moment of a real random variable, μ[X ^ p].
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].
@[simp]
theorem
probability_theory.moment_zero
{Ω : Type u_1}
{m : measurable_space Ω}
{p : ℕ}
{μ : measure_theory.measure Ω}
(hp : p ≠ 0) :
probability_theory.moment 0 p μ = 0
@[simp]
theorem
probability_theory.central_moment_zero
{Ω : Type u_1}
{m : measurable_space Ω}
{p : ℕ}
{μ : measure_theory.measure Ω}
(hp : p ≠ 0) :
probability_theory.central_moment 0 p μ = 0
theorem
probability_theory.central_moment_one'
{Ω : Type u_1}
{m : measurable_space Ω}
{X : Ω → ℝ}
{μ : measure_theory.measure Ω}
[measure_theory.is_finite_measure μ]
(h_int : measure_theory.integrable X μ) :
@[simp]
theorem
probability_theory.central_moment_one
{Ω : Type u_1}
{m : measurable_space Ω}
{X : Ω → ℝ}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ] :
probability_theory.central_moment X 1 μ = 0
theorem
probability_theory.central_moment_two_eq_variance
{Ω : Type u_1}
{m : measurable_space Ω}
{X : Ω → ℝ}
{μ : measure_theory.measure Ω}
[measure_theory.is_finite_measure μ]
(hX : measure_theory.mem_ℒp X 2 μ) :
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)].
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
- probability_theory.cgf X μ t = real.log (probability_theory.mgf X μ t)
@[simp]
theorem
probability_theory.mgf_zero_fun
{Ω : Type u_1}
{m : measurable_space Ω}
{μ : measure_theory.measure Ω}
{t : ℝ} :
probability_theory.mgf 0 μ t = (⇑μ set.univ).to_real
@[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 : ℝ} :
probability_theory.mgf X 0 t = 0
@[simp]
theorem
probability_theory.cgf_zero_measure
{Ω : Type u_1}
{m : measurable_space Ω}
{X : Ω → ℝ}
{t : ℝ} :
probability_theory.cgf X 0 t = 0
@[simp]
theorem
probability_theory.mgf_const'
{Ω : Type u_1}
{m : measurable_space Ω}
{μ : measure_theory.measure Ω}
{t : ℝ}
(c : ℝ) :
@[simp]
theorem
probability_theory.mgf_const
{Ω : Type u_1}
{m : measurable_space Ω}
{μ : measure_theory.measure Ω}
{t : ℝ}
(c : ℝ)
[measure_theory.is_probability_measure μ] :
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 : ℝ}
[measure_theory.is_finite_measure μ]
(hμ : μ ≠ 0)
(c : ℝ) :
@[simp]
theorem
probability_theory.cgf_const
{Ω : Type u_1}
{m : measurable_space Ω}
{μ : measure_theory.measure Ω}
{t : ℝ}
[measure_theory.is_probability_measure μ]
(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 Ω} :
probability_theory.mgf X μ 0 = (⇑μ set.univ).to_real
@[simp]
theorem
probability_theory.mgf_zero
{Ω : Type u_1}
{m : measurable_space Ω}
{X : Ω → ℝ}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ] :
probability_theory.mgf X μ 0 = 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 Ω}
[measure_theory.is_probability_measure μ] :
probability_theory.cgf X μ 0 = 0
theorem
probability_theory.mgf_undef
{Ω : Type u_1}
{m : measurable_space Ω}
{X : Ω → ℝ}
{μ : measure_theory.measure Ω}
{t : ℝ}
(hX : ¬measure_theory.integrable (λ (ω : Ω), rexp (t * X ω)) μ) :
probability_theory.mgf X μ t = 0
theorem
probability_theory.cgf_undef
{Ω : Type u_1}
{m : measurable_space Ω}
{X : Ω → ℝ}
{μ : measure_theory.measure Ω}
{t : ℝ}
(hX : ¬measure_theory.integrable (λ (ω : Ω), rexp (t * X ω)) μ) :
probability_theory.cgf X μ t = 0
theorem
probability_theory.mgf_nonneg
{Ω : Type u_1}
{m : measurable_space Ω}
{X : Ω → ℝ}
{μ : measure_theory.measure Ω}
{t : ℝ} :
0 ≤ probability_theory.mgf X μ t
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 < probability_theory.mgf X μ t
theorem
probability_theory.mgf_pos
{Ω : Type u_1}
{m : measurable_space Ω}
{X : Ω → ℝ}
{μ : measure_theory.measure Ω}
{t : ℝ}
[measure_theory.is_probability_measure μ]
(h_int_X : measure_theory.integrable (λ (ω : Ω), rexp (t * X ω)) μ) :
0 < probability_theory.mgf X μ t
theorem
probability_theory.mgf_neg
{Ω : Type u_1}
{m : measurable_space Ω}
{X : Ω → ℝ}
{μ : measure_theory.measure Ω}
{t : ℝ} :
probability_theory.mgf (-X) μ t = probability_theory.mgf X μ (-t)
theorem
probability_theory.cgf_neg
{Ω : Type u_1}
{m : measurable_space Ω}
{X : Ω → ℝ}
{μ : measure_theory.measure Ω}
{t : ℝ} :
probability_theory.cgf (-X) μ t = probability_theory.cgf X μ (-t)
theorem
probability_theory.indep_fun.exp_mul
{Ω : Type u_1}
{m : measurable_space Ω}
{μ : measure_theory.measure Ω}
{X Y : Ω → ℝ}
(h_indep : probability_theory.indep_fun X Y μ)
(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 : probability_theory.indep_fun X Y μ)
(hX : measure_theory.ae_strongly_measurable (λ (ω : Ω), rexp (t * X ω)) μ)
(hY : measure_theory.ae_strongly_measurable (λ (ω : Ω), rexp (t * Y ω)) μ) :
probability_theory.mgf (X + Y) μ t = probability_theory.mgf X μ t * probability_theory.mgf Y μ t
theorem
probability_theory.indep_fun.mgf_add'
{Ω : Type u_1}
{m : measurable_space Ω}
{μ : measure_theory.measure Ω}
{t : ℝ}
{X Y : Ω → ℝ}
(h_indep : probability_theory.indep_fun X Y μ)
(hX : measure_theory.ae_strongly_measurable X μ)
(hY : measure_theory.ae_strongly_measurable Y μ) :
probability_theory.mgf (X + Y) μ t = probability_theory.mgf X μ t * probability_theory.mgf Y μ t
theorem
probability_theory.indep_fun.cgf_add
{Ω : Type u_1}
{m : measurable_space Ω}
{μ : measure_theory.measure Ω}
{t : ℝ}
{X Y : Ω → ℝ}
(h_indep : probability_theory.indep_fun X Y μ)
(h_int_X : measure_theory.integrable (λ (ω : Ω), rexp (t * X ω)) μ)
(h_int_Y : measure_theory.integrable (λ (ω : Ω), rexp (t * Y ω)) μ) :
probability_theory.cgf (X + Y) μ t = probability_theory.cgf X μ t + probability_theory.cgf Y μ t
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 : probability_theory.indep_fun X Y μ)
(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 : ℝ}
[measure_theory.is_probability_measure μ]
{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 : ℝ}
[measure_theory.is_probability_measure μ]
{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 : ι), probability_theory.mgf (X i) μ t)
theorem
probability_theory.Indep_fun.cgf_sum
{Ω : Type u_1}
{ι : Type u_2}
{m : measurable_space Ω}
{μ : measure_theory.measure Ω}
{t : ℝ}
[measure_theory.is_probability_measure μ]
{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 : ι), probability_theory.cgf (X i) μ t)
theorem
probability_theory.measure_ge_le_exp_mul_mgf
{Ω : Type u_1}
{m : measurable_space Ω}
{X : Ω → ℝ}
{μ : measure_theory.measure Ω}
{t : ℝ}
[measure_theory.is_finite_measure μ]
(ε : ℝ)
(ht : 0 ≤ t)
(h_int : measure_theory.integrable (λ (ω : Ω), rexp (t * X ω)) μ) :
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 : ℝ}
[measure_theory.is_finite_measure μ]
(ε : ℝ)
(ht : t ≤ 0)
(h_int : measure_theory.integrable (λ (ω : Ω), rexp (t * X ω)) μ) :
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 : ℝ}
[measure_theory.is_finite_measure μ]
(ε : ℝ)
(ht : 0 ≤ t)
(h_int : measure_theory.integrable (λ (ω : Ω), rexp (t * X ω)) μ) :
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 : ℝ}
[measure_theory.is_finite_measure μ]
(ε : ℝ)
(ht : t ≤ 0)
(h_int : measure_theory.integrable (λ (ω : Ω), rexp (t * X ω)) μ) :
Chernoff bound on the lower tail of a real random variable.