Theorems · Theorem · measure theory

MeasureTheory.Measure.isProjectiveLimit_infinitePi

∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)],
  MeasureTheory.IsProjectiveLimit (MeasureTheory.Measure.infinitePi μ) fun I => MeasureTheory.Measure.pi fun i => μ ↑i

The product measure is the projective limit of the partial product measures. This ensures uniqueness and expresses the value of the product measure applied to cylinders.

Defined in

Mathlib.Probability.ProductMeasure

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsProbabilityMeasure