mathlib documentation

probability.moments

Moments and moment generating function #

Main definitions #

Main results #

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) :
@[simp]
theorem probability_theory.central_moment_zero {Ω : Type u_1} {m : measurable_space Ω} {p : } {μ : measure_theory.measure Ω} (hp : p 0) :
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.mgf_zero_measure {Ω : Type u_1} {m : measurable_space Ω} {X : Ω → } {t : } :
@[simp]
theorem probability_theory.cgf_zero_measure {Ω : Type u_1} {m : measurable_space Ω} {X : Ω → } {t : } :
@[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 * real.exp (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 = real.exp (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 : ) :
probability_theory.cgf (λ (_x : Ω), c) μ t = real.log (μ set.univ).to_real + t * 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 Ω} :
@[simp]
@[simp]
theorem probability_theory.cgf_zero' {Ω : Type u_1} {m : measurable_space Ω} {X : Ω → } {μ : measure_theory.measure Ω} :
@[simp]
theorem probability_theory.mgf_undef {Ω : Type u_1} {m : measurable_space Ω} {X : Ω → } {μ : measure_theory.measure Ω} {t : } (hX : ¬measure_theory.integrable (λ (ω : Ω), real.exp (t * X ω)) μ) :
theorem probability_theory.cgf_undef {Ω : Type u_1} {m : measurable_space Ω} {X : Ω → } {μ : measure_theory.measure Ω} {t : } (hX : ¬measure_theory.integrable (λ (ω : Ω), real.exp (t * X ω)) μ) :
theorem probability_theory.mgf_nonneg {Ω : Type u_1} {m : measurable_space Ω} {X : Ω → } {μ : measure_theory.measure Ω} {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 (λ (ω : Ω), real.exp (t * X ω)) μ) :
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 (λ (ω : Ω), real.exp (t * X ω)) μ) :
theorem probability_theory.mgf_neg {Ω : Type u_1} {m : measurable_space Ω} {X : Ω → } {μ : measure_theory.measure Ω} {t : } :
theorem probability_theory.cgf_neg {Ω : Type u_1} {m : measurable_space Ω} {X : Ω → } {μ : measure_theory.measure Ω} {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 (λ (ω : Ω), real.exp (s * X ω)) (λ (ω : Ω), real.exp (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 μ) (h_int_X : measure_theory.integrable (λ (ω : Ω), real.exp (t * X ω)) μ) (h_int_Y : measure_theory.integrable (λ (ω : Ω), real.exp (t * Y ω)) μ) :
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 (λ (ω : Ω), real.exp (t * X ω)) μ) (h_int_Y : measure_theory.integrable (λ (ω : Ω), real.exp (t * Y ω)) μ) :
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 (λ (ω : Ω), real.exp (t * X ω)) μ) (h_int_Y : measure_theory.integrable (λ (ω : Ω), real.exp (t * Y ω)) μ) :
measure_theory.integrable (λ (ω : Ω), real.exp (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 smeasure_theory.integrable (λ (ω : Ω), real.exp (t * X i ω)) μ) :
measure_theory.integrable (λ (ω : Ω), real.exp (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 ι} (h_int : ∀ (i : ι), i smeasure_theory.integrable (λ (ω : Ω), real.exp (t * X i ω)) μ) :
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 smeasure_theory.integrable (λ (ω : Ω), real.exp (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 (λ (ω : Ω), real.exp (t * X ω)) μ) :
(μ {ω : Ω | ε X ω}).to_real real.exp (-t * ε) * probability_theory.mgf X μ 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 : } [measure_theory.is_finite_measure μ] (ε : ) (ht : t 0) (h_int : measure_theory.integrable (λ (ω : Ω), real.exp (t * X ω)) μ) :
(μ {ω : Ω | X ω ε}).to_real real.exp (-t * ε) * probability_theory.mgf X μ 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 : } [measure_theory.is_finite_measure μ] (ε : ) (ht : 0 t) (h_int : measure_theory.integrable (λ (ω : Ω), real.exp (t * X ω)) μ) :
(μ {ω : Ω | ε X ω}).to_real real.exp (-t * ε + probability_theory.cgf X μ 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 : } [measure_theory.is_finite_measure μ] (ε : ) (ht : t 0) (h_int : measure_theory.integrable (λ (ω : Ω), real.exp (t * X ω)) μ) :
(μ {ω : Ω | X ω ε}).to_real real.exp (-t * ε + probability_theory.cgf X μ t)

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