Existence of a law from convergent characteristic functions

A pointwise limit of characteristic functions of probability measures on a finite-dimensional real inner product space is itself a characteristic function, provided it is continuous at zero. The representing probability measure is unique, and the original sequence converges weakly to it. In particular, constructing approximating laws and computing their characteristic-function limit suffices to construct a limiting law; a candidate measure need not be supplied in advance.

exists_probabilityMeasure_of_tendsto_charFun supplies this existence form of Lévy's continuity theorem. It complements Mathlib's ProbabilityMeasure.tendsto_of_tendsto_charFun, whose input already includes a limiting probability measure. The proof uses Mathlib's isTightMeasureSet_of_tendsto_charFun and isCompact_closure_of_isTightMeasureSet to obtain a weak cluster limit, identifies its characteristic function by bounded-continuous integration, and then applies Mathlib's convergence and characteristic-function uniqueness theorems.

References

• P. Billingsley, Probability and Measure, third edition, Wiley, 1995, section 29 (the continuity theorem for characteristic functions).

theorem TauCeti.exists_probabilityMeasure_of_tendsto_charFun {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : ℕ → MeasureTheory.ProbabilityMeasure E} {f : E → ℂ} (hf : ContinuousAt f 0) (h : ∀ (t : E), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.charFun (↑(μ n)) t) Filter.atTop (nhds (f t))) : ∃! μ₀ : MeasureTheory.ProbabilityMeasure E, MeasureTheory.charFun ↑μ₀ = f ∧ Filter.Tendsto μ Filter.atTop (nhds μ₀)

Lévy's continuity theorem, including existence. If the characteristic functions of a sequence of probability measures converge pointwise to a function continuous at zero, there is a unique probability measure with that characteristic function, and the sequence converges weakly to it. Continuity is required only at zero; normalization of the limit follows from the probability measures in the sequence.