mathlib3 documentation

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 #

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]
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]
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 * rexp (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 : ) :
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_undef {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {μ : measure_theory.measure Ω} {t : } (hX : ¬measure_theory.integrable (λ (ω : Ω), rexp (t * X ω)) μ) :
theorem probability_theory.cgf_undef {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {μ : measure_theory.measure Ω} {t : } (hX : ¬measure_theory.integrable (λ (ω : Ω), rexp (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 (λ (ω : Ω), rexp (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 (λ (ω : Ω), rexp (t * X ω)) μ) :
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 ω)) μ) :
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 ω)) μ) :
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 ω)) μ) :
(μ {ω : Ω | ε X ω}).to_real rexp (-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 (λ (ω : Ω), rexp (t * X ω)) μ) :
(μ {ω : Ω | X ω ε}).to_real rexp (-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 (λ (ω : Ω), rexp (t * X ω)) μ) :
(μ {ω : Ω | ε X ω}).to_real rexp (-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 (λ (ω : Ω), rexp (t * X ω)) μ) :
(μ {ω : Ω | X ω ε}).to_real rexp (-t * ε + probability_theory.cgf X μ t)

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