Theorems · Theorem · measure theory

MeasureTheory.Measure.pi_prod_map_IicProdIoc

∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} (μ : (n : ℕ) → MeasureTheory.Measure (X n))
  [hμ : ∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)] {a b : ℕ},
  MeasureTheory.Measure.map (IicProdIoc a b)
      ((MeasureTheory.Measure.pi fun i => μ ↑i).prod (MeasureTheory.Measure.pi fun i => μ ↑i)) =
    MeasureTheory.Measure.pi fun i => μ ↑i

Let μ : (i : Iic b) → Measure (X i) be a family of measures. Up to an equivalence, (⨂ i : Iic a, μ i) ⊗ (⨂ i : Ioc a b, μ i) = ⨂ i : Iic b, μ i, where ⊗ denotes the product of measures.

Defined in

Mathlib.Probability.ProductMeasure

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsProbabilityMeasure