Theorems · Theorem · measure theory

MeasureTheory.Measure.map_piSingleton

∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} (μ : (n : ℕ) → MeasureTheory.Measure (X n))
  [∀ (n : ℕ), MeasureTheory.SigmaFinite (μ n)] (n : ℕ),
  MeasureTheory.Measure.map (⇑(MeasurableEquiv.piSingleton n)) (μ (n + 1)) = MeasureTheory.Measure.pi fun i => μ ↑i

Let μ (i + 1) : Measure (X (i + 1)) be a measure. Up to an equivalence, μ i = ⨂ j : Ioc i (i + 1), μ i, where ⊗ denotes the product of measures.

Defined in

Mathlib.Probability.ProductMeasure

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.SigmaFinite