Theorems · Theorem · measure theory

IsPiSystem.tendsto_measureReal_biUnion

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

Given a π-system, if a sequence of 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 259 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpace