The complex-valued moment generating function

The moment generating function (mgf) is t : ℝ ↦ μ[fun ω ↦ rexp (t * X ω)]. It can be extended to a complex function z : ℂ ↦ μ[fun ω ↦ cexp (z * X ω)], which we call complexMGF X μ. That function is holomorphic on the vertical strip with base the interior of the interval of definition of the mgf. On the vertical line that goes through 0, complexMGF X μ is equal to the characteristic function. This allows us to link properties of the characteristic function and the mgf (mostly deducing properties of the mgf from those of the characteristic function).

Main definitions

• complexMGF X μ: the function z : ℂ ↦ μ[fun ω ↦ cexp (z * X ω)].

Main results

• complexMGF_ofReal: for x : ℝ, complexMGF X μ x = mgf X μ x.

• hasDerivAt_complexMGF: for all z : ℂ such that the real part z.re belongs to the interior of the interval of definition of the mgf, complexMGF X μ is differentiable at z with derivative μ[X * exp (z * X)].

• differentiableOn_complexMGF: complexMGF X μ is holomorphic on the vertical strip {z | z.re ∈ interior (integrableExpSet X μ)}.

• analyticOn_complexMGF: complexMGF X μ is analytic on the vertical strip {z | z.re ∈ interior (integrableExpSet X μ)}.

• eqOn_complexMGF_of_mgf: if two random variables have the same moment generating function, then they have the same complexMGF on the vertical strip {z | z.re ∈ interior (integrableExpSet X μ)}. Once we know that equal mgf implies equal distributions, we will be able to show that the complexMGF are equal everywhere, not only on the strip. This lemma will be used in the proof of the equality of distributions.

TODO

Once we have a definition for the characteristic function, we will be able to prove the following.

• x : ℝ ↦ complexMGF X μ (I * x) is equal to the characteristic function of the random variable X.
• As a consequence, if two random variables have same mgf, then they have the same characteristic function and the same distribution.

noncomputable def ProbabilityTheory.complexMGF {Ω : Type u_1} {m : MeasurableSpace Ω} (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) (z : ℂ) : ℂ

Complex extension of the moment generating function.

Equations

• ProbabilityTheory.complexMGF X μ z = ∫ (x : Ω), (fun (ω : Ω) => Complex.exp (z * ↑(X ω))) x ∂μ

theorem ProbabilityTheory.complexMGF_undef {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ} (hX : AEMeasurable X μ) (h : ¬MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (z.re * X ω)) μ) : complexMGF X μ z = 0

theorem ProbabilityTheory.complexMGF_id_map {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (hX : AEMeasurable X μ) : complexMGF id (MeasureTheory.Measure.map X μ) = complexMGF X μ

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

theorem ProbabilityTheory.norm_complexMGF_le_mgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ} : ‖complexMGF X μ z‖ ≤ mgf X μ z.re

@[deprecated ProbabilityTheory.norm_complexMGF_le_mgf (since := "2025-02-17")]

theorem ProbabilityTheory.abs_complexMGF_le_mgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ} : ‖complexMGF X μ z‖ ≤ mgf X μ z.re

Alias of ProbabilityTheory.norm_complexMGF_le_mgf.

theorem ProbabilityTheory.complexMGF_ofReal {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (x : ℝ) : complexMGF X μ ↑x = ↑(mgf X μ x)

theorem ProbabilityTheory.re_complexMGF_ofReal {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (x : ℝ) : (complexMGF X μ ↑x).re = mgf X μ x

theorem ProbabilityTheory.re_complexMGF_ofReal' {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} : (fun (x : ℝ) => (complexMGF X μ ↑x).re) = mgf X μ

theorem ProbabilityTheory.hasDerivAt_integral_pow_mul_exp {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)) (n : ℕ) : HasDerivAt (fun (z : ℂ) => ∫ (x : Ω), (fun (ω : Ω) => ↑(X ω) ^ n * Complex.exp (z * ↑(X ω))) x ∂μ) (∫ (x : Ω), (fun (ω : Ω) => ↑(X ω) ^ (n + 1) * Complex.exp (z * ↑(X ω))) x ∂μ) z

For z : ℂ with z.re ∈ interior (integrableExpSet X μ), the derivative of the function z' ↦ μ[X ^ n * cexp (z' * X)] at z is μ[X ^ (n + 1) * cexp (z * X)].

theorem ProbabilityTheory.hasDerivAt_complexMGF {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)) : HasDerivAt (complexMGF X μ) (∫ (x : Ω), (fun (ω : Ω) => ↑(X ω) * Complex.exp (z * ↑(X ω))) x ∂μ) z

For all z : ℂ with z.re ∈ interior (integrableExpSet X μ), complexMGF X μ is differentiable at z with derivative μ[X * exp (z * X)].

theorem ProbabilityTheory.differentiableOn_complexMGF {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} : DifferentiableOn ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}

complexMGF X μ is holomorphic on the vertical strip {z | z.re ∈ interior (integrableExpSet X μ)}.

theorem ProbabilityTheory.analyticOnNhd_complexMGF {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}

theorem ProbabilityTheory.analyticOn_complexMGF {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} : AnalyticOn ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}

complexMGF X μ is analytic on the vertical strip {z | z.re ∈ interior (integrableExpSet X μ)}.

theorem ProbabilityTheory.analyticAt_complexMGF {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)) : AnalyticAt ℂ (complexMGF X μ) z

complexMGF X μ is analytic at any point z with z.re ∈ interior (integrableExpSet X μ).

Iterated derivatives of complexMGF

theorem ProbabilityTheory.hasDerivAt_iteratedDeriv_complexMGF {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)) (n : ℕ) : HasDerivAt (iteratedDeriv n (complexMGF X μ)) (∫ (x : Ω), (fun (ω : Ω) => ↑(X ω) ^ (n + 1) * Complex.exp (z * ↑(X ω))) x ∂μ) z

theorem ProbabilityTheory.iteratedDeriv_complexMGF {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)) (n : ℕ) : iteratedDeriv n (complexMGF X μ) z = ∫ (x : Ω), (fun (ω : Ω) => ↑(X ω) ^ n * Complex.exp (z * ↑(X ω))) x ∂μ

For z : ℂ with z.re ∈ interior (integrableExpSet X μ), the n-th derivative of the function complexMGF X μ at z is μ[X ^ n * cexp (z * X)].

We prove that if two random variables have the same mgf, then they also have the same complexMGF.

theorem ProbabilityTheory.integrableExpSet_eq_of_mgf' {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {Ω' : Type u_3} {mΩ' : MeasurableSpace Ω'} {Y : Ω' → ℝ} {μ' : MeasureTheory.Measure Ω'} (hXY : mgf X μ = mgf Y μ') (hμμ' : μ = 0 ↔ μ' = 0) : integrableExpSet X μ = integrableExpSet Y μ'

If two random variables have the same moment generating function then they have the same integrableExpSet.

theorem ProbabilityTheory.integrableExpSet_eq_of_mgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {Ω' : Type u_3} {mΩ' : MeasurableSpace Ω'} {Y : Ω' → ℝ} {μ' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure μ] (hXY : mgf X μ = mgf Y μ') : integrableExpSet X μ = integrableExpSet Y μ'

If two random variables have the same moment generating function then they have the same integrableExpSet.

theorem ProbabilityTheory.eqOn_complexMGF_of_mgf' {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {Ω' : Type u_3} {mΩ' : MeasurableSpace Ω'} {Y : Ω' → ℝ} {μ' : MeasureTheory.Measure Ω'} (hXY : mgf X μ = mgf Y μ') (hμμ' : μ = 0 ↔ μ' = 0) : Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}

If two random variables have the same moment generating function then they have the same complexMGF on the vertical strip {z | z.re ∈ interior (integrableExpSet X μ)}.

TODO: once we know that equal mgf implies equal distributions, we will be able to show that the complexMGF are equal everywhere, not only on the strip. This lemma will be used in the proof of the equality of distributions.

theorem ProbabilityTheory.eqOn_complexMGF_of_mgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {Ω' : Type u_3} {mΩ' : MeasurableSpace Ω'} {Y : Ω' → ℝ} {μ' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure μ] (hXY : mgf X μ = mgf Y μ') : Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}

If two random variables have the same moment generating function then they have the same complexMGF on the vertical strip {z | z.re ∈ interior (integrableExpSet X μ)}.