Theorems · Theorem · measure theory

MeasureTheory.Measure.pi_prod_map_IocProdIoc

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

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

Defined in

Mathlib.Probability.ProductMeasure

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsProbabilityMeasure