Theorems · Theorem · measure theory

MeasureTheory.Measure.pi_map_pi

∀ {ι : Type u_1} [inst : Fintype ι] {X : ι → Type u_4} {Y : ι → Type u_5} {mX : (i : ι) → MeasurableSpace (X i)}
  {μ : (i : ι) → MeasureTheory.Measure (X i)} [inst_1 : (i : ι) → MeasurableSpace (Y i)] {f : (i : ι) → X i → Y i}
  [hμ : ∀ (i : ι), MeasureTheory.SigmaFinite (MeasureTheory.Measure.map (f i) (μ i))],
  (∀ (i : ι), AEMeasurable (f i) (μ i)) →
    MeasureTheory.Measure.map (fun x i => f i (x i)) (MeasureTheory.Measure.pi μ) =
      MeasureTheory.Measure.pi fun i => MeasureTheory.Measure.map (f i) (μ i)

Defined in

Mathlib.MeasureTheory.Constructions.Pi

Cited by

3 results in Mathlib

Foundations

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

Assumes

FintypeMeasurableSpaceMeasureTheory.SigmaFinite