Lévy's convergence theorem

This file contains developments related to Lévy's convergence theorem, which links convergence of characteristic functions and convergence in distribution in finite dimensional inner product spaces.

Main statements

• isTightMeasureSet_of_tendsto_charFun: if the characteristic functions of a sequence of measures μ : ℕ → Measure E on a finite dimensional inner product space converge pointwise to a function which is continuous at 0, then {μ n | n} is tight.
• ProbabilityMeasure.tendsto_iff_tendsto_charFun: the weak convergence of probability measures is equivalent to the pointwise convergence of their characteristic functions.

theorem MeasureTheory.isTightMeasureSet_of_tendsto_charFun {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : ℕ → Measure E} [∀ (i : ℕ), IsProbabilityMeasure (μ i)] {f : E → ℂ} (hf : ContinuousAt f 0) (h : ∀ (t : E), Filter.Tendsto (fun (n : ℕ) => charFun (μ n) t) Filter.atTop (nhds (f t))) : IsTightMeasureSet (Set.range μ)

If the characteristic functions of a sequence of measures μ : ℕ → Measure E converge pointwise to a function which is continuous at 0, then {μ n | n} is tight.

theorem MeasureTheory.ProbabilityMeasure.tendsto_of_tight_of_separatesPoints (𝕜 : Type u_2) [RCLike 𝕜] {E : Type u_3} [MeasurableSpace E] [TopologicalSpace E] [PolishSpace E] [BorelSpace E] {ι : Type u_4} {𝓕 : Filter ι} {μ : ι → ProbabilityMeasure E} (h_tight : IsTightMeasureSet {x : Measure E | ∃ (n : ι), ↑(μ n) = x}) {μ₀ : ProbabilityMeasure E} {A : StarSubalgebra 𝕜 (BoundedContinuousFunction E 𝕜)} (hA : (StarSubalgebra.map (BoundedContinuousFunction.toContinuousMapStarₐ 𝕜) A).SeparatesPoints) (hμ : ∀ g ∈ A, Filter.Tendsto (fun (n : ι) => ∫ (x : E), g x ∂↑(μ n)) 𝓕 (nhds (∫ (x : E), g x ∂↑μ₀))) : Filter.Tendsto μ 𝓕 (nhds μ₀)

Let μ be a tight sequence of probability measures and μ₀ a probability measure. If A is a star sub-algebra of bounded continuous scalar functions that separates points and the integrals of elements of A with respect to μ converge to the integrals with respect to μ₀, then μ converges weakly to μ₀.

theorem MeasureTheory.ProbabilityMeasure.tendsto_charPoly_of_tendsto_charFun {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {ι : Type u_2} {𝓕 : Filter ι} {μ₀ : ProbabilityMeasure E} {μ : ι → ProbabilityMeasure E} (h : ∀ (t : E), Filter.Tendsto (fun (n : ι) => charFun (↑(μ n)) t) 𝓕 (nhds (charFun (↑μ₀) t))) {g : BoundedContinuousFunction E ℂ} (hg : g ∈ BoundedContinuousFunction.charPoly Real.continuous_probChar ⋯) : Filter.Tendsto (fun (n : ι) => ∫ (x : E), g x ∂↑(μ n)) 𝓕 (nhds (∫ (x : E), g x ∂↑μ₀))

theorem MeasureTheory.ProbabilityMeasure.tendsto_of_tendsto_charFun {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ₀ : ProbabilityMeasure E} {μ : ℕ → ProbabilityMeasure E} (h : ∀ (t : E), Filter.Tendsto (fun (n : ℕ) => charFun (↑(μ n)) t) Filter.atTop (nhds (charFun (↑μ₀) t))) : Filter.Tendsto μ Filter.atTop (nhds μ₀)

If the characteristic functions of a sequence of probability measures converge pointwise to the characteristic function of a probability measure, then the measures converge weakly.

theorem MeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_charFun {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ₀ : ProbabilityMeasure E} {μ : ℕ → ProbabilityMeasure E} : Filter.Tendsto μ Filter.atTop (nhds μ₀) ↔ ∀ (t : E), Filter.Tendsto (fun (n : ℕ) => charFun (↑(μ n)) t) Filter.atTop (nhds (charFun (↑μ₀) t))

The Lévy convergence theorem: the weak convergence of probability measures is equivalent to the pointwise convergence of their characteristic functions.