feat(MeasureTheory/Constructions/Pi): add measurePreserving_pi (#14185

)

See the Zulip [thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/MeasureTheory.2EmeasurePreserving_pi/near/447399178)

Mathlib/MeasureTheory/Constructions/Pi.lean

@@ -970,6 +970,26 @@ 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)) {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 _)]
+    · 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))]
+    {f : (i : ι) → (α' i) → (β' i)} (hf : ∀ i, MeasurePreserving (f i)) :
+    MeasurePreserving (fun (a : (i : ι) → α' i) (i : ι) ↦ (f i) (a i)) :=
+  measurePreserving_pi _ _ hf
+
 end MeasurePreserving
 
 end MeasureTheory