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.

theorem MeasureTheory.TendstoInDistribution.of_tendsto_charFun {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Ω' : Type u_3} {Ω : ℕ → Type u_4} {m : (n : ℕ) → MeasurableSpace (Ω n)} {P : (n : ℕ) → Measure (Ω n)} [∀ (n : ℕ), IsProbabilityMeasure (P n)] {m' : MeasurableSpace Ω'} {P' : Measure Ω'} [IsProbabilityMeasure P'] {X : (n : ℕ) → Ω n → E} {X' : Ω' → E} (hX : ∀ (n : ℕ), AEMeasurable (X n) (P n)) (hX' : AEMeasurable X' P') (h : ∀ (t : E), Filter.Tendsto (fun (n : ℕ) => charFun (Measure.map (X n) (P n)) t) Filter.atTop (nhds (charFun (Measure.map X' P') t))) : TendstoInDistribution X Filter.atTop X' P P'

If the characteristic functions of a sequence of pushforward measures converge pointwise to the characteristic function of a pushforward measure, then the random variables converge in distribution.

theorem MeasureTheory.TendstoInDistribution.tendsto_charFun {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Ω' : Type u_3} {Ω : ℕ → Type u_4} {m : (n : ℕ) → MeasurableSpace (Ω n)} {P : (n : ℕ) → Measure (Ω n)} [∀ (n : ℕ), IsProbabilityMeasure (P n)] {m' : MeasurableSpace Ω'} {P' : Measure Ω'} [IsProbabilityMeasure P'] {X : (n : ℕ) → Ω n → E} {X' : Ω' → E} (h : TendstoInDistribution X Filter.atTop X' P P') (t : E) : Filter.Tendsto (fun (n : ℕ) => charFun (Measure.map (X n) (P n)) t) Filter.atTop (nhds (charFun (Measure.map X' P') t))

If a sequence of random variables converges in distribution to a random variable, then the characteristic functions of the sequence of pushforward measures under the sequence of random variables converge pointwise to the characteristic function of the pushforward measure under the random variable.

theorem MeasureTheory.tendstoInDistribution_iff_tendsto_charFun {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Ω' : Type u_3} {Ω : ℕ → Type u_4} {m : (n : ℕ) → MeasurableSpace (Ω n)} {P : (n : ℕ) → Measure (Ω n)} [∀ (n : ℕ), IsProbabilityMeasure (P n)] {m' : MeasurableSpace Ω'} {P' : Measure Ω'} [IsProbabilityMeasure P'] {X : (n : ℕ) → Ω n → E} {X' : Ω' → E} (hX : ∀ (n : ℕ), AEMeasurable (X n) (P n)) (hX' : AEMeasurable X' P') : TendstoInDistribution X Filter.atTop X' P P' ↔ ∀ (t : E), Filter.Tendsto (fun (n : ℕ) => charFun (Measure.map (X n) (P n)) t) Filter.atTop (nhds (charFun (Measure.map X' P') t))

The convergence in distribution of random variables is equivalent to the pointwise convergence of the characteristic functions of their pushforwards.