From 7ad9310345cd43d8ed77719da5a5476eb4daf0d6 Mon Sep 17 00:00:00 2001 From: Xavier Roblot Date: Thu, 27 Jun 2024 10:21:13 +0200 Subject: [PATCH 1/3] 1st commit --- Mathlib/MeasureTheory/Constructions/Pi.lean | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/Mathlib/MeasureTheory/Constructions/Pi.lean b/Mathlib/MeasureTheory/Constructions/Pi.lean index 8251ebd7f261e9..503f7f93386dbe 100644 --- a/Mathlib/MeasureTheory/Constructions/Pi.lean +++ b/Mathlib/MeasureTheory/Constructions/Pi.lean @@ -932,6 +932,23 @@ theorem volume_preserving_piFinsetUnion (α : ι → Type*) [DecidableEq ι] {s MeasurePreserving (MeasurableEquiv.piFinsetUnion α h) volume volume := measurePreserving_piFinsetUnion h (fun _ ↦ volume) +theorem measurePreserving_pi {β : ι → Type*} [∀ i, MeasurableSpace (β i)] + (ν : (i : ι) → Measure (β i)) [∀ i, SigmaFinite (ν 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 + convert ((MeasurableEquiv.piCongrRight f).symm.measurable.measurePreserving (Measure.pi ν)).symm + refine Measure.pi_eq fun s hs ↦ ?_ + rw [MeasurableEquiv.map_symm, Measure.comap_apply] + simp_rw [MeasurableEquiv.image_eq_preimage, MeasurableEquiv.piCongrRight, Equiv.piCongrRight, + MeasurableEquiv.coe_toEquiv, MeasurableEquiv.coe_toEquiv_symm, MeasurableEquiv.symm_mk, + MeasurableEquiv.coe_mk, Equiv.coe_fn_symm_mk, Set.preimage_pi, + ← MeasurableEquiv.image_eq_preimage, Measure.pi_pi, + ← MeasurePreserving.measure_preimage (hf _) + ((MeasurableEquiv.measurableSet_image (f _)).mpr (hs _)), MeasurableEquiv.preimage_image] + · exact (MeasurableEquiv.piCongrRight f).injective + · exact fun _ hs ↦ ((MeasurableEquiv.piCongrRight f).measurableSet_image ).mpr hs + · exact MeasurableSet.univ_pi hs + end MeasurePreserving end MeasureTheory From 766d25fb187416b59e3b38ffb56133928371c4b1 Mon Sep 17 00:00:00 2001 From: Xavier Roblot Date: Thu, 27 Jun 2024 13:57:28 +0200 Subject: [PATCH 2/3] New version --- Mathlib/MeasureTheory/Constructions/Pi.lean | 31 +++++++++++---------- 1 file changed, 17 insertions(+), 14 deletions(-) diff --git a/Mathlib/MeasureTheory/Constructions/Pi.lean b/Mathlib/MeasureTheory/Constructions/Pi.lean index 31cafb3595519a..d0e2ae680ccc6c 100644 --- a/Mathlib/MeasureTheory/Constructions/Pi.lean +++ b/Mathlib/MeasureTheory/Constructions/Pi.lean @@ -971,21 +971,24 @@ theorem volume_preserving_piFinsetUnion (α : ι → Type*) [DecidableEq ι] {s measurePreserving_piFinsetUnion h (fun _ ↦ volume) theorem measurePreserving_pi {β : ι → Type*} [∀ i, MeasurableSpace (β i)] - (ν : (i : ι) → Measure (β i)) [∀ i, SigmaFinite (ν i)] {f : (i : ι) → (α i) ≃ᵐ (β i)} + (ν : (i : ι) → Measure (β i)) [∀ i, SigmaFinite (ν 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 - convert ((MeasurableEquiv.piCongrRight f).symm.measurable.measurePreserving (Measure.pi ν)).symm - refine Measure.pi_eq fun s hs ↦ ?_ - rw [MeasurableEquiv.map_symm, Measure.comap_apply] - simp_rw [MeasurableEquiv.image_eq_preimage, MeasurableEquiv.piCongrRight, Equiv.piCongrRight, - MeasurableEquiv.coe_toEquiv, MeasurableEquiv.coe_toEquiv_symm, MeasurableEquiv.symm_mk, - MeasurableEquiv.coe_mk, Equiv.coe_fn_symm_mk, Set.preimage_pi, - ← MeasurableEquiv.image_eq_preimage, Measure.pi_pi, - ← MeasurePreserving.measure_preimage (hf _) - ((MeasurableEquiv.measurableSet_image (f _)).mpr (hs _)), MeasurableEquiv.preimage_image] - · exact (MeasurableEquiv.piCongrRight f).injective - · exact fun _ hs ↦ ((MeasurableEquiv.piCongrRight f).measurableSet_image ).mpr hs - · exact MeasurableSet.univ_pi hs + MeasurePreserving (fun a i ↦ f i (a i)) (Measure.pi μ) (Measure.pi ν) where + measurable := + measurable_pi_iff.mpr <| fun i ↦ (hf i).measurable.comp (measurable_pi_apply i) + map_eq := by + refine (Measure.pi_eq fun s hs ↦ ?_).symm + rw [Measure.map_apply, Set.preimage_pi, Measure.pi_pi] + simp_rw [← MeasurePreserving.measure_preimage (hf _) (hs _)] + · exact measurable_pi_iff.mpr <| fun i ↦ (hf i).measurable.comp (measurable_pi_apply i) + · exact MeasurableSet.univ_pi hs + +theorem volume_preserving_pi {α' β' : ι → Type*} [∀ i, MeasureSpace (α' i)] + [∀ i, MeasureSpace (β' i)] [∀ i, SigmaFinite (volume : Measure (α' i))] + [∀ i, SigmaFinite (volume : Measure (β' i))] {f : (i : ι) → (α' i) → (β' i)} + (hf : ∀ i, MeasurePreserving (f i)) : + MeasurePreserving (fun (a : (i : ι) → α' i) (i : ι) ↦ (f i) (a i)) := + measurePreserving_pi _ _ hf end MeasurePreserving From 98d4aa137e49dc5e14499f69faeb3de25905ea2f Mon Sep 17 00:00:00 2001 From: Xavier Roblot Date: Fri, 28 Jun 2024 14:35:32 +0200 Subject: [PATCH 3/3] Remove hyp --- Mathlib/MeasureTheory/Constructions/Pi.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/MeasureTheory/Constructions/Pi.lean b/Mathlib/MeasureTheory/Constructions/Pi.lean index d0e2ae680ccc6c..02da9602dc3791 100644 --- a/Mathlib/MeasureTheory/Constructions/Pi.lean +++ b/Mathlib/MeasureTheory/Constructions/Pi.lean @@ -971,12 +971,13 @@ theorem volume_preserving_piFinsetUnion (α : ι → Type*) [DecidableEq ι] {s measurePreserving_piFinsetUnion h (fun _ ↦ volume) theorem measurePreserving_pi {β : ι → Type*} [∀ i, MeasurableSpace (β i)] - (ν : (i : ι) → Measure (β i)) [∀ i, SigmaFinite (ν i)] {f : (i : ι) → (α i) → (β i)} + (ν : (i : ι) → Measure (β i)) {f : (i : ι) → (α i) → (β i)} [∀ i, SigmaFinite (ν i)] (hf : ∀ i, MeasurePreserving (f i) (μ i) (ν i)) : MeasurePreserving (fun a i ↦ f i (a i)) (Measure.pi μ) (Measure.pi ν) where measurable := measurable_pi_iff.mpr <| fun i ↦ (hf i).measurable.comp (measurable_pi_apply i) map_eq := by + haveI : ∀ i, SigmaFinite (μ i) := fun i ↦ (hf i).sigmaFinite refine (Measure.pi_eq fun s hs ↦ ?_).symm rw [Measure.map_apply, Set.preimage_pi, Measure.pi_pi] simp_rw [← MeasurePreserving.measure_preimage (hf _) (hs _)] @@ -984,9 +985,8 @@ theorem measurePreserving_pi {β : ι → Type*} [∀ i, MeasurableSpace (β i)] · exact MeasurableSet.univ_pi hs theorem volume_preserving_pi {α' β' : ι → Type*} [∀ i, MeasureSpace (α' i)] - [∀ i, MeasureSpace (β' i)] [∀ i, SigmaFinite (volume : Measure (α' i))] - [∀ i, SigmaFinite (volume : Measure (β' i))] {f : (i : ι) → (α' i) → (β' i)} - (hf : ∀ i, MeasurePreserving (f i)) : + [∀ i, MeasureSpace (β' i)] [∀ i, SigmaFinite (volume : Measure (β' i))] + {f : (i : ι) → (α' i) → (β' i)} (hf : ∀ i, MeasurePreserving (f i)) : MeasurePreserving (fun (a : (i : ι) → α' i) (i : ι) ↦ (f i) (a i)) := measurePreserving_pi _ _ hf