feat(Probability/Independence/InfinitePi): rearrangement of infinite product measures (leanprover-community#39503)

This PR introduces a lemma for coordinate transformations of `infinitePi` measures.

- `MeasureTheory.Measure.map_infinitePi_infinitePi_of_inj`: if `f : α → ι` is injective, then the pushforward of the coordinates rearranged according to `f` (i.e., the law of `fun ω i ↦ ω (f i)` is the same as the infinite product of the rearranged laws.

This lemma bears some resemblance to `infinitePi_map_piCongrLeft`, but does not require `f` to be a bijection and probably is easier to work with in practice.

Author: jvanwinden

Mathlib/Probability/Independence/InfinitePi.lean

@@ -108,6 +108,14 @@ lemma iIndepFun_infinitePi {Ω : ι → Type*} {mΩ : ∀ i, MeasurableSpace (Ω
   congrm infinitePi fun i ↦ ?_
   rw [← infinitePi_map_eval P i, map_map (mX i) (by fun_prop), Function.comp_def]
 
+lemma _root_.MeasureTheory.Measure.map_infinitePi_infinitePi_of_inj {α : Type*} {Ω : ι → Type*}
+    {mΩ : ∀ i, MeasurableSpace (Ω i)} {P : ∀ i, Measure (Ω i)}
+    [∀ i, IsProbabilityMeasure (P i)] {f : α → ι} (hf : Function.Injective f) :
+    (infinitePi P).map (fun ω i ↦ ω (f i)) = infinitePi (fun i ↦ P (f i)) := by
+  rw [(iIndepFun_iff_map_fun_eq_infinitePi_map <| by fun_prop).mp ?_]
+  · simp [infinitePi_map_eval]
+  exact .precomp hf <| iIndepFun_infinitePi (X := fun x ω ↦ ω) <| by fun_prop
+
 section curry
 
 omit [IsProbabilityMeasure P]