Theorems · Theorem · probability

MeasureTheory.ProbabilityMeasure.tendsto_of_tight_of_separatesPoints

∀ (𝕜 : Type u_2) [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : MeasurableSpace E] [inst_2 : TopologicalSpace E]
  [PolishSpace E] [inst_4 : BorelSpace E] {ι : Type u_4} {𝓕 : Filter ι} {μ : ι → MeasureTheory.ProbabilityMeasure E},
  MeasureTheory.IsTightMeasureSet {x | ∃ n, ↑(μ n) = x} →
    ∀ {μ₀ : MeasureTheory.ProbabilityMeasure E} {A : StarSubalgebra 𝕜 (BoundedContinuousFunction E 𝕜)},
      (StarSubalgebra.map (BoundedContinuousFunction.toContinuousMapStarₐ 𝕜) A).SeparatesPoints →
        (∀ 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 μ₀.

Defined in

Mathlib.MeasureTheory.Measure.LevyConvergence

Cited by

1 results in Mathlib

Foundations

Depth 284 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeMeasurableSpaceTopologicalSpacePolishSpaceBorelSpace