feat(measure_theory/measure/measure_space): let measure.map work with…

… ae_measurable functions (#13241)

Currently, `measure.map f μ` is zero if `f` is not measurable. This means that one can not say that two integrable random variables `X` and `Y` have the same distribution by requiring `measure.map X μ = measure.map Y μ`, as `X` or `Y` might not be measurable. We adjust the definition of `measure.map` to also work with almost everywhere measurable functions. This means that many results in the library that were only true for measurable functions become true for ae measurable functions. We generalize some of the existing code to this more general setting.

src/dynamics/ergodic/measure_preserving.lean

@@ -52,6 +52,10 @@ namespace measure_preserving
 protected lemma id (μ : measure α) : measure_preserving id μ μ :=
 ⟨measurable_id, map_id⟩
 
+protected lemma ae_measurable {f : α → β} (hf : measure_preserving f μa μb) :
+  ae_measurable f μa :=
+hf.1.ae_measurable
+
 lemma symm {e : α ≃ᵐ β} {μa : measure α} {μb : measure β} (h : measure_preserving e μa μb) :
   measure_preserving e.symm μb μa :=
 ⟨e.symm.measurable,
@@ -86,7 +90,7 @@ lemma comp {g : β → γ} {f : α → β} (hg : measure_preserving g μb μc)
 
 protected lemma sigma_finite {f : α → β} (hf : measure_preserving f μa μb) [sigma_finite μb] :
   sigma_finite μa :=
-sigma_finite.of_map μa hf.1 (by rwa hf.map_eq)
+sigma_finite.of_map μa hf.ae_measurable (by rwa hf.map_eq)
 
 lemma measure_preimage {f : α → β} (hf : measure_preserving f μa μb)
   {s : set β} (hs : measurable_set s) :

src/measure_theory/constructions/borel_space.lean

@@ -739,7 +739,7 @@ hf.borel_measurable.mono opens_measurable_space.borel_le
 
 /-- A continuous function from an `opens_measurable_space` to a `borel_space`
 is ae-measurable. -/
-lemma continuous.ae_measurable {f : α → γ} (h : continuous f) (μ : measure α) : ae_measurable f μ :=
+lemma continuous.ae_measurable {f : α → γ} (h : continuous f) {μ : measure α} : ae_measurable f μ :=
 h.measurable.ae_measurable
 
 lemma closed_embedding.measurable {f : α → γ} (hf : closed_embedding f) :

src/measure_theory/constructions/prod.lean

@@ -549,7 +549,7 @@ lemma map_prod_map {δ} [measurable_space δ] {f : α → β} {g : γ → δ}
   (hgc : sigma_finite (map g μc)) (hf : measurable f) (hg : measurable g) :
   (map f μa).prod (map g μc) = map (prod.map f g) (μa.prod μc) :=
 begin
-  haveI := hgc.of_map μc hg,
+  haveI := hgc.of_map μc hg.ae_measurable,
   refine prod_eq (λ s t hs ht, _),
   rw [map_apply (hf.prod_map hg) (hs.prod ht), map_apply hf hs, map_apply hg ht],
   exact prod_prod (f ⁻¹' s) (g ⁻¹' t)
@@ -575,10 +575,10 @@ begin
   to deduce `sigma_finite μc`. -/
   rcases eq_or_ne μa 0 with (rfl|ha),
   { rw [← hf.map_eq, zero_prod, measure.map_zero, zero_prod],
-    exact ⟨this, (mapₗ _).map_zero⟩ },
+    exact ⟨this, by simp only [measure.map_zero]⟩ },
   haveI : sigma_finite μc,
   { rcases (ae_ne_bot.2 ha).nonempty_of_mem hg with ⟨x, hx : map (g x) μc = μd⟩,
-    exact sigma_finite.of_map _ hgm.of_uncurry_left (by rwa hx) },
+    exact sigma_finite.of_map _ hgm.of_uncurry_left.ae_measurable (by rwa hx) },
   -- Thus we can apply `measure.prod_eq` to prove equality of measures.
   refine ⟨this, (prod_eq $ λ s t hs ht, _).symm⟩,
   rw [map_apply this (hs.prod ht)],
@@ -654,7 +654,7 @@ variables [sigma_finite ν]
 
 lemma lintegral_prod_swap [sigma_finite μ] (f : α × β → ℝ≥0∞)
   (hf : ae_measurable f (μ.prod ν)) : ∫⁻ z, f z.swap ∂(ν.prod μ) = ∫⁻ z, f z ∂(μ.prod ν) :=
-by { rw ← prod_swap at hf, rw [← lintegral_map' hf measurable_swap, prod_swap] }
+by { rw ← prod_swap at hf, rw [← lintegral_map' hf measurable_swap.ae_measurable, prod_swap] }
 
 /-- **Tonelli's Theorem**: For `ℝ≥0∞`-valued measurable functions on `α × β`,
   the integral of `f` is equal to the iterated integral. -/
@@ -831,7 +831,7 @@ lemma integral_prod_swap (f : α × β → E)
   (hf : ae_strongly_measurable f (μ.prod ν)) : ∫ z, f z.swap ∂(ν.prod μ) = ∫ z, f z ∂(μ.prod ν) :=
 begin
   rw ← prod_swap at hf,
-  rw [← integral_map measurable_swap hf, prod_swap]
+  rw [← integral_map measurable_swap.ae_measurable hf, prod_swap]
 end
 
 variables {E' : Type*} [normed_group E'] [complete_space E'] [normed_space ℝ E']

src/measure_theory/function/ess_sup.lean

@@ -152,7 +152,7 @@ variables {γ : Type*} {mγ : measurable_space γ} {f : α → γ} {g : γ → 
 
 include mγ
 
-lemma ess_sup_comp_le_ess_sup_map_measure (hf : measurable f) :
+lemma ess_sup_comp_le_ess_sup_map_measure (hf : ae_measurable f μ) :
   ess_sup (g ∘ f) μ ≤ ess_sup g (measure.map f μ) :=
 begin
   refine Limsup_le_Limsup_of_le (λ t, _) (by is_bounded_default) (by is_bounded_default),
@@ -165,7 +165,7 @@ end
 lemma _root_.measurable_embedding.ess_sup_map_measure (hf : measurable_embedding f) :
   ess_sup g (measure.map f μ) = ess_sup (g ∘ f) μ :=
 begin
-  refine le_antisymm _ (ess_sup_comp_le_ess_sup_map_measure hf.measurable),
+  refine le_antisymm _ (ess_sup_comp_le_ess_sup_map_measure hf.measurable.ae_measurable),
   refine Limsup_le_Limsup (by is_bounded_default) (by is_bounded_default) (λ c h_le, _),
   rw eventually_map at h_le ⊢,
   exact hf.ae_map_iff.mpr h_le,
@@ -174,7 +174,7 @@ end
 variables [measurable_space β] [topological_space β] [second_countable_topology β]
   [order_closed_topology β] [opens_measurable_space β]
 
-lemma ess_sup_map_measure_of_measurable (hg : measurable g) (hf : measurable f) :
+lemma ess_sup_map_measure_of_measurable (hg : measurable g) (hf : ae_measurable f μ) :
   ess_sup g (measure.map f μ) = ess_sup (g ∘ f) μ :=
 begin
   refine le_antisymm _ (ess_sup_comp_le_ess_sup_map_measure hf),
@@ -184,7 +184,7 @@ begin
   exact h_le,
 end
 
-lemma ess_sup_map_measure (hg : ae_measurable g (measure.map f μ)) (hf : measurable f) :
+lemma ess_sup_map_measure (hg : ae_measurable g (measure.map f μ)) (hf : ae_measurable f μ) :
   ess_sup g (measure.map f μ) = ess_sup (g ∘ f) μ :=
 begin
   rw [ess_sup_congr_ae hg.ae_eq_mk, ess_sup_map_measure_of_measurable hg.measurable_mk hf],

src/measure_theory/function/l1_space.lean

@@ -495,13 +495,17 @@ begin
 end
 
 lemma integrable_map_measure {f : α → δ} {g : δ → β}
-  (hg : ae_strongly_measurable g (measure.map f μ)) (hf : measurable f) :
+  (hg : ae_strongly_measurable g (measure.map f μ)) (hf : ae_measurable f μ) :
   integrable g (measure.map f μ) ↔ integrable (g ∘ f) μ :=
 by { simp_rw ← mem_ℒp_one_iff_integrable, exact mem_ℒp_map_measure_iff hg hf, }
 
+lemma integrable.comp_ae_measurable {f : α → δ} {g : δ → β}
+  (hg : integrable g (measure.map f μ)) (hf : ae_measurable f μ) : integrable (g ∘ f) μ :=
+(integrable_map_measure hg.ae_strongly_measurable hf).mp hg
+
 lemma integrable.comp_measurable {f : α → δ} {g : δ → β}
   (hg : integrable g (measure.map f μ)) (hf : measurable f) : integrable (g ∘ f) μ :=
-(integrable_map_measure hg.ae_strongly_measurable hf).mp hg
+hg.comp_ae_measurable hf.ae_measurable
 
 lemma _root_.measurable_embedding.integrable_map_iff
   {f : α → δ} (hf : measurable_embedding f) {g : δ → β} :
@@ -515,7 +519,7 @@ by { simp_rw ← mem_ℒp_one_iff_integrable, exact f.mem_ℒp_map_measure_iff,
 lemma measure_preserving.integrable_comp {ν : measure δ} {g : δ → β}
   {f : α → δ} (hf : measure_preserving f μ ν) (hg : ae_strongly_measurable g ν) :
   integrable (g ∘ f) μ ↔ integrable g ν :=
-by { rw ← hf.map_eq at hg ⊢, exact (integrable_map_measure hg hf.measurable).symm }
+by { rw ← hf.map_eq at hg ⊢, exact (integrable_map_measure hg hf.measurable.ae_measurable).symm }
 
 lemma measure_preserving.integrable_comp_emb {f : α → δ} {ν} (h₁ : measure_preserving f μ ν)
   (h₂ : measurable_embedding f) {g : δ → β} :

src/measure_theory/function/lp_space.lean

@@ -788,11 +788,11 @@ variables {β : Type*} {mβ : measurable_space β} {f : α → β} {g : β → E
 include mβ
 
 lemma snorm_ess_sup_map_measure
-  (hg : ae_strongly_measurable g (measure.map f μ)) (hf : measurable f) :
+  (hg : ae_strongly_measurable g (measure.map f μ)) (hf : ae_measurable f μ) :
   snorm_ess_sup g (measure.map f μ) = snorm_ess_sup (g ∘ f) μ :=
 ess_sup_map_measure hg.ennnorm hf
 
-lemma snorm_map_measure (hg : ae_strongly_measurable g (measure.map f μ)) (hf : measurable f) :
+lemma snorm_map_measure (hg : ae_strongly_measurable g (measure.map f μ)) (hf : ae_measurable f μ) :
   snorm g p (measure.map f μ) = snorm (g ∘ f) p μ :=
 begin
   by_cases hp_zero : p = 0,
@@ -804,9 +804,10 @@ begin
   rw lintegral_map' (hg.ennnorm.pow_const p.to_real) hf,
 end
 
-lemma mem_ℒp_map_measure_iff (hg : ae_strongly_measurable g (measure.map f μ)) (hf : measurable f) :
+lemma mem_ℒp_map_measure_iff
+  (hg : ae_strongly_measurable g (measure.map f μ)) (hf : ae_measurable f μ) :
   mem_ℒp g p (measure.map f μ) ↔ mem_ℒp (g ∘ f) p μ :=
-by simp [mem_ℒp, snorm_map_measure hg hf, hg.comp_measurable hf, hg]
+by simp [mem_ℒp, snorm_map_measure hg hf, hg.comp_ae_measurable hf, hg]
 
 lemma _root_.measurable_embedding.snorm_ess_sup_map_measure {g : β → F}
   (hf : measurable_embedding f) :

src/measure_theory/function/strongly_measurable.lean

@@ -1288,10 +1288,16 @@ lemma _root_.ae_strongly_measurable_of_ae_strongly_measurable_trim {α} {m m0 :
   ae_strongly_measurable f μ :=
 ⟨hf.mk f, strongly_measurable.mono hf.strongly_measurable_mk hm, ae_eq_of_ae_eq_trim hf.ae_eq_mk⟩
 
+lemma comp_ae_measurable {γ : Type*} {mγ : measurable_space γ} {mα : measurable_space α} {f : γ → α}
+  {μ : measure γ} (hg : ae_strongly_measurable g (measure.map f μ)) (hf : ae_measurable f μ) :
+  ae_strongly_measurable (g ∘ f) μ :=
+⟨(hg.mk g) ∘ hf.mk f, hg.strongly_measurable_mk.comp_measurable hf.measurable_mk,
+  (ae_eq_comp hf hg.ae_eq_mk).trans ((hf.ae_eq_mk).fun_comp (hg.mk g))⟩
+
 lemma comp_measurable {γ : Type*} {mγ : measurable_space γ} {mα : measurable_space α} {f : γ → α}
   {μ : measure γ} (hg : ae_strongly_measurable g (measure.map f μ)) (hf : measurable f) :
   ae_strongly_measurable (g ∘ f) μ :=
-⟨(hg.mk g) ∘ f, hg.strongly_measurable_mk.comp_measurable hf, ae_eq_comp hf hg.ae_eq_mk⟩
+hg.comp_ae_measurable hf.ae_measurable
 
 lemma is_separable_ae_range (hf : ae_strongly_measurable f μ) :
   ∃ (t : set β), is_separable t ∧ ∀ᵐ x ∂μ, f x ∈ t :=

src/measure_theory/group/integration.lean

@@ -130,7 +130,7 @@ begin
     simp_rw [map_map (measurable_id'.const_div g) (measurable_id'.const_mul g⁻¹).inv,
       function.comp, div_inv_eq_mul, mul_inv_cancel_left, map_id'],
     exact hf.ae_strongly_measurable },
-  { exact (measurable_id'.const_mul g⁻¹).inv }
+  { exact (measurable_id'.const_mul g⁻¹).inv.ae_measurable }
 end
 
 @[to_additive]

src/measure_theory/group/prod.lean

@@ -160,7 +160,7 @@ begin
   simp_rw [lintegral_lintegral h2f, lintegral_lintegral hf],
   conv_rhs { rw [← map_prod_mul_inv_eq μ ν] },
   symmetry,
-  exact lintegral_map' (hf.mono' (map_prod_mul_inv_eq μ ν).absolutely_continuous) h,
+  exact lintegral_map' (hf.mono' (map_prod_mul_inv_eq μ ν).absolutely_continuous) h.ae_measurable,
 end
 
 @[to_additive]

src/measure_theory/integral/bochner.lean

@@ -1292,13 +1292,13 @@ lemma integral_map_of_strongly_measurable {β} [measurable_space β] {φ : α 
 begin
   by_cases hfi : integrable f (measure.map φ μ), swap,
   { rw [integral_undef hfi, integral_undef],
-    rwa [← integrable_map_measure hfm.ae_strongly_measurable hφ] },
+    rwa [← integrable_map_measure hfm.ae_strongly_measurable hφ.ae_measurable] },
   borelize E,
   haveI : separable_space (range f ∪ {0} : set E) := hfm.separable_space_range_union_singleton,
   refine tendsto_nhds_unique
     (tendsto_integral_approx_on_of_measurable_of_range_subset hfm.measurable hfi _ subset.rfl) _,
   convert tendsto_integral_approx_on_of_measurable_of_range_subset (hfm.measurable.comp hφ)
-    ((integrable_map_measure hfm.ae_strongly_measurable hφ).1 hfi) (range f ∪ {0})
+    ((integrable_map_measure hfm.ae_strongly_measurable hφ.ae_measurable).1 hfi) (range f ∪ {0})
     (by simp [insert_subset_insert, set.range_comp_subset_range]) using 1,
   ext1 i,
   simp only [simple_func.approx_on_comp, simple_func.integral_eq, measure.map_apply, hφ,
@@ -1309,20 +1309,24 @@ begin
   simp,
 end
 
-lemma integral_map {β} [measurable_space β] {φ : α → β} (hφ : measurable φ)
+lemma integral_map {β} [measurable_space β] {φ : α → β} (hφ : ae_measurable φ μ)
   {f : β → E} (hfm : ae_strongly_measurable f (measure.map φ μ)) :
   ∫ y, f y ∂(measure.map φ μ) = ∫ x, f (φ x) ∂μ :=
 let g := hfm.mk f in calc
 ∫ y, f y ∂(measure.map φ μ) = ∫ y, g y ∂(measure.map φ μ) : integral_congr_ae hfm.ae_eq_mk
-... = ∫ x, g (φ x) ∂μ : integral_map_of_strongly_measurable hφ hfm.strongly_measurable_mk
+... = ∫ y, g y ∂(measure.map (hφ.mk φ) μ) :
+  by { congr' 1, exact measure.map_congr hφ.ae_eq_mk }
+... = ∫ x, g (hφ.mk φ x) ∂μ :
+  integral_map_of_strongly_measurable hφ.measurable_mk hfm.strongly_measurable_mk
+... = ∫ x, g (φ x) ∂μ : integral_congr_ae (hφ.ae_eq_mk.symm.fun_comp _)
 ... = ∫ x, f (φ x) ∂μ : integral_congr_ae $ ae_eq_comp hφ (hfm.ae_eq_mk).symm
 
 lemma _root_.measurable_embedding.integral_map {β} {_ : measurable_space β} {f : α → β}
   (hf : measurable_embedding f) (g : β → E) :
   ∫ y, g y ∂(measure.map f μ) = ∫ x, g (f x) ∂μ :=
 begin
   by_cases hgm : ae_strongly_measurable g (measure.map f μ),
-  { exact integral_map hf.measurable hgm },
+  { exact integral_map hf.measurable.ae_measurable hgm },
   { rw [integral_non_ae_strongly_measurable hgm, integral_non_ae_strongly_measurable],
     rwa ← hf.ae_strongly_measurable_map_iff }
 end

src/measure_theory/integral/lebesgue.lean

@@ -1948,11 +1948,14 @@ begin
 end
 
 lemma lintegral_map' {mβ : measurable_space β} {f : β → ℝ≥0∞} {g : α → β}
-  (hf : ae_measurable f (measure.map g μ)) (hg : measurable g) :
+  (hf : ae_measurable f (measure.map g μ)) (hg : ae_measurable g μ) :
   ∫⁻ a, f a ∂(measure.map g μ) = ∫⁻ a, f (g a) ∂μ :=
 calc ∫⁻ a, f a ∂(measure.map g μ) = ∫⁻ a, hf.mk f a ∂(measure.map g μ) :
   lintegral_congr_ae hf.ae_eq_mk
-... = ∫⁻ a, hf.mk f (g a) ∂μ : lintegral_map hf.measurable_mk hg
+... = ∫⁻ a, hf.mk f a ∂(measure.map (hg.mk g) μ) :
+  by { congr' 1, exact measure.map_congr hg.ae_eq_mk }
+... = ∫⁻ a, hf.mk f (hg.mk g a) ∂μ : lintegral_map hf.measurable_mk hg.measurable_mk
+... = ∫⁻ a, hf.mk f (g a) ∂μ : lintegral_congr_ae $ hg.ae_eq_mk.symm.fun_comp _
 ... = ∫⁻ a, f (g a) ∂μ : lintegral_congr_ae (ae_eq_comp hg hf.ae_eq_mk.symm)
 
 lemma lintegral_map_le {mβ : measurable_space β} (f : β → ℝ≥0∞) {g : α → β} (hg : measurable g) :

src/measure_theory/integral/set_integral.lean

@@ -274,11 +274,13 @@ calc ∫ a, indicator_const_Lp p ht hμt x a ∂μ
 ... = (μ t).to_real • x : by rw inter_univ
 
 lemma set_integral_map {β} [measurable_space β] {g : α → β} {f : β → E} {s : set β}
-  (hs : measurable_set s) (hf : ae_strongly_measurable f (measure.map g μ)) (hg : measurable g) :
+  (hs : measurable_set s)
+  (hf : ae_strongly_measurable f (measure.map g μ)) (hg : ae_measurable g μ) :
   ∫ y in s, f y ∂(measure.map g μ) = ∫ x in g ⁻¹' s, f (g x) ∂μ :=
 begin
-  rw [measure.restrict_map hg hs, integral_map hg (hf.mono_measure _)],
-  exact measure.map_mono g measure.restrict_le_self
+  rw [measure.restrict_map_of_ae_measurable hg hs,
+      integral_map (hg.mono_measure measure.restrict_le_self) (hf.mono_measure _)],
+  exact measure.map_mono_of_ae_measurable measure.restrict_le_self hg
 end
 
 lemma _root_.measurable_embedding.set_integral_map {β} {_ : measurable_space β} {f : α → β}

src/measure_theory/measure/ae_measurable.lean

@@ -120,9 +120,14 @@ lemma smul_measure [monoid R] [distrib_mul_action R ℝ≥0∞] [is_scalar_tower
   ae_measurable f (c • μ) :=
 ⟨h.mk f, h.measurable_mk, ae_smul_measure h.ae_eq_mk c⟩
 
-lemma comp_measurable {f : α → δ} {g : δ → β} (hg : ae_measurable g (μ.map f)) (hf : measurable f) :
-  ae_measurable (g ∘ f) μ :=
-⟨hg.mk g ∘ f, hg.measurable_mk.comp hf, ae_eq_comp hf hg.ae_eq_mk⟩
+lemma comp_ae_measurable {f : α → δ} {g : δ → β}
+  (hg : ae_measurable g (μ.map f)) (hf : ae_measurable f μ) : ae_measurable (g ∘ f) μ :=
+⟨hg.mk g ∘ hf.mk f, hg.measurable_mk.comp hf.measurable_mk,
+  (ae_eq_comp hf hg.ae_eq_mk).trans ((hf.ae_eq_mk).fun_comp (mk g hg))⟩
+
+lemma comp_measurable {f : α → δ} {g : δ → β}
+  (hg : ae_measurable g (μ.map f)) (hf : measurable f) : ae_measurable (g ∘ f) μ :=
+hg.comp_ae_measurable hf.ae_measurable
 
 lemma comp_measurable' {ν : measure δ} {f : α → δ} {g : δ → β} (hg : ae_measurable g ν)
   (hf : measurable f) (h : μ.map f ≪ ν) : ae_measurable (g ∘ f) μ :=
@@ -259,3 +264,27 @@ end
 lemma ae_measurable.indicator (hfm : ae_measurable f μ) {s} (hs : measurable_set s) :
   ae_measurable (s.indicator f) μ :=
 (ae_measurable_indicator_iff hs).mpr hfm.restrict
+
+lemma measure_theory.measure.restrict_map_of_ae_measurable
+  {f : α → δ} (hf : ae_measurable f μ) {s : set δ} (hs : measurable_set s) :
+  (μ.map f).restrict s = (μ.restrict $ f ⁻¹' s).map f :=
+calc
+(μ.map f).restrict s = (μ.map (hf.mk f)).restrict s :
+  by { congr' 1, apply measure.map_congr hf.ae_eq_mk }
+... = (μ.restrict $ (hf.mk f) ⁻¹' s).map (hf.mk f) :
+  measure.restrict_map hf.measurable_mk hs
+... = (μ.restrict $ (hf.mk f) ⁻¹' s).map f :
+  measure.map_congr (ae_restrict_of_ae (hf.ae_eq_mk.symm))
+... = (μ.restrict $ f ⁻¹' s).map f :
+begin
+  apply congr_arg,
+  ext1 t ht,
+  simp only [ht, measure.restrict_apply],
+  apply measure_congr,
+  apply (eventually_eq.refl _ _).inter (hf.ae_eq_mk.symm.preimage s)
+end
+
+lemma measure_theory.measure.map_mono_of_ae_measurable
+  {f : α → δ} (h : μ ≤ ν) (hf : ae_measurable f ν) :
+  μ.map f ≤ ν.map f :=
+λ s hs, by simpa [hf, hs, hf.mono_measure h] using measure.le_iff'.1 h (f ⁻¹' s)

src/measure_theory/measure/lebesgue.lean

@@ -454,10 +454,10 @@ begin
   { apply measure_congr,
     apply eventually_eq.rfl.inter,
     exact
-      ((ae_eq_comp' measurable_fst hf.ae_eq_mk measure.prod_fst_absolutely_continuous).comp₂ _
-        eventually_eq.rfl).inter
-      (eventually_eq.rfl.comp₂ _
-        (ae_eq_comp' measurable_fst hg.ae_eq_mk measure.prod_fst_absolutely_continuous)) },
+      ((ae_eq_comp' measurable_fst.ae_measurable
+        hf.ae_eq_mk measure.prod_fst_absolutely_continuous).comp₂ _ eventually_eq.rfl).inter
+      (eventually_eq.rfl.comp₂ _ (ae_eq_comp' measurable_fst.ae_measurable
+        hg.ae_eq_mk measure.prod_fst_absolutely_continuous)) },
   rw [lintegral_congr_ae h₁,
       ← volume_region_between_eq_lintegral' hf.measurable_mk hg.measurable_mk hs],
   convert h₂ using 1,