Moment determinacy of finite measures with finite exponential moments

A finite measure on ℝ whose exponential moments are finite in a neighbourhood of the origin is determined by its sequence of polynomial moments ∫ xⁿ dμ. This is the analytic engine behind the completeness step (B1) of the OrthogonalL2Bases roadmap (TauCetiRoadmap/OrthogonalL2Bases/README.md, Part B1 — Completeness toolkit (moment determinacy)): the roadmap's ae_eq_zero_of_forall_moment_eq_zero-style lemmas rest on the fact that "vanishing moments" pins a distribution down, which for finite measures is exactly the determinacy result proved here.

The mechanism is the one the roadmap describes — the (complex) moment-generating function is analytic on a strip around the imaginary axis, and its Taylor coefficients at 0 are the moments, so matching moments force the two functions to agree, hence the characteristic functions agree and the measures coincide. The proof stays inside Mathlib's ProbabilityTheory.complexMGF / MeasureTheory.charFun API:

• ProbabilityTheory.analyticAt_complexMGF and analyticOnNhd_complexMGF supply the analyticity on the strip {z | z.re ∈ interior (integrableExpSet id μ)};
• ProbabilityTheory.iteratedDeriv_complexMGF identifies the n-th derivative at 0 with the n-th complex moment;
• the identity principle (analyticOrderAt_eq_top, AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq) propagates equality from 0 to the whole strip, in particular to the imaginary axis;
• ProbabilityTheory.complexMGF_id_mul_I turns the imaginary-axis values into charFun, and MeasureTheory.Measure.ext_of_charFun concludes.

Both routes share one strip-propagation core, adapted from Mathlib's ProbabilityTheory.eqOn_complexMGF_of_mgf' (Mathlib/Probability/Moments/ComplexMGF.lean): it reuses the same analyticity strip and the same convex_integrableExpSet.interior.…linear_preimage Complex.reLm |>.isPreconnected identity-principle idiom. That file's ## TODO note ("once we know that equal mgf implies equal distributions …") records the determinacy fact as an open gap in Mathlib; the results here complete it for finite measures, both via the polynomial-moment route and directly from the moment-generating function.

This file also records determinacy directly from the moment-generating function: a measure on ℝ with finite exponential moments near 0 is determined among finite measures by the values its moment-generating function takes on an arbitrarily small neighbourhood of the origin.

Main declarations

• TauCeti.charFun_eq_of_forall_integral_pow_eq: matching moments (and finite exponential moments near 0) give equal characteristic functions.
• TauCeti.Measure.ext_of_forall_integral_pow_eq: matching moments determine a finite measure on ℝ.
• TauCeti.Measure.ext_of_forall_integral_pow_eq_of_exists_integrable_exp: the same conclusion from the roadmap's exponential-moment hypothesis ∃ a > 0, Integrable (fun x => exp (a * |x|)) μ, which already puts 0 in the interior of the integrability strip. This is the form the completeness argument consumes: the hypothesis holds for Gaussian decay and automatically for compactly supported measures.
• TauCeti.charFun_eq_of_mgf_eq and TauCeti.Measure.ext_of_mgf: the same two conclusions from an equality of moment-generating functions near 0 instead of an equality of moments.

The shared strip-propagation core

Determinacy from the moment-generating function

theorem TauCeti.charFun_eq_of_mgf_eq {μ ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure ν] (hμ : 0 ∈ interior (ProbabilityTheory.integrableExpSet id μ)) (hmgf : ProbabilityTheory.mgf id μ =ᶠ[nhds 0] ProbabilityTheory.mgf id ν) : MeasureTheory.charFun μ = MeasureTheory.charFun ν

Determinacy at the level of characteristic functions, from the moment-generating function. Two measures on ℝ, one with finite exponential moments near 0 and the other finite, whose moment-generating functions agree on a neighbourhood of 0, have the same characteristic function.

theorem TauCeti.Measure.ext_of_mgf {μ ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure ν] (hμ : 0 ∈ interior (ProbabilityTheory.integrableExpSet id μ)) (hmgf : ProbabilityTheory.mgf id μ =ᶠ[nhds 0] ProbabilityTheory.mgf id ν) : μ = ν

A finite measure on ℝ with finite exponential moments near 0 is determined by its moment-generating function near 0. This is the determinacy statement recorded as a TODO in Mathlib's Mathlib/Probability/Moments/ComplexMGF.lean.

The strip hypothesis is asked of one measure only: matching the moment-generating functions near 0 matches the two total masses, and forces the second measure to have the exponential moments of the first at every rate near 0.

Determinacy from the moments

theorem TauCeti.charFun_eq_of_forall_integral_pow_eq {μ ν : MeasureTheory.Measure ℝ} (hμ : 0 ∈ interior (ProbabilityTheory.integrableExpSet id μ)) (hν : 0 ∈ interior (ProbabilityTheory.integrableExpSet id ν)) (hmom : ∀ (n : ℕ), ∫ (x : ℝ), x ^ n ∂μ = ∫ (x : ℝ), x ^ n ∂ν) : MeasureTheory.charFun μ = MeasureTheory.charFun ν

Moment determinacy at the level of characteristic functions. If two measures on ℝ have finite exponential moments near 0 (so their complex moment-generating functions are analytic on a strip about the imaginary axis) and agree on every polynomial moment ∫ xⁿ, then their characteristic functions coincide.

theorem TauCeti.Measure.ext_of_forall_integral_pow_eq {μ ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hμ : 0 ∈ interior (ProbabilityTheory.integrableExpSet id μ)) (hν : 0 ∈ interior (ProbabilityTheory.integrableExpSet id ν)) (hmom : ∀ (n : ℕ), ∫ (x : ℝ), x ^ n ∂μ = ∫ (x : ℝ), x ^ n ∂ν) : μ = ν

Moment determinacy for finite measures on ℝ. A finite measure on ℝ with finite exponential moments near 0 is determined by its polynomial moments ∫ xⁿ. Combines charFun_eq_of_forall_integral_pow_eq with MeasureTheory.Measure.ext_of_charFun.

theorem TauCeti.Measure.ext_of_forall_integral_pow_eq_of_exists_integrable_exp {μ ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hμ : ∃ (a : ℝ), 0 < a ∧ MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (a * |x|)) μ) (hν : ∃ (a : ℝ), 0 < a ∧ MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (a * |x|)) ν) (hmom : ∀ (n : ℕ), ∫ (x : ℝ), x ^ n ∂μ = ∫ (x : ℝ), x ^ n ∂ν) : μ = ν

Moment determinacy, exponential-moment form (the roadmap's B1 hypothesis). A finite measure on ℝ for which some exponential moment ∫ e^{a|x|} dμ with a > 0 is finite is determined by its polynomial moments. This is the form the completeness argument consumes: the hypothesis holds for Gaussian decay and automatically for compactly supported measures.