Theorems · Theorem · measure theory

IsPiSystem.tendsto_probabilityMeasure_biUnion

∀ {Ω : Type u_1} {ι : Type u_2} [inst : MeasurableSpace Ω] {S : Set (Set Ω)},
  IsPiSystem S →
    ∀ {μ : ι → MeasureTheory.ProbabilityMeasure Ω} {ν : MeasureTheory.ProbabilityMeasure Ω} {l : Filter ι}
      {t : Finset (Set Ω)},
      (∀ s ∈ t, s ∈ S) →
        (∀ s ∈ S, MeasurableSet s) →
          (∀ s ∈ S, Filter.Tendsto (fun i => (μ i) s) l (nhds (ν s))) →
            Filter.Tendsto (fun i => (μ i) (⋃ s ∈ t, s)) l (nhds (ν (⋃ s ∈ t, s)))

Given a π-system, if a sequence of probability measures converges along all elements of the π-system, then it also converges along finite unions of elements of the π-system.

Defined in

Mathlib.MeasureTheory.Measure.Portmanteau

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpace