Analytic continuation of a moment-generating function

The moment-generating function of a real random variable X is the restriction to the real axis of ProbabilityTheory.complexMGF X μ, which is analytic on the vertical strip over the interior of the exponential-integrability domain. A closed form for mgf X μ on a real interval therefore determines complexMGF X μ on the whole strip above it, as soon as the proposed formula is itself analytic there. For an a.e.-measurable X, complexMGF X μ on the imaginary axis is the characteristic function of the law of X, so this is the standard route from a moment-generating function to a characteristic function.

TauCeti.eqOn_complexMGF_of_eqOn_mgf packages that continuation step, and MeasureTheory.charFun_eq_complexMGF_inner supplies its vector-valued end point: on a type carrying a real-valued pairing ⟪·, ·⟫, the characteristic function at t is the value at Complex.I of the complex moment-generating function of the statistic x ↦ ⟪x, t⟫. The bulk of the file carries the continuation out for the closed form

mgf X μ t = ∏ j, (1 - 2 * t * lam j) ^ (-a j),

a product of real powers of a pencil of linear factors. This is the shape taken by the trace statistic of a Wishart matrix and, more generally, by any weighted sum of independent scaled chi-squared variables with weights lam j. On the imaginary axis the answer must be written as an exponential of a sum of principal logarithms rather than as a single complex power of the product: multiplying the factors before taking the logarithm can cross the branch cut.

Main results

• TauCeti.eqOn_complexMGF_of_eqOn_mgf: an analytic function agreeing with mgf X μ on an open convex set of reals inside the exponential-integrability domain agrees with complexMGF X μ on the vertical strip above that set.
• TauCeti.complexMGF_eq_exp_of_mgf_eq_prod_rpow: the value of complexMGF X μ at any point of the strip on which the pencil 1 - 2 * z.re * lam j is positive.
• TauCeti.complexMGF_I_eq_exp_of_mgf_eq_prod_rpow: its value at Complex.I, which for a measurable X is the characteristic function of the law of X at 1.
• MeasureTheory.charFun_eq_complexMGF_inner: for a real-valued pairing ⟪·, ·⟫, the characteristic function at t is the value at Complex.I of the complex moment-generating function of the statistic x ↦ ⟪x, t⟫.

References

• E. Mayerhofer, Reforming the Wishart characteristic function, arXiv:1901.09347, for the branch analysis that forces the sum-of-logarithms form.
• The identity-theorem argument follows ProbabilityTheory.eqOn_complexMGF_of_mgf' in Mathlib/Probability/Moments/ComplexMGF.lean.

Continuation from a real interval to a vertical strip

theorem TauCeti.eqOn_complexMGF_of_eqOn_mgf {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {s : Set ℝ} {g : ℂ → ℂ} (hs : IsOpen s) (hconv : Convex ℝ s) (hsub : s ⊆ ProbabilityTheory.integrableExpSet X μ) (hg : AnalyticOnNhd ℂ g {z : ℂ | z.re ∈ s}) (hmgf : ∀ t ∈ s, g ↑t = ↑(ProbabilityTheory.mgf X μ t)) : Set.EqOn (ProbabilityTheory.complexMGF X μ) g {z : ℂ | z.re ∈ s}

Analytic continuation of a moment-generating function. If g is analytic on the vertical strip over an open convex set s of reals on which the exponential moments of X are finite, and g agrees with mgf X μ on s, then g agrees with complexMGF X μ on the whole strip.

A product of real powers of a linear pencil

theorem TauCeti.complexMGF_eq_exp_of_mgf_eq_prod_rpow {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {ι : Type u_2} [Fintype ι] (lam a : ι → ℝ) (hmgf : ∀ (t : ℝ), (∀ (j : ι), 0 < 1 - 2 * t * lam j) → ProbabilityTheory.mgf X μ t = ∏ j : ι, (1 - 2 * t * lam j) ^ (-a j)) {z : ℂ} (hz : ∀ (j : ι), 0 < 1 - 2 * z.re * lam j) : ProbabilityTheory.complexMGF X μ z = Complex.exp (-∑ j : ι, ↑(a j) * Complex.log (1 - 2 * z * ↑(lam j)))

Continuation of a product-of-powers moment-generating function. If the moment-generating function of X is the product ∏ j, (1 - 2 * t * lam j) ^ (-a j) wherever every factor of the pencil is positive, then complexMGF X μ is given at every point of the corresponding vertical strip by the exponential of minus the sum of the principal logarithms.

The value is not a principal complex power of ∏ j, (1 - 2 * z * lam j): collecting the factors before taking the logarithm can cross the branch cut.

theorem TauCeti.complexMGF_I_eq_exp_of_mgf_eq_prod_rpow {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {ι : Type u_2} [Fintype ι] (lam a : ι → ℝ) (hmgf : ∀ (t : ℝ), (∀ (j : ι), 0 < 1 - 2 * t * lam j) → ProbabilityTheory.mgf X μ t = ∏ j : ι, (1 - 2 * t * lam j) ^ (-a j)) : ProbabilityTheory.complexMGF X μ Complex.I = Complex.exp (-∑ j : ι, ↑(a j) * Complex.log (1 - 2 * Complex.I * ↑(lam j)))

The value of complexMGF X μ at Complex.I, for a moment-generating function that is a product of real powers of a linear pencil. Every factor 1 - 2 * I * lam j has real part 1, so the principal logarithms are unambiguous.

For a measurable X this is the characteristic function of the law of X at 1, by ProbabilityTheory.complexMGF_mul_I.

The characteristic function of a real-valued pairing

theorem MeasureTheory.charFun_eq_complexMGF_inner {E : Type u_1} [Inner ℝ E] [MeasurableSpace E] (μ : Measure E) (t : E) : charFun μ t = ProbabilityTheory.complexMGF (fun (x : E) => inner ℝ x t) μ Complex.I

For a type carrying a real-valued pairing ⟪·, ·⟫, the characteristic function at t is the value at Complex.I of the complex moment-generating function of the statistic x ↦ ⟪x, t⟫. This is the vector-valued companion of ProbabilityTheory.complexMGF_id_mul_I, and it is how a closed form for the moment-generating function of such a statistic turns into a characteristic function. No inner-product axioms are needed: both sides read off the same Inner ℝ E instance.