Derivatives of Moment and Cumulant Generating Functions

Auxiliary results for differentiating exponential moments, tilted expectations, and cumulant generating functions.

Main definitions

This module extends Mathlib's existing moment-generating and tilted-measure definitions.

Main results

• ProbabilityTheory.tilt_first_deriv: first derivative of an exponential moment.
• ProbabilityTheory.tilt_second_deriv: second derivative of an exponential moment.
• ProbabilityTheory.cgf_deriv_one: first derivative of the cumulant generating function.
• ProbabilityTheory.cgf_deriv_two: second derivative of the cumulant generating function.

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

theorem LeanPool.ProbabilityTheory.integrable_expt {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} (t b : ℝ) (ht : t > 0) (hX : AEMeasurable X μ) (hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ

theorem LeanPool.ProbabilityTheory.integrable_expt_bound {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {t a b : ℝ} (hX : AEMeasurable X μ) (h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ

theorem LeanPool.ProbabilityTheory.tilt_var_bound {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (a b t : ℝ) {X : Ω → ℝ} (h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b) (hX : AEMeasurable X μ) : ProbabilityTheory.variance X (μ.tilted fun (ω : Ω) => t * X ω) ≤ ((b - a) / 2) ^ 2

theorem LeanPool.ProbabilityTheory.integrable_bounded {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (a b : ℝ) {X : Ω → ℝ} (hX : AEMeasurable X μ) (h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b) : MeasureTheory.Integrable X μ

theorem LeanPool.ProbabilityTheory.tilt_first_deriv {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (t a b : ℝ) {X : Ω → ℝ} (hX : AEMeasurable X μ) (h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b) : have g := fun (t : ℝ) => ProbabilityTheory.mgf X μ t; have g' := fun (t : ℝ) => ∫ (x : Ω), (fun (ω : Ω) => Real.exp (t * X ω) * X ω) x ∂μ; HasDerivAt g (g' t) t

Derivation of mgf X μ t is μ[exp (t * X ω) * X ω]. In order to deal with the differentiation of parametric integrals, hasDerivAt_integral_of_dominated_loc_of_deriv_le are used in the proof.

theorem LeanPool.ProbabilityTheory.tilt_second_deriv {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (t a b : ℝ) {X : Ω → ℝ} (hX : AEMeasurable X μ) (h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b) : have g := fun (t : ℝ) => ∫ (x : Ω), (fun (ω : Ω) => Real.exp (t * X ω) * X ω) x ∂μ; have g' := fun (t : ℝ) => ∫ (x : Ω), (fun (ω : Ω) => Real.exp (t * X ω) * X ω ^ 2) x ∂μ; HasDerivAt g (g' t) t

Derivation of μ[fun ω ↦ rexp (t * X ω) * X ω] is μ[fun ω ↦ rexp (t * X ω) * X ω ^ 2]. In order to deal with the differentiation of parametric integrals, hasDerivAt_integral_of_dominated_loc_of_deriv_le are used in the proof.

theorem LeanPool.ProbabilityTheory.integrable_deriv_expt {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (t a b : ℝ) {X : Ω → ℝ} (hX : AEMeasurable X μ) (h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω) * X ω) μ

theorem LeanPool.ProbabilityTheory.integral_tilted {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (t : ℝ) (f : ℝ → ℝ) {X : Ω → ℝ} (hX : AEMeasurable X μ) : (∫ (x : Ω), (fun (ω : Ω) => f (X ω)) x ∂μ.tilted fun (ω : Ω) => t * X ω) = (∫ (x : Ω), (fun (ω : Ω) => Real.exp (t * X ω) * f (X ω)) x ∂μ) / ProbabilityTheory.mgf X μ t

Derivatives of cumulant

theorem LeanPool.ProbabilityTheory.cgf_deriv_one {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [NeZero μ] (a b : ℝ) {X : Ω → ℝ} (hX : AEMeasurable X μ) (h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b) : have f := fun (t : ℝ) => ProbabilityTheory.cgf X μ t; have f' := fun (t : ℝ) => ∫ (x : Ω), X x ∂μ.tilted fun (ω : Ω) => t * X ω; ∀ (x : ℝ), HasDerivAt f (f' x) x

First derivative of cumulant cgf X μ f. It can be described by exponential tilting.

theorem LeanPool.ProbabilityTheory.cgf_deriv_two {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [NeZero μ] (a b : ℝ) {X : Ω → ℝ} (hX : AEMeasurable X μ) (h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b) : have g' := fun (t : ℝ) => ∫ (x : Ω), X x ∂μ.tilted fun (ω : Ω) => t * X ω; have g'' := fun (t : ℝ) => (∫ (x : Ω), (X ^ 2) x ∂μ.tilted fun (ω : Ω) => t * X ω) - (∫ (x : Ω), X x ∂μ.tilted fun (ω : Ω) => t * X ω) ^ 2; ∀ (x : ℝ), HasDerivAt g' (g'' x) x

Second derivative of cumulant cgf X μ f.