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.

source

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 ∂μ

Instances For

source

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

Instances For

source

@[simp]

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

moment 0 p μ = 0

source

@[simp]

theorem ProbabilityTheory.moment_zero_measure {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {p : ℕ} :

moment X p 0 = 0

source

@[simp]

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

centralMoment 0 p μ = 0

source

@[simp]

theorem ProbabilityTheory.centralMoment_zero_measure {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {p : ℕ} :

centralMoment X p 0 = 0

source

theorem ProbabilityTheory.centralMoment_one' {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (h_int : MeasureTheory.Integrable X μ) :

centralMoment X 1 μ = (1 - (μ Set.univ).toReal) * ∫ (x : Ω), X x ∂μ

source

@[simp]

theorem ProbabilityTheory.centralMoment_one {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsZeroOrProbabilityMeasure μ] :

centralMoment X 1 μ = 0

source

theorem ProbabilityTheory.centralMoment_two_eq_variance {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (hX : AEMeasurable X μ) :

centralMoment X 2 μ = variance X μ

source

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 ∂μ

Instances For

source

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)

Instances For

source

@[simp]

theorem ProbabilityTheory.mgf_zero_fun {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} :

mgf 0 μ t = (μ Set.univ).toReal

source

@[simp]

theorem ProbabilityTheory.cgf_zero_fun {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} :

cgf 0 μ t = Real.log (μ Set.univ).toReal

source

@[simp]

theorem ProbabilityTheory.mgf_zero_measure {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} :

mgf X 0 = 0

source

@[simp]

theorem ProbabilityTheory.cgf_zero_measure {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} :

cgf X 0 = 0

source

@[simp]

theorem ProbabilityTheory.mgf_const' {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} (c : ℝ) :

mgf (fun (x : Ω) => c) μ t = (μ Set.univ).toReal * Real.exp (t * c)

source

theorem ProbabilityTheory.mgf_const {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} (c : ℝ) [MeasureTheory.IsProbabilityMeasure μ] :

mgf (fun (x : Ω) => c) μ t = Real.exp (t * c)

source

@[simp]

theorem ProbabilityTheory.cgf_const' {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hμ : μ ≠ 0) (c : ℝ) :

cgf (fun (x : Ω) => c) μ t = Real.log (μ Set.univ).toReal + t * c

source

@[simp]

theorem ProbabilityTheory.cgf_const {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (c : ℝ) :

cgf (fun (x : Ω) => c) μ t = t * c

source

@[simp]

theorem ProbabilityTheory.mgf_zero' {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} :

mgf X μ 0 = (μ Set.univ).toReal

source

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

mgf X μ 0 = 1

source

theorem ProbabilityTheory.cgf_zero' {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} :

cgf X μ 0 = Real.log (μ Set.univ).toReal

source

@[simp]

theorem ProbabilityTheory.cgf_zero {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsZeroOrProbabilityMeasure μ] :

cgf X μ 0 = 0

source

theorem ProbabilityTheory.mgf_undef {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (hX : ¬MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) :

mgf X μ t = 0

source

theorem ProbabilityTheory.cgf_undef {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (hX : ¬MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) :

cgf X μ t = 0

source

theorem ProbabilityTheory.mgf_nonneg {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} :

0 ≤ mgf X μ t

source

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 < mgf X μ t

source

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 < mgf X μ t

source

theorem ProbabilityTheory.mgf_pos_iff {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} [hμ : NeZero μ] :

0 < mgf X μ t ↔ MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ

source

theorem ProbabilityTheory.exp_cgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} [hμ : NeZero μ] (hX : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) :

Real.exp (cgf X μ t) = mgf X μ t

source

@[deprecated ProbabilityTheory.exp_cgf (since := "2025-03-08")]

theorem ProbabilityTheory.exp_cgf_of_neZero {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} [hμ : NeZero μ] (hX : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) :

Real.exp (cgf X μ t) = mgf X μ t

Alias of ProbabilityTheory.exp_cgf.

source

theorem ProbabilityTheory.mgf_map {Ω : Type u_1} {m : MeasurableSpace Ω} {Ω' : Type u_3} {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω'} {Y : Ω' → Ω} {X : Ω → ℝ} (hY : AEMeasurable Y μ) {t : ℝ} (hX : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * X ω)) (MeasureTheory.Measure.map Y μ)) :

mgf X (MeasureTheory.Measure.map Y μ) t = mgf (X ∘ Y) μ t

source

theorem ProbabilityTheory.mgf_id_map {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (hX : AEMeasurable X μ) :

mgf id (MeasureTheory.Measure.map X μ) = mgf X μ

source

theorem ProbabilityTheory.mgf_congr {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} {Y : Ω → ℝ} (h : X =ᵐ[μ] Y) :

mgf X μ t = mgf Y μ t

source

theorem ProbabilityTheory.mgf_congr_identDistrib {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {Ω' : Type u_3} {mΩ' : MeasurableSpace Ω'} {μ' : MeasureTheory.Measure Ω'} {Y : Ω' → ℝ} (h : IdentDistrib X Y μ μ') :

mgf X μ = mgf Y μ'

source

theorem ProbabilityTheory.mgf_neg {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} :

mgf (-X) μ t = mgf X μ (-t)

source

theorem ProbabilityTheory.cgf_neg {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} :

cgf (-X) μ t = cgf X μ (-t)

source

theorem ProbabilityTheory.mgf_smul_left {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (α : ℝ) :

mgf (α • X) μ t = mgf X μ (α * t)

source

theorem ProbabilityTheory.mgf_const_add {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (α : ℝ) :

mgf (fun (ω : Ω) => α + X ω) μ t = Real.exp (t * α) * mgf X μ t

source

theorem ProbabilityTheory.mgf_add_const {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (α : ℝ) :

mgf (fun (ω : Ω) => X ω + α) μ t = mgf X μ t * Real.exp (t * α)

source

theorem ProbabilityTheory.mgf_mono_of_nonneg {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} {Y : Ω → ℝ} (hXY : X ≤ᵐ[μ] Y) (ht : 0 ≤ t) (htY : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * Y ω)) μ) :

mgf X μ t ≤ mgf Y μ t

The moment generating function is monotone in the random variable for t ≥ 0.

source

theorem ProbabilityTheory.mgf_anti_of_nonpos {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} {Y : Ω → ℝ} (hXY : X ≤ᵐ[μ] Y) (ht : t ≤ 0) (htX : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) :

mgf Y μ t ≤ mgf X μ t

The moment generating function is antitone in the random variable for t ≤ 0.

source

theorem ProbabilityTheory.IndepFun.exp_mul {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ) (s t : ℝ) :

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.

source

theorem ProbabilityTheory.IndepFun.mgf_add {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ) (hX : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * X ω)) μ) (hY : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * Y ω)) μ) :

mgf (X + Y) μ t = mgf X μ t * mgf Y μ t

source

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

mgf (X + Y) μ t = mgf X μ t * mgf Y μ t

source

theorem ProbabilityTheory.IndepFun.cgf_add {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ) (h_int_X : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) (h_int_Y : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * Y ω)) μ) :

cgf (X + Y) μ t = cgf X μ t + cgf Y μ t

source

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) ω)) μ

source

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 * (∑ i ∈ s, X i) ω)) μ

source

theorem ProbabilityTheory.IndepFun.integrable_exp_mul_add {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X Y : Ω → ℝ} (h_indep : 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) ω)) μ

source

theorem ProbabilityTheory.iIndepFun.integrable_exp_mul_sum {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → ℝ} (h_indep : iIndepFun 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 * (∑ i ∈ s, X i) ω)) μ

source

theorem ProbabilityTheory.iIndepFun.mgf_sum {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (s : Finset ι) :

mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t

source

theorem ProbabilityTheory.iIndepFun.cgf_sum {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ) (h_meas : ∀ (i : ι), Measurable (X i)) {s : Finset ι} (h_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X i ω)) μ) :

cgf (∑ i ∈ s, X i) μ t = ∑ i ∈ s, cgf (X i) μ t

source

theorem ProbabilityTheory.mgf_congr_of_identDistrib {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (X : Ω → ℝ) {Ω' : Type u_3} {m' : MeasurableSpace Ω'} {μ' : MeasureTheory.Measure Ω'} (X' : Ω' → ℝ) (hident : IdentDistrib X X' μ μ') (t : ℝ) :

mgf X μ t = mgf X' μ' t

source

theorem ProbabilityTheory.mgf_sum_of_identDistrib {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {s : Finset ι} {j : ι} (h_meas : ∀ (i : ι), Measurable (X i)) (h_indep : iIndepFun X μ) (hident : ∀ i ∈ s, ∀ j ∈ s, IdentDistrib (X i) (X j) μ μ) (hj : j ∈ s) (t : ℝ) :

mgf (∑ i ∈ s, X i) μ t = mgf (X j) μ t ^ s.card

source

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 * ε) * mgf X μ t

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

source

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 * ε) * mgf X μ t

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

source

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 * ε + cgf X μ t)

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

source

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 * ε + cgf X μ t)

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

source

theorem ProbabilityTheory.mgf_dirac {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {x : ℝ} (hX : MeasureTheory.Measure.map X μ = MeasureTheory.Measure.dirac x) (t : ℝ) :

mgf X μ t = Real.exp (x * t)

source

theorem ProbabilityTheory.mgf_dirac' {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {t : ℝ} [MeasurableSingletonClass Ω] {ω : Ω} :

mgf X (MeasureTheory.Measure.dirac ω) t = Real.exp (t * X ω)

source

theorem ProbabilityTheory.aemeasurable_exp_mul {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (t : ℝ) (hX : AEMeasurable X μ) :

MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * X ω)) μ

source

theorem ProbabilityTheory.integrable_exp_mul_of_le {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} (t b : ℝ) (ht : 0 ≤ t) (hX : AEMeasurable X μ) (hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b) :

MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ

Documentation

Mathlib.Probability.Moments.Basic

Moments and moment generating function #

Main definitions #

Main results #