feat: add an alias for the forward direction of indepFun_iff_map_prod_eq_prod_map_map (leanprover-community#39767)

When assuming `hXY : IndepFun X Y P`, if one wants to rewrite `P.map (fun w => (X w, Y w)) = (P.map X).prod (P.map Y)`, one has to use [ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Probability/Independence/Basic.html#ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map), which is an iff with side-condition so is not convenient. We thus introduce an alias for this direction.

We do the same for the `iIndepFun` version, removing the unnecessary `IsProbabilityMeasure` hypothesis there. We do the same in the `infinitePi` case too.

Author: EtienneC30

Mathlib/Probability/HasLaw.lean

@@ -188,7 +188,7 @@ lemma indepFun_iff_hasLaw_prodMk_prod [IsFiniteMeasure P] {𝓨 : Type*} {m𝓨
     X ⟂ᵢ[P] Y ↔ HasLaw (fun ω ↦ (X ω, Y ω)) (μ.prod ν) P where
   mp h :=
     { map_eq := by
-        rw [(indepFun_iff_map_prod_eq_prod_map_map (by fun_prop) (by fun_prop)).1 h, hX.map_eq,
+        rw [h.map_prod_eq_prod_map_map (by fun_prop) (by fun_prop), hX.map_eq,
           hY.map_eq] }
   mpr h := by
     rw [indepFun_iff_map_prod_eq_prod_map_map (by fun_prop) (by fun_prop),
@@ -201,8 +201,7 @@ lemma iIndepFun.hasLaw_pi {ι : Type*} [Fintype ι] {𝓧 : ι → Type*} {m𝓧
     (h : iIndepFun X P) :
     HasLaw (fun ω i ↦ X i ω) (Measure.pi μ) P where
   map_eq := by
-    have := h.isProbabilityMeasure
-    rw [(iIndepFun_iff_map_fun_eq_pi_map (by fun_prop)).1 h]
+    rw [h.map_fun_eq_pi_map (by fun_prop)]
     simp_rw [fun i ↦ (hX i).map_eq]
 
 lemma iIndepFun_iff_hasLaw_pi_pi [IsProbabilityMeasure P] {ι : Type*} [Fintype ι] {𝓧 : ι → Type*}

Mathlib/Probability/IdentDistrib.lean

@@ -348,8 +348,7 @@ lemma indepFun_of_identDistrib_pair
     {X : γ → α} {X' : δ → α} {Y : γ → β} {Y' : δ → β} (h_indep : X ⟂ᵢ[μ] Y)
     (h_ident : IdentDistrib (fun ω ↦ (X ω, Y ω)) (fun ω ↦ (X' ω, Y' ω)) μ μ') :
     X' ⟂ᵢ[μ'] Y' := by
-  rw [indepFun_iff_map_prod_eq_prod_map_map _ _, ← h_ident.map_eq,
-    (indepFun_iff_map_prod_eq_prod_map_map _ _).1 h_indep]
+  rw [indepFun_iff_map_prod_eq_prod_map_map, ← h_ident.map_eq, h_indep.map_prod_eq_prod_map_map]
   · exact congr (congrArg Measure.prod <| (h_ident.comp measurable_fst).map_eq)
       (h_ident.comp measurable_snd).map_eq
   · exact measurable_fst.aemeasurable.comp_aemeasurable h_ident.aemeasurable_fst

Mathlib/Probability/IdentDistribIndep.lean

@@ -47,8 +47,8 @@ lemma IdentDistrib.prodMk [IsFiniteMeasure μ]
     have : IsFiniteMeasure ν := by
       have : IsFiniteMeasure (ν.map Z) := by rw [← hXZ.map_eq]; infer_instance
       exact Measure.isFiniteMeasure_of_map hXZ.aemeasurable_snd
-    rw [(indepFun_iff_map_prod_eq_prod_map_map hXZ.aemeasurable_fst hYW.aemeasurable_fst).mp hXY,
-      (indepFun_iff_map_prod_eq_prod_map_map hXZ.aemeasurable_snd hYW.aemeasurable_snd).mp hZW,
+    rw [hXY.map_prod_eq_prod_map_map hXZ.aemeasurable_fst hYW.aemeasurable_fst,
+      hZW.map_prod_eq_prod_map_map hXZ.aemeasurable_snd hYW.aemeasurable_snd,
       hXZ.map_eq, hYW.map_eq]
 
 /-- If `(X i)` and `(Y i)` are families of independent random variables indexed by a countable

Mathlib/Probability/Independence/Basic.lean

@@ -705,33 +705,7 @@ theorem indepFun_iff_map_prod_eq_prod_map_map {mβ : MeasurableSpace β} {mβ' :
     f ⟂ᵢ[μ] g ↔ μ.map (fun ω ↦ (f ω, g ω)) = (μ.map f).prod (μ.map g) := by
   apply indepFun_iff_map_prod_eq_prod_map_map' hf hg <;> apply IsFiniteMeasure.toSigmaFinite
 
-theorem iIndepFun_iff_map_fun_eq_pi_map [Fintype ι] {β : ι → Type*}
-    {m : ∀ i, MeasurableSpace (β i)} {f : Π i, Ω → β i} [IsProbabilityMeasure μ]
-    (hf : ∀ i, AEMeasurable (f i) μ) :
-    iIndepFun f μ ↔ μ.map (fun ω i ↦ f i ω) = Measure.pi (fun i ↦ μ.map (f i)) := by
-  classical
-  rw [iIndepFun_iff_measure_inter_preimage_eq_mul]
-  have h₀ {s : ∀ i, Set (β i)} (hm : ∀ (i : ι), MeasurableSet (s i)) :
-      ∏ i : ι, μ (f i ⁻¹' s i) = ∏ i : ι, μ.map (f i) (s i) ∧
-      μ (⋂ i : ι, (f i ⁻¹' s i)) = μ.map (fun ω i ↦ f i ω) (univ.pi s) := by
-    constructor
-    · congr with x
-      rw [Measure.map_apply_of_aemeasurable (hf x) (hm x)]
-    · rw [Measure.map_apply_of_aemeasurable (aemeasurable_pi_lambda _ fun x ↦ hf x)
-        (.univ_pi hm)]
-      congr with x
-      simp
-  constructor
-  · refine fun hS ↦ (Measure.pi_eq fun h hm ↦ ?_).symm
-    rw [← (h₀ hm).1, ← (h₀ hm).2]
-    simpa [hm] using hS Finset.univ (sets := h)
-  · intro h S s hs
-    specialize h₀ (s := fun i ↦ if i ∈ S then s i else univ)
-      fun i ↦ by beta_reduce; split_ifs with hiS <;> simp [hiS, hs]
-    simp only [apply_ite, preimage_univ, measure_univ, Finset.prod_ite_mem, Finset.univ_inter,
-      Finset.prod_ite, Finset.filter_univ_mem, iInter_ite, iInter_univ, inter_univ, h,
-      Measure.pi_pi] at h₀
-    rw [h₀.2, ← h₀.1]
+alias ⟨IndepFun.map_prod_eq_prod_map_map, _⟩ := indepFun_iff_map_prod_eq_prod_map_map
 
 @[symm]
 nonrec theorem IndepFun.symm {_ : MeasurableSpace β} {_ : MeasurableSpace β'}
@@ -777,25 +751,6 @@ lemma indepFun_prod₀ (mX : AEMeasurable X μ) (mY : AEMeasurable Y ν) :
     · rw [measurePreserving_snd.map_eq]
       exact (AEMeasurable.ae_eq_mk mY).symm
 
-variable {ι : Type*} [Fintype ι] {Ω : ι → Type*} {mΩ : ∀ i, MeasurableSpace (Ω i)}
-    {μ : (i : ι) → Measure (Ω i)} [∀ i, IsProbabilityMeasure (μ i)]
-    {𝓧 : ι → Type*} [∀ i, MeasurableSpace (𝓧 i)] {X : (i : ι) → Ω i → 𝓧 i}
-
-/-- Given random variables `X i : Ω i → 𝓧 i`, they are independent when viewed as random
-variables defined on the product space `Π i, Ω i`. -/
-lemma iIndepFun_pi (mX : ∀ i, AEMeasurable (X i) (μ i)) :
-    iIndepFun (fun i ω ↦ X i (ω i)) (Measure.pi μ) := by
-  refine iIndepFun_iff_map_fun_eq_pi_map ?_ |>.2 ?_
-  · exact fun i ↦ (mX i).comp_quasiMeasurePreserving (Measure.quasiMeasurePreserving_eval _ i)
-  rw [Measure.pi_map_pi mX]
-  congr
-  ext i : 1
-  rw [← (measurePreserving_eval μ i).map_eq, AEMeasurable.map_map_of_aemeasurable,
-    Function.comp_def]
-  · rw [(measurePreserving_eval μ i).map_eq]
-    exact mX i
-  · exact (measurable_pi_apply i).aemeasurable
-
 end Prod
 
 theorem IndepFun.comp {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'}
@@ -882,6 +837,71 @@ lemma iIndepFun_iff_finset : iIndepFun f μ ↔ ∀ s : Finset ι, iIndepFun (s.
 
 alias ⟨iIndepFun.restrict, _⟩ := iIndepFun_iff_finset
 
+theorem iIndepFun.map_fun_eq_pi_map [Fintype ι] {β : ι → Type*}
+    {m : ∀ i, MeasurableSpace (β i)} {f : Π i, Ω → β i}
+    (hf : ∀ i, AEMeasurable (f i) μ) (h : iIndepFun f μ) :
+    μ.map (fun ω i ↦ f i ω) = Measure.pi (fun i ↦ μ.map (f i)) := by
+  classical
+  have := h.isProbabilityMeasure
+  rw [iIndepFun_iff_measure_inter_preimage_eq_mul] at h
+  have h₀ {s : ∀ i, Set (β i)} (hm : ∀ (i : ι), MeasurableSet (s i)) :
+      ∏ i : ι, μ (f i ⁻¹' s i) = ∏ i : ι, μ.map (f i) (s i) ∧
+      μ (⋂ i : ι, (f i ⁻¹' s i)) = μ.map (fun ω i ↦ f i ω) (univ.pi s) := by
+    constructor
+    · congr with x
+      rw [Measure.map_apply_of_aemeasurable (hf x) (hm x)]
+    · rw [Measure.map_apply_of_aemeasurable (aemeasurable_pi_lambda _ fun x ↦ hf x)
+        (.univ_pi hm)]
+      congr with x
+      simp
+  refine (Measure.pi_eq fun h' hm ↦ ?_).symm
+  rw [← (h₀ hm).1, ← (h₀ hm).2]
+  simpa [hm] using h Finset.univ (sets := h')
+
+theorem iIndepFun_iff_map_fun_eq_pi_map [Fintype ι] {β : ι → Type*}
+    {m : ∀ i, MeasurableSpace (β i)} {f : Π i, Ω → β i} [IsProbabilityMeasure μ]
+    (hf : ∀ i, AEMeasurable (f i) μ) :
+    iIndepFun f μ ↔ μ.map (fun ω i ↦ f i ω) = Measure.pi (fun i ↦ μ.map (f i)) := by
+  refine ⟨iIndepFun.map_fun_eq_pi_map hf, ?_⟩
+  classical
+  rw [iIndepFun_iff_measure_inter_preimage_eq_mul]
+  have h₀ {s : ∀ i, Set (β i)} (hm : ∀ (i : ι), MeasurableSet (s i)) :
+      ∏ i : ι, μ (f i ⁻¹' s i) = ∏ i : ι, μ.map (f i) (s i) ∧
+      μ (⋂ i : ι, (f i ⁻¹' s i)) = μ.map (fun ω i ↦ f i ω) (univ.pi s) := by
+    constructor
+    · congr with x
+      rw [Measure.map_apply_of_aemeasurable (hf x) (hm x)]
+    · rw [Measure.map_apply_of_aemeasurable (aemeasurable_pi_lambda _ fun x ↦ hf x)
+        (.univ_pi hm)]
+      congr with x
+      simp
+  intro h S s hs
+  specialize h₀ (s := fun i ↦ if i ∈ S then s i else univ)
+    fun i ↦ by beta_reduce; split_ifs with hiS <;> simp [hiS, hs]
+  simp only [apply_ite, preimage_univ, measure_univ, Finset.prod_ite_mem, Finset.univ_inter,
+    Finset.prod_ite, Finset.filter_univ_mem, iInter_ite, iInter_univ, inter_univ, h,
+    Measure.pi_pi] at h₀
+  rw [h₀.2, ← h₀.1]
+
+variable {ι : Type*} [Fintype ι] {Ω : ι → Type*} {mΩ : ∀ i, MeasurableSpace (Ω i)}
+    {μ : (i : ι) → Measure (Ω i)} [∀ i, IsProbabilityMeasure (μ i)]
+    {𝓧 : ι → Type*} [∀ i, MeasurableSpace (𝓧 i)] {X : (i : ι) → Ω i → 𝓧 i}
+
+/-- Given random variables `X i : Ω i → 𝓧 i`, they are independent when viewed as random
+variables defined on the product space `Π i, Ω i`. -/
+lemma iIndepFun_pi (mX : ∀ i, AEMeasurable (X i) (μ i)) :
+    iIndepFun (fun i ω ↦ X i (ω i)) (Measure.pi μ) := by
+  refine iIndepFun_iff_map_fun_eq_pi_map ?_ |>.2 ?_
+  · exact fun i ↦ (mX i).comp_quasiMeasurePreserving (Measure.quasiMeasurePreserving_eval _ i)
+  rw [Measure.pi_map_pi mX]
+  congr
+  ext i : 1
+  rw [← (measurePreserving_eval μ i).map_eq, AEMeasurable.map_map_of_aemeasurable,
+    Function.comp_def]
+  · rw [(measurePreserving_eval μ i).map_eq]
+    exact mX i
+  · exact (measurable_pi_apply i).aemeasurable
+
 end iIndepFun
 
 section Mul

Mathlib/Probability/Independence/InfinitePi.lean

@@ -33,29 +33,39 @@ open MeasureTheory Measure ProbabilityTheory
 
 namespace ProbabilityTheory
 
-variable {ι Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω} [IsProbabilityMeasure P]
+variable {ι Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω}
     {𝓧 : ι → Type*} {m𝓧 : ∀ i, MeasurableSpace (𝓧 i)} {X : Π i, Ω → 𝓧 i}
 
+/-- If random variables are independent then their joint distribution is the product measure. This
+is a version where the random variable `ω ↦ (Xᵢ(ω))ᵢ` is almost everywhere measurable.
+See `iIndepFun.map_fun_eq_infinitePi_map₀'` for a version which only assumes that
+each `Xᵢ` is almost everywhere measurable and that `ι` is countable. -/
+lemma iIndepFun.map_fun_eq_infinitePi_map₀ (mX : AEMeasurable (fun ω i ↦ X i ω) P)
+    (h : iIndepFun X P) :
+    P.map (fun ω i ↦ X i ω) = infinitePi (fun i ↦ P.map (X i)) := by
+  have := h.isProbabilityMeasure
+  have _ i := isProbabilityMeasure_map (mX.eval i)
+  refine eq_infinitePi _ fun s t ht ↦ ?_
+  rw [iIndepFun_iff_finset] at h
+  have : (s : Set ι).pi t = s.restrict ⁻¹' (Set.univ.pi fun i ↦ t i) := by ext; simp
+  rw [this, ← map_apply, AEMeasurable.map_map_of_aemeasurable]
+  · have : s.restrict ∘ (fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω := by ext; simp
+    rw [this, (h s).map_fun_eq_pi_map, pi_pi]
+    · simp only [Finset.restrict]
+      rw [s.prod_coe_sort fun i ↦ P.map (X i) (t i)]
+    exact fun i ↦ mX.eval i
+  any_goals fun_prop
+  · exact mX
+  · exact .univ_pi fun i ↦ ht i
+
 /-- Random variables are independent iff their joint distribution is the product measure. This
 is a version where the random variable `ω ↦ (Xᵢ(ω))ᵢ` is almost everywhere measurable.
 See `iIndepFun_iff_map_fun_eq_infinitePi_map₀'` for a version which only assumes that
 each `Xᵢ` is almost everywhere measurable and that `ι` is countable. -/
-lemma iIndepFun_iff_map_fun_eq_infinitePi_map₀ (mX : AEMeasurable (fun ω i ↦ X i ω) P) :
+lemma iIndepFun_iff_map_fun_eq_infinitePi_map₀ [IsProbabilityMeasure P]
+    (mX : AEMeasurable (fun ω i ↦ X i ω) P) :
     iIndepFun X P ↔ P.map (fun ω i ↦ X i ω) = infinitePi (fun i ↦ P.map (X i)) where
-  mp h := by
-    have _ i := isProbabilityMeasure_map (mX.eval i)
-    refine eq_infinitePi _ fun s t ht ↦ ?_
-    rw [iIndepFun_iff_finset] at h
-    have : (s : Set ι).pi t = s.restrict ⁻¹' (Set.univ.pi fun i ↦ t i) := by ext; simp
-    rw [this, ← map_apply, AEMeasurable.map_map_of_aemeasurable]
-    · have : s.restrict ∘ (fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω := by ext; simp
-      rw [this, (iIndepFun_iff_map_fun_eq_pi_map ?_).1 (h s), pi_pi]
-      · simp only [Finset.restrict]
-        rw [s.prod_coe_sort fun i ↦ P.map (X i) (t i)]
-      exact fun i ↦ mX.eval i
-    any_goals fun_prop
-    · exact mX
-    · exact .univ_pi fun i ↦ ht i
+  mp h := h.map_fun_eq_infinitePi_map₀ mX
   mpr h := by
     have _ i := isProbabilityMeasure_map (mX.eval i)
     rw [iIndepFun_iff_finset]
@@ -68,19 +78,33 @@ lemma iIndepFun_iff_map_fun_eq_infinitePi_map₀ (mX : AEMeasurable (fun ω i 
       exact mX
     exact fun i ↦ mX.eval i
 
+/-- If random variables are independent then their joint distribution is the product measure. This
+is an `AEMeasurable` version of `iIndepFun.map_fun_eq_infinitePi_map`, which is why it requires
+`ι` to be countable. -/
+lemma iIndepFun.map_fun_eq_infinitePi_map₀' [Countable ι] (mX : ∀ i, AEMeasurable (X i) P)
+    (h : iIndepFun X P) :
+    P.map (fun ω i ↦ X i ω) = infinitePi (fun i ↦ P.map (X i)) :=
+  h.map_fun_eq_infinitePi_map₀ <| aemeasurable_pi_iff.2 mX
+
 /-- Random variables are independent iff their joint distribution is the product measure. This is
 an `AEMeasurable` version of `iIndepFun_iff_map_fun_eq_infinitePi_map`, which is why it requires
 `ι` to be countable. -/
-lemma iIndepFun_iff_map_fun_eq_infinitePi_map₀' [Countable ι] (mX : ∀ i, AEMeasurable (X i) P) :
+lemma iIndepFun_iff_map_fun_eq_infinitePi_map₀' [IsProbabilityMeasure P] [Countable ι]
+    (mX : ∀ i, AEMeasurable (X i) P) :
     iIndepFun X P ↔ P.map (fun ω i ↦ X i ω) = infinitePi (fun i ↦ P.map (X i)) :=
   iIndepFun_iff_map_fun_eq_infinitePi_map₀ <| aemeasurable_pi_iff.2 mX
 
+/-- If random variables are independent then their joint distribution is the product measure. -/
+lemma iIndepFun.map_fun_eq_infinitePi_map (mX : ∀ i, Measurable (X i)) (h : iIndepFun X P) :
+    P.map (fun ω i ↦ X i ω) = infinitePi (fun i ↦ P.map (X i)) :=
+  h.map_fun_eq_infinitePi_map₀ <| measurable_pi_iff.2 mX |>.aemeasurable
+
 /-- Random variables are independent iff their joint distribution is the product measure. -/
-lemma iIndepFun_iff_map_fun_eq_infinitePi_map (mX : ∀ i, Measurable (X i)) :
+lemma iIndepFun_iff_map_fun_eq_infinitePi_map [IsProbabilityMeasure P]
+    (mX : ∀ i, Measurable (X i)) :
     iIndepFun X P ↔ P.map (fun ω i ↦ X i ω) = infinitePi (fun i ↦ P.map (X i)) :=
   iIndepFun_iff_map_fun_eq_infinitePi_map₀ <| measurable_pi_iff.2 mX |>.aemeasurable
 
-omit [IsProbabilityMeasure P] in
 lemma iIndepFun.hasLaw_infinitePi {μ : (i : ι) → Measure (𝓧 i)} (hX : ∀ i, HasLaw (X i) (μ i) P)
     (h1 : iIndepFun X P) (h2 : AEMeasurable (fun ω i ↦ X i ω) P) :
     HasLaw (fun ω i ↦ X i ω) (infinitePi μ) P where
@@ -90,7 +114,7 @@ lemma iIndepFun.hasLaw_infinitePi {μ : (i : ι) → Measure (𝓧 i)} (hX : ∀
     rw [(iIndepFun_iff_map_fun_eq_infinitePi_map₀ h2).1 h1]
     simp_rw [fun i ↦ (hX i).map_eq]
 
-lemma iIndepFun_iff_hasLaw_Pi_infinitePi {μ : (i : ι) → Measure (𝓧 i)}
+lemma iIndepFun_iff_hasLaw_Pi_infinitePi [IsProbabilityMeasure P] {μ : (i : ι) → Measure (𝓧 i)}
     (hX : ∀ i, HasLaw (X i) (μ i) P) (hm : AEMeasurable (fun ω i ↦ X i ω) P) :
     iIndepFun X P ↔ HasLaw (fun ω i ↦ X i ω) (infinitePi μ) P where
   mp h := h.hasLaw_infinitePi hX hm
@@ -118,8 +142,6 @@ lemma _root_.MeasureTheory.Measure.map_infinitePi_infinitePi_of_inj {α : Type*}
 
 section curry
 
-omit [IsProbabilityMeasure P]
-
 section dependent
 
 variable {κ : ι → Type*} {𝓧 : (i : ι) → κ i → Type*} {m𝓧 : ∀ i j, MeasurableSpace (𝓧 i j)}

Mathlib/Probability/Independence/Integration.lean

@@ -258,9 +258,9 @@ theorem IndepFun.integral_bilin_comp_comp
     (hf.comp_aemeasurable hX).isProbabilityMeasure_of_indepFun (f ∘ X) (g ∘ Y) h
       (hXY.comp₀ hX hY hf.1.aemeasurable hg.1.aemeasurable)
   rw [← integral_map (f := fun z ↦ B (f z.1) (g z.2)) (φ := fun ω ↦ (X ω, Y ω)) (by fun_prop),
-    (indepFun_iff_map_prod_eq_prod_map_map hX hY).1 hXY,
-    integral_prod_bilin _ hf hg, integral_map hX hf.1, integral_map hY hg.1]
-  rw [(indepFun_iff_map_prod_eq_prod_map_map hX hY).1 hXY]
+    hXY.map_prod_eq_prod_map_map hX hY, integral_prod_bilin _ hf hg, integral_map hX hf.1,
+    integral_map hY hg.1]
+  rw [hXY.map_prod_eq_prod_map_map hX hY]
   exact Continuous.comp_aestronglyMeasurable₂ (g := (B · ·)) (by fun_prop)
     hf.1.comp_fst hg.1.comp_snd
 
@@ -457,11 +457,11 @@ lemma iIndepFun.integral_fun_prod_comp (hX : iIndepFun X μ)
   have := hX.isProbabilityMeasure
   change ∫ ω, (fun x ↦ ∏ i, f i (x i)) (X · ω) ∂μ = _
   rw [← integral_map (f := fun x ↦ ∏ i, f i (x i)) (φ := fun ω ↦ (X · ω)),
-    (iIndepFun_iff_map_fun_eq_pi_map mX).1 hX, integral_fintype_prod_eq_prod]
+    hX.map_fun_eq_pi_map mX, integral_fintype_prod_eq_prod]
   · congr with i
     rw [integral_map (mX i) (hf i)]
   · fun_prop
-  rw [(iIndepFun_iff_map_fun_eq_pi_map mX).1 hX]
+  rw [hX.map_fun_eq_pi_map mX]
   exact Finset.aestronglyMeasurable_fun_prod Finset.univ fun i _ ↦
     (hf i).comp_quasiMeasurePreserving (Measure.quasiMeasurePreserving_eval _ i)