Results relating Measure.tilted to mgf and cgf

For a random variable X : Ω → ℝ and a measure μ, the tilted measure μ.tilted (t * X ·) is linked to the moment-generating function (mgf) and the cumulant-generating function (cgf) of X.

Main statements

• integral_tilted_mul_self: the integral of X against the tilted measure μ.tilted (t * X ·) is the first derivative of the cumulant-generating function of X at t. (μ.tilted (t * X ·))[X] = deriv (cgf X μ) t
• variance_tilted_mul: the variance of X under the tilted measure μ.tilted (t * X ·) is the second derivative of the cumulant-generating function of X at t. Var[X; μ.tilted (t * X ·)] = iteratedDeriv 2 (cgf X μ) t

Apply lemmas for tilted expressed with mgf or cgf.

theorem ProbabilityTheory.tilted_mul_apply_mgf' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} {s : Set Ω} (hs : MeasurableSet s) : (μ.tilted fun (x : Ω) => t * X x) s = ∫⁻ (a : Ω) in s, ENNReal.ofReal (Real.exp (t * X a) / mgf X μ t) ∂μ

theorem ProbabilityTheory.tilted_mul_apply_mgf {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} [MeasureTheory.SFinite μ] (s : Set Ω) : (μ.tilted fun (x : Ω) => t * X x) s = ∫⁻ (a : Ω) in s, ENNReal.ofReal (Real.exp (t * X a) / mgf X μ t) ∂μ

theorem ProbabilityTheory.tilted_mul_apply_cgf' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} {s : Set Ω} (hs : MeasurableSet s) (ht : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : (μ.tilted fun (x : Ω) => t * X x) s = ∫⁻ (a : Ω) in s, ENNReal.ofReal (Real.exp (t * X a - cgf X μ t)) ∂μ

theorem ProbabilityTheory.tilted_mul_apply_cgf {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} [MeasureTheory.SFinite μ] (s : Set Ω) (ht : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : (μ.tilted fun (x : Ω) => t * X x) s = ∫⁻ (a : Ω) in s, ENNReal.ofReal (Real.exp (t * X a - cgf X μ t)) ∂μ

theorem ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_mgf' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} {s : Set Ω} (hs : MeasurableSet s) : (μ.tilted fun (x : Ω) => t * X x) s = ENNReal.ofReal (∫ (a : Ω) in s, Real.exp (t * X a) / mgf X μ t ∂μ)

theorem ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_mgf {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} [MeasureTheory.SFinite μ] (s : Set Ω) : (μ.tilted fun (x : Ω) => t * X x) s = ENNReal.ofReal (∫ (a : Ω) in s, Real.exp (t * X a) / mgf X μ t ∂μ)

theorem ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_cgf' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} {s : Set Ω} (hs : MeasurableSet s) (ht : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : (μ.tilted fun (x : Ω) => t * X x) s = ENNReal.ofReal (∫ (a : Ω) in s, Real.exp (t * X a - cgf X μ t) ∂μ)

theorem ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_cgf {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} [MeasureTheory.SFinite μ] (s : Set Ω) (ht : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : (μ.tilted fun (x : Ω) => t * X x) s = ENNReal.ofReal (∫ (a : Ω) in s, Real.exp (t * X a - cgf X μ t) ∂μ)

Integral of tilted expressed with mgf or cgf.

theorem ProbabilityTheory.setIntegral_tilted_mul_eq_mgf' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : Ω → E) {s : Set Ω} (hs : MeasurableSet s) : (∫ (x : Ω) in s, g x ∂μ.tilted fun (x : Ω) => t * X x) = ∫ (x : Ω) in s, (Real.exp (t * X x) / mgf X μ t) • g x ∂μ

theorem ProbabilityTheory.setIntegral_tilted_mul_eq_mgf {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasureTheory.SFinite μ] (g : Ω → E) (s : Set Ω) : (∫ (x : Ω) in s, g x ∂μ.tilted fun (x : Ω) => t * X x) = ∫ (x : Ω) in s, (Real.exp (t * X x) / mgf X μ t) • g x ∂μ

theorem ProbabilityTheory.setIntegral_tilted_mul_eq_cgf' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : Ω → E) {s : Set Ω} (hs : MeasurableSet s) (ht : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : (∫ (x : Ω) in s, g x ∂μ.tilted fun (x : Ω) => t * X x) = ∫ (x : Ω) in s, Real.exp (t * X x - cgf X μ t) • g x ∂μ

theorem ProbabilityTheory.setIntegral_tilted_mul_eq_cgf {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasureTheory.SFinite μ] (g : Ω → E) (s : Set Ω) (ht : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : (∫ (x : Ω) in s, g x ∂μ.tilted fun (x : Ω) => t * X x) = ∫ (x : Ω) in s, Real.exp (t * X x - cgf X μ t) • g x ∂μ

theorem ProbabilityTheory.integral_tilted_mul_eq_mgf {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : Ω → E) : (∫ (ω : Ω), g ω ∂μ.tilted fun (x : Ω) => t * X x) = ∫ (ω : Ω), (Real.exp (t * X ω) / mgf X μ t) • g ω ∂μ

theorem ProbabilityTheory.integral_tilted_mul_eq_cgf {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : Ω → E) (ht : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : (∫ (ω : Ω), g ω ∂μ.tilted fun (x : Ω) => t * X x) = ∫ (ω : Ω), Real.exp (t * X ω - cgf X μ t) • g ω ∂μ

theorem ProbabilityTheory.integral_tilted_mul_self {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)) : (∫ (x : Ω), X x ∂μ.tilted fun (x : Ω) => t * X x) = deriv (cgf X μ) t

The integral of X against the tilted measure μ.tilted (t * X ·) is the first derivative of the cumulant-generating function of X at t.

theorem ProbabilityTheory.memLp_tilted_mul {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)) (p : NNReal) : MeasureTheory.MemLp X (↑p) (μ.tilted fun (x : Ω) => t * X x)

theorem ProbabilityTheory.variance_tilted_mul {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)) : variance X (μ.tilted fun (x : Ω) => t * X x) = iteratedDeriv 2 (cgf X μ) t

The variance of X under the tilted measure μ.tilted (t * X ·) is the second derivative of the cumulant-generating function of X at t.