Theorems · Theorem · measure theory

MeasureTheory.Measure.infinitePi_map_piCurry_symm

∀ {ι : Type u_3} {κ : ι → Type u_4} {X : (i : ι) → κ i → Type u_5} {mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)}
  (μ : (i : ι) → (j : κ i) → MeasureTheory.Measure (X i j))
  [hμ : ∀ (i : ι) (j : κ i), MeasureTheory.IsProbabilityMeasure (μ i j)],
  MeasureTheory.Measure.map (⇑(MeasurableEquiv.piCurry X).symm)
      (MeasureTheory.Measure.infinitePi fun i => MeasureTheory.Measure.infinitePi fun j => μ i j) =
    MeasureTheory.Measure.infinitePi fun p => μ p.fst p.snd

Defined in

Mathlib.Probability.ProductMeasure

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsProbabilityMeasure