MeasureTheory.measurePreserving_pi

Stream: Is there code for X?

[Xavier Roblot]

We have docs#MeasureTheory.MeasurePreserving.prod but not docs#MeasureTheory.measurePreserving_pi, it seems. Is this statement true?

import Mathlib.MeasureTheory.Constructions.Pi

theorem MeasureTheory.measurePreserving_pi {ι : Type*} [Fintype ι] {α : ι → Type*} {β : ι → Type*}
    [∀ i, MeasurableSpace (α i)] [∀ i, MeasurableSpace (β i)] (μ : (i : ι) → Measure (α i))
    (ν : (i : ι) → Measure (β i)) [∀ i, SFinite (μ i)] [∀ i, SFinite (ν i)]
    {f : (i : ι) → (α i) → (β i)} (hf : ∀ i, MeasurePreserving (f i) (μ i) (ν i)) :
    MeasurePreserving (fun a i ↦ f i (a i)) (Measure.pi μ) (Measure.pi ν)  := by
  sorry

and if so what would be the best way to prove it?

[Yury G. Kudryashov]

Did you try to use docs#MeasureTheory.Measure.pi_eq ?

[Yury G. Kudryashov]

UPD: I see that you want SFinite, not SigmaFinite. I don't know about details here.

[Yury G. Kudryashov]

As of now, SFinite is mentioned 0 times in the file about pi measures.

[Floris van Doorn]

You need SigmaFinite to work with iterated products. The reason is that we need docs#MeasureTheory.Measure.prod_eq, which has a comment above it that it's false for SFinite measures. I once looked at whether we can can generalize parts of the theory of Measure.pi to SFinite measures, but I don't think it's possible (at least with the current definition).

[Xavier Roblot]

Floris van Doorn said:

You need SigmaFinite to work with iterated products. The reason is that we need docs#MeasureTheory.Measure.prod_eq, which has a comment above it that it's false for SFinite measures. I once looked at whether we can can generalize parts of the theory of Measure.pi to SFinite measures, but I don't think it's possible (at least with the current definition).

Right. I am happy with SigmaFinite. I put SFinite because it was what was used for docs#MeasureTheory.MeasurePreserving.prod. Anyway, I'll have a look at docs#MeasureTheory.Measure.pi_eq. Thanks to you both!

[Xavier Roblot]

#14185