Theorems · Theorem · measure theory

MeasureTheory.piContent_tendsto_zero

∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {A : ℕ → Set ((i : ι) → X i)},
  (∀ (n : ℕ), A n ∈ MeasureTheory.measurableCylinders X) →
    Antitone A → ⋂ n, A n = ∅ → Filter.Tendsto (fun n => (MeasureTheory.piContent μ) (A n)) Filter.atTop (nhds 0)

This is the key theorem to build the product of an arbitrary family of probability measures: the piContent of a decreasing sequence of cylinders with empty intersection converges to 0. This implies the σ-additivity of piContent (see addContent_iUnion_eq_sum_of_tendsto_zero), which allows to extend it to the σ-algebra by Carathéodory's theorem.

Defined in

Mathlib.Probability.ProductMeasure

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsProbabilityMeasure