Theorems · Theorem · measure theory

MeasureTheory.Measure.infinitePi_map_pi

∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {Y : ι → Type u_3} [inst : (i : ι) → MeasurableSpace (Y i)]
  {f : (i : ι) → X i → Y i},
  (∀ (i : ι), Measurable (f i)) →
    MeasureTheory.Measure.map (fun x i => f i (x i)) (MeasureTheory.Measure.infinitePi μ) =
      MeasureTheory.Measure.infinitePi fun i => MeasureTheory.Measure.map (f i) (μ i)

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.IsProbabilityMeasureMeasurableSpace