Theorems · Theorem · measure theory

IsPiSystem.tendsto_probabilityMeasure_of_tendsto_of_mem

∀ {Ω : Type u_1} {ι : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [SecondCountableTopology Ω]
  [inst_3 : OpensMeasurableSpace Ω] {S : Set (Set Ω)},
  IsPiSystem S →
    ∀ {μ : ι → MeasureTheory.ProbabilityMeasure Ω} {ν : MeasureTheory.ProbabilityMeasure Ω} {l : Filter ι}
      [l.IsCountablyGenerated],
      (∀ s ∈ S, MeasurableSet s) →
        (∀ (u : Set Ω), IsOpen u → ∀ x ∈ u, ∃ s ∈ S, s ∈ nhds x ∧ s ⊆ u) →
          (∀ s ∈ S, Filter.Tendsto (fun i => (μ i) s) l (nhds (ν s))) → Filter.Tendsto μ l (nhds ν)

Assume that, applied to all the elements of a π-system, a sequence of probability measures converges to a limiting probability measure. Assume also that the π-system contains arbitrarily small neighborhoods of any point. Then the sequence of probability measures converges for the weak topology.

Defined in

Mathlib.MeasureTheory.Measure.Portmanteau

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceSecondCountableTopologyOpensMeasurableSpaceFilter.IsCountablyGenerated