feat(measure_theory/interval_integral): improve integral_comp lemmas (#6795)

I expand our collection of `integral_comp` lemmas so that they can handle all interval integrals of the form
`∫ x in a..b, f (c * x + d)`, for any function `f : ℝ → E`  and any real constants `c` and `d` such that `c ≠ 0`.


This PR now also removes the `ae_measurable` assumptions from the preexisting `interval_comp` lemmas (thank you @sgouezel!).



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: benjamindavidson

src/data/equiv/mul_add.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Callum Sutton, Yury Kudryashov
 import algebra.group.hom
 import algebra.group.type_tags
 import algebra.group.units_hom
+import algebra.group_with_zero
 
 /-!
 # Multiplicative and additive equivs
@@ -478,6 +479,37 @@ lemma inv_symm : (equiv.inv G).symm = equiv.inv G := rfl
 
 end group
 
+section group_with_zero
+variables [group_with_zero G]
+
+/-- Left multiplication by a nonzero element in a `group_with_zero` is a permutation of the
+underlying type. -/
+protected def mul_left' (a : G) (ha : a ≠ 0) : perm G :=
+{ to_fun := λ x, a * x,
+  inv_fun := λ x, a⁻¹ * x,
+  left_inv := λ x, by { dsimp, rw [← mul_assoc, inv_mul_cancel ha, one_mul] },
+  right_inv := λ x, by { dsimp, rw [← mul_assoc, mul_inv_cancel ha, one_mul] } }
+
+@[simp] lemma coe_mul_left' (a : G) (ha : a ≠ 0) : ⇑(equiv.mul_left' a ha) = (*) a := rfl
+
+@[simp] lemma mul_left'_symm_apply (a : G) (ha : a ≠ 0) :
+  ((equiv.mul_left' a ha).symm : G → G) = (*) a⁻¹ := rfl
+
+/-- Right multiplication by a nonzero element in a `group_with_zero` is a permutation of the
+underlying type. -/
+protected def mul_right' (a : G) (ha : a ≠ 0) : perm G :=
+{ to_fun := λ x, x * a,
+  inv_fun := λ x, x * a⁻¹,
+  left_inv := λ x, by { dsimp, rw [mul_assoc, mul_inv_cancel ha, mul_one] },
+  right_inv := λ x, by { dsimp, rw [mul_assoc, inv_mul_cancel ha, mul_one] } }
+
+@[simp] lemma coe_mul_right' (a : G) (ha : a ≠ 0) : ⇑(equiv.mul_right' a ha) = λ x, x * a := rfl
+
+@[simp] lemma mul_right'_symm_apply (a : G) (ha : a ≠ 0) :
+  ((equiv.mul_right' a ha).symm : G → G) = λ x, x * a⁻¹ := rfl
+
+end group_with_zero
+
 end equiv
 
 section type_tags

src/measure_theory/bochner_integration.lean

@@ -1095,8 +1095,7 @@ by { simp_rw [← of_real_norm_eq_coe_nnnorm], apply ennreal.of_real_le_of_le_to
   exact norm_integral_le_lintegral_norm f }
 
 lemma integral_eq_zero_of_ae {f : α → E} (hf : f =ᵐ[μ] 0) : ∫ a, f a ∂μ = 0 :=
-if hfm : ae_measurable f μ then by simp [integral_congr_ae hf, integral_zero]
-else integral_non_ae_measurable hfm
+by simp [integral_congr_ae hf, integral_zero]
 
 /-- If `f` has finite integral, then `∫ x in s, f x ∂μ` is absolutely continuous in `s`: it tends
 to zero as `μ s` tends to zero. -/
@@ -1549,6 +1548,17 @@ let g := hfm.mk f in calc
 ... = ∫ x, g (φ x) ∂μ : integral_map_of_measurable hφ hfm.measurable_mk
 ... = ∫ x, f (φ x) ∂μ : integral_congr_ae $ ae_eq_comp hφ (hfm.ae_eq_mk).symm
 
+lemma integral_map_of_closed_embedding {β} [topological_space α] [borel_space α]
+  [topological_space β] [measurable_space β] [borel_space β]
+  {φ : α → β} (hφ : closed_embedding φ) (f : β → E) :
+  ∫ y, f y ∂(measure.map φ μ) = ∫ x, f (φ x) ∂μ :=
+begin
+  by_cases hfm : ae_measurable f (measure.map φ μ),
+  { exact integral_map hφ.continuous.measurable hfm },
+  { rw [integral_non_ae_measurable hfm, integral_non_ae_measurable],
+    rwa ae_measurable_comp_right_iff_of_closed_embedding hφ }
+end
+
 lemma integral_dirac' (f : α → E) (a : α) (hfm : measurable f) :
   ∫ x, f x ∂(measure.dirac a) = f a :=
 calc ∫ x, f x ∂(measure.dirac a) = ∫ x, f a ∂(measure.dirac a) :

src/measure_theory/borel_space.lean

@@ -387,6 +387,10 @@ lemma continuous.measurable {f : α → γ} (hf : continuous f) :
 hf.borel_measurable.mono opens_measurable_space.borel_le
   (le_of_eq $ borel_space.measurable_eq)
 
+lemma closed_embedding.measurable {f : α → γ} (hf : closed_embedding f) :
+  measurable f :=
+hf.continuous.measurable
+
 @[priority 100, to_additive]
 instance has_continuous_mul.has_measurable_mul [has_mul γ] [has_continuous_mul γ] :
   has_measurable_mul γ :=
@@ -428,6 +432,9 @@ rfl
   (h.to_measurable_equiv.symm : γ₂ → γ) = h.symm :=
 rfl
 
+lemma homeomorph.measurable (h : α ≃ₜ γ) : measurable h :=
+h.continuous.measurable
+
 end homeomorph
 
 lemma measurable_of_continuous_on_compl_singleton [t1_space α] {f : α → γ} (a : α)
@@ -524,7 +531,7 @@ end
 lemma measurable_comp_iff_of_closed_embedding {f : δ → β} (g : β → γ) (hg : closed_embedding g) :
   measurable (g ∘ f) ↔ measurable f :=
 begin
-  refine ⟨λ hf, _, λ hf, hg.continuous.measurable.comp hf⟩,
+  refine ⟨λ hf, _, λ hf, hg.measurable.comp hf⟩,
   apply measurable_of_is_closed, intros s hs,
   convert hf (hg.is_closed_map s hs).measurable_set,
   rw [@preimage_comp _ _ _ f g, preimage_image_eq _ hg.to_embedding.inj]
@@ -535,7 +542,7 @@ lemma ae_measurable_comp_iff_of_closed_embedding {f : δ → β} {μ : measure 
 begin
   by_cases h : nonempty β,
   { resetI,
-    refine ⟨λ hf, _, λ hf, hg.continuous.measurable.comp_ae_measurable hf⟩,
+    refine ⟨λ hf, _, λ hf, hg.measurable.comp_ae_measurable hf⟩,
     convert hg.measurable_inv_fun.comp_ae_measurable hf,
     ext x,
     exact (function.left_inverse_inv_fun hg.to_embedding.inj (f x)).symm },
@@ -544,6 +551,26 @@ begin
           (measurable_of_not_nonempty H f).ae_measurable] }
 end
 
+lemma ae_measurable_comp_right_iff_of_closed_embedding {g : α → β} {μ : measure α}
+  {f : β → δ} (hg : closed_embedding g) :
+  ae_measurable (f ∘ g) μ ↔ ae_measurable f (measure.map g μ) :=
+begin
+  refine ⟨λ h, _, λ h, h.comp_measurable hg.measurable⟩,
+  by_cases hα : nonempty α,
+  swap, { simp [measure.eq_zero_of_not_nonempty hα μ] },
+  resetI,
+  refine ⟨(h.mk _) ∘ (function.inv_fun g), h.measurable_mk.comp hg.measurable_inv_fun, _⟩,
+  have : μ = measure.map (function.inv_fun g) (measure.map g μ),
+    by rw [measure.map_map hg.measurable_inv_fun hg.measurable,
+           (function.left_inverse_inv_fun hg.to_embedding.inj).comp_eq_id, measure.map_id],
+  rw this at h,
+  filter_upwards [ae_of_ae_map hg.measurable_inv_fun h.ae_eq_mk,
+    ae_map_mem_range g hg.closed_range.measurable_set μ],
+  assume x hx₁ hx₂,
+  convert hx₁,
+  exact ((function.left_inverse_inv_fun hg.to_embedding.inj).right_inv_on_range hx₂).symm,
+end
+
 section linear_order
 
 variables [linear_order α] [order_topology α] [second_countable_topology α]
@@ -1302,7 +1329,7 @@ protected lemma map [opens_measurable_space α] [measurable_space β] [topologic
   [t2_space β] [borel_space β] (hμ : μ.regular) (f : α ≃ₜ β) :
   (measure.map f μ).regular :=
 begin
-  have hf := f.continuous.measurable,
+  have hf := f.measurable,
   have h2f := f.to_equiv.injective.preimage_surjective,
   have h3f := f.to_equiv.surjective,
   split,

src/measure_theory/interval_integral.lean

@@ -278,7 +278,7 @@ notation `∫` binders ` in ` a `..` b `, ` r:(scoped:60 f, interval_integral f
 
 namespace interval_integral
 
-section
+section basic
 
 variables {a b c d : α} {f g : α → E} {μ : measure α}
 
@@ -370,39 +370,109 @@ lemma integral_smul_measure (c : ℝ≥0∞) :
   ∫ x in a..b, f x ∂(c • μ) = c.to_real • ∫ x in a..b, f x ∂μ :=
 by simp only [interval_integral, measure.restrict_smul, integral_smul_measure, smul_sub]
 
-lemma integral_comp_add_right {a b : ℝ} (c : ℝ) {f : ℝ → E} (hfm : ae_measurable f) :
-  ∫ x in a..b, f (x + c) = ∫ x in a+c..b+c, f x :=
-have A : ae_measurable f (measure.map (λ x, x + c) volume), by rwa [real.map_volume_add_right],
-calc ∫ x in a..b, f (x + c) = ∫ x in a+c..b+c, f x ∂(measure.map (λ x, x + c) volume) :
-  by simp only [interval_integral, set_integral_map measurable_set_Ioc A (measurable_add_const _),
-    preimage_add_const_Ioc, add_sub_cancel]
-... = ∫ x in a+c..b+c, f x : by rw [real.map_volume_add_right]
+end basic
+
+section comp
 
-lemma integral_comp_mul_right {a b c : ℝ} {f : ℝ → E} (hc : 0 < c) (hfm : ae_measurable f) :
+variables {a b c : ℝ} (f : ℝ → E)
+
+lemma integral_comp_mul_right_of_pos (hc : 0 < c) :
   ∫ x in a..b, f (x * c) = c⁻¹ • ∫ x in a*c..b*c, f x :=
 begin
-  have A : ae_measurable f (measure.map (λ (x : ℝ), x*c) volume),
-    by { rw real.map_volume_mul_right (ne_of_gt hc), exact hfm.smul_measure _ },
-  conv_rhs { rw [← real.smul_map_volume_mul_right (ne_of_gt hc)] },
+  have A : closed_embedding (λ x, x * c) := (homeomorph.mul_right' c hc.ne').closed_embedding,
+  conv_rhs { rw [← real.smul_map_volume_mul_right hc.ne'] },
   rw [integral_smul_measure],
-  simp only [interval_integral, set_integral_map measurable_set_Ioc A (measurable_mul_const _),
-    hc, preimage_mul_const_Ioc, mul_div_cancel _ (ne_of_gt hc), abs_of_pos,
-    ennreal.to_real_of_real (le_of_lt hc), inv_smul_smul' (ne_of_gt hc)],
+  simp only [interval_integral, hc, preimage_mul_const_Ioc, mul_div_cancel _ hc.ne',
+    abs_of_pos, set_integral_map_of_closed_embedding measurable_set_Ioc A,
+    ennreal.to_real_of_real hc.le, inv_smul_smul' hc.ne'],
 end
 
-lemma integral_comp_mul_left {a b c : ℝ} {f : ℝ → E} (hc : 0 < c) (hfm : ae_measurable f) :
+lemma integral_comp_neg : ∫ x in a..b, f (-x) = ∫ x in -b..-a, f x :=
+begin
+  have A : closed_embedding (λ x, -x) := (homeomorph.neg ℝ).closed_embedding,
+  conv_rhs { rw ← real.map_volume_neg },
+  simp only [interval_integral, set_integral_map_of_closed_embedding measurable_set_Ioc A,
+    neg_preimage, preimage_neg_Ioc, neg_neg, restrict_congr_set Ico_ae_eq_Ioc],
+end
+
+lemma integral_comp_mul_right_of_neg (hc : c < 0) :
+  ∫ x in a..b, f (x * c) = c⁻¹ • ∫ x in a*c..b*c, f x :=
+begin
+  let g := λ x, f (-x),
+  have h : (λ x, f (x * c)) = λ x, g (x * -c) := by simp_rw [g, neg_mul_eq_mul_neg, neg_neg],
+  rw [h, integral_comp_mul_right_of_pos g (neg_pos.mpr hc), integral_comp_neg f, integral_symm],
+  simp only [neg_mul_eq_mul_neg, neg_neg, inv_neg, neg_smul, ← smul_neg],
+end
+
+lemma integral_comp_mul_right (hc : c ≠ 0) :
+  ∫ x in a..b, f (x * c) = c⁻¹ • ∫ x in a*c..b*c, f x :=
+begin
+  cases lt_or_gt_of_ne hc with hneg hpos,
+  exacts [integral_comp_mul_right_of_neg f hneg, integral_comp_mul_right_of_pos f hpos],
+end
+
+lemma integral_comp_mul_left (hc : c ≠ 0) :
   ∫ x in a..b, f (c * x) = c⁻¹ • ∫ x in c*a..c*b, f x :=
-by simpa only [mul_comm c] using integral_comp_mul_right hc hfm
+by simpa only [mul_comm c] using integral_comp_mul_right f hc
+
+lemma integral_comp_div (hc : c ≠ 0) :
+  ∫ x in a..b, f (x / c) = c • ∫ x in a/c..b/c, f x :=
+by simpa only [inv_inv'] using integral_comp_mul_right f (inv_ne_zero hc)
 
-lemma integral_comp_neg {a b : ℝ} {f : ℝ → E} (hfm : ae_measurable f) :
-  ∫ x in a..b, f (-x) = ∫ x in -b..-a, f x :=
+lemma integral_comp_add_right (d : ℝ) :
+  ∫ x in a..b, f (x + d) = ∫ x in a+d..b+d, f x :=
+have A : closed_embedding (λ x, x + d) := (homeomorph.add_right d).closed_embedding,
+calc ∫ x in a..b, f (x + d) = ∫ x in a+d..b+d, f x ∂(measure.map (λ x, x + d) volume) :
+  by simp only [interval_integral, set_integral_map_of_closed_embedding measurable_set_Ioc A,
+    preimage_add_const_Ioc, add_sub_cancel]
+... = ∫ x in a+d..b+d, f x : by rw [real.map_volume_add_right]
+
+lemma integral_comp_mul_add (hc : c ≠ 0) (d : ℝ) :
+  ∫ x in a..b, f (c * x + d) = c⁻¹ • ∫ x in c*a+d..c*b+d, f x :=
+by rw [← integral_comp_add_right f d, ← integral_comp_mul_left _ hc]
+
+lemma integral_comp_add_mul (hc : c ≠ 0) (d : ℝ) :
+  ∫ x in a..b, f (d + c * x) = c⁻¹ • ∫ x in d+c*a..d+c*b, f x :=
+by simpa only [add_comm] using integral_comp_mul_add f hc d
+
+lemma integral_comp_div_add (hc : c ≠ 0) (d : ℝ) :
+  ∫ x in a..b, f (x / c + d) = c • ∫ x in a/c+d..b/c+d, f x :=
+by simpa only [div_eq_inv_mul, inv_inv'] using integral_comp_mul_add f (inv_ne_zero hc) d
+
+lemma integral_comp_add_div (hc : c ≠ 0) (d : ℝ) :
+  ∫ x in a..b, f (d + x / c) = c • ∫ x in d+a/c..d+b/c, f x :=
+by simpa only [div_eq_inv_mul, inv_inv'] using integral_comp_add_mul f (inv_ne_zero hc) d
+
+lemma integral_comp_mul_sub (hc : c ≠ 0) (d : ℝ) :
+  ∫ x in a..b, f (c * x - d) = c⁻¹ • ∫ x in c*a-d..c*b-d, f x :=
+by simpa only [sub_eq_add_neg] using integral_comp_mul_add f hc (-d)
+
+lemma integral_comp_sub_mul (hc : c ≠ 0) (d : ℝ) :
+  ∫ x in a..b, f (d - c * x) = c⁻¹ • ∫ x in d-c*b..d-c*a, f x :=
 begin
-  have A : ae_measurable f (measure.map (λ (x : ℝ), -x) volume), by rwa real.map_volume_neg,
-  conv_rhs { rw ← real.map_volume_neg },
-  simp only [interval_integral, set_integral_map measurable_set_Ioc A measurable_neg, neg_preimage,
-    preimage_neg_Ioc, neg_neg, restrict_congr_set Ico_ae_eq_Ioc]
+  simp only [sub_eq_add_neg, neg_mul_eq_neg_mul],
+  rw [integral_comp_add_mul f (neg_ne_zero.mpr hc) d, integral_symm],
+  simp only [inv_neg, smul_neg, neg_neg, neg_smul],
 end
 
+lemma integral_comp_div_sub (hc : c ≠ 0) (d : ℝ) :
+  ∫ x in a..b, f (x / c - d) = c • ∫ x in a/c-d..b/c-d, f x :=
+by simpa only [div_eq_inv_mul, inv_inv'] using integral_comp_mul_sub f (inv_ne_zero hc) d
+
+lemma integral_comp_sub_div (hc : c ≠ 0) (d : ℝ) :
+  ∫ x in a..b, f (d - x / c) = c • ∫ x in d-b/c..d-a/c, f x :=
+by simpa only [div_eq_inv_mul, inv_inv'] using integral_comp_sub_mul f (inv_ne_zero hc) d
+
+lemma integral_comp_sub_right (d : ℝ) :
+  ∫ x in a..b, f (x - d) = ∫ x in a-d..b-d, f x :=
+by simpa only [sub_eq_add_neg] using integral_comp_add_right f (-d)
+
+lemma integral_comp_sub_left (d : ℝ) :
+  ∫ x in a..b, f (d - x) = ∫ x in d-b..d-a, f x :=
+by simpa only [one_mul, one_smul, inv_one] using integral_comp_sub_mul f one_ne_zero d
+
+end comp
+
 /-!
 ### Integral is an additive function of the interval
 
@@ -411,14 +481,13 @@ as well as a few other identities trivially equivalent to this one. We also prov
 `∫ x in a..b, f x ∂μ = ∫ x, f x ∂μ` provided that `support f ⊆ Ioc a b`.
 -/
 
-variables [topological_space α] [opens_measurable_space α]
-
 section order_closed_topology
 
-variables [order_closed_topology α]
+variables [topological_space α] [order_closed_topology α] [opens_measurable_space α]
+  {a b c d : α} {f g : α → E} {μ : measure α}
 
 /-- If two functions are equal in the relevant interval, their interval integrals are also equal. -/
-lemma integral_congr {a b : α} {f g : α → E} (h : eq_on f g (interval a b)) :
+lemma integral_congr {a b : α} (h : eq_on f g (interval a b)) :
   ∫ x in a..b, f x ∂μ = ∫ x in a..b, g x ∂μ :=
 by cases le_total a b with hab hab; simpa [hab, integral_of_le, integral_of_ge]
   using set_integral_congr measurable_set_Ioc (h.mono Ioc_subset_Icc_self)
@@ -497,8 +566,6 @@ end
 
 end order_closed_topology
 
-end
-
 lemma integral_eq_zero_iff_of_le_of_nonneg_ae {f : ℝ → ℝ} {a b : ℝ} (hab : a ≤ b)
   (hf : 0 ≤ᵐ[volume.restrict (Ioc a b)] f) (hfi : interval_integrable f volume a b) :
   ∫ x in a..b, f x = 0 ↔ f =ᵐ[volume.restrict (Ioc a b)] 0 :=

src/measure_theory/measure_space.lean

@@ -1519,10 +1519,33 @@ lemma mem_ae_map_iff {f : α → β} (hf : measurable f) {s : set β} (hs : meas
   s ∈ (map f μ).ae ↔ (f ⁻¹' s) ∈ μ.ae :=
 by simp only [mem_ae_iff, map_apply hf hs.compl, preimage_compl]
 
+lemma mem_ae_of_mem_ae_map {f : α → β} (hf : measurable f) {s : set β} (hs : s ∈ (map f μ).ae) :
+  f ⁻¹' s ∈ μ.ae :=
+begin
+  apply le_antisymm _ bot_le,
+  calc μ (f ⁻¹' sᶜ) ≤ (map f μ) sᶜ : le_map_apply hf sᶜ
+  ... = 0 : hs
+end
+
 lemma ae_map_iff {f : α → β} (hf : measurable f) {p : β → Prop} (hp : measurable_set {x | p x}) :
   (∀ᵐ y ∂ (map f μ), p y) ↔ ∀ᵐ x ∂ μ, p (f x) :=
 mem_ae_map_iff hf hp
 
+lemma ae_of_ae_map {f : α → β} (hf : measurable f) {p : β → Prop} (h : ∀ᵐ y ∂ (map f μ), p y) :
+  ∀ᵐ x ∂ μ, p (f x) :=
+mem_ae_of_mem_ae_map hf h
+
+lemma ae_map_mem_range (f : α → β) (hf : measurable_set (range f)) (μ : measure α) :
+  ∀ᵐ x ∂(map f μ), x ∈ range f :=
+begin
+  by_cases h : measurable f,
+  { change range f ∈ (map f μ).ae,
+    rw mem_ae_map_iff h hf,
+    apply eventually_of_forall,
+    exact mem_range_self },
+  { simp [map_of_not_measurable h] }
+end
+
 lemma ae_restrict_iff {p : α → Prop} (hp : measurable_set {x | p x}) :
   (∀ᵐ x ∂(μ.restrict s), p x) ↔ ∀ᵐ x ∂μ, x ∈ s → p x :=
 begin
@@ -1534,7 +1557,7 @@ lemma ae_imp_of_ae_restrict {s : set α} {p : α → Prop} (h : ∀ᵐ x ∂(μ.
   ∀ᵐ x ∂μ, x ∈ s → p x :=
 begin
   simp only [ae_iff] at h ⊢,
-  simpa [set_of_and, inter_comm] using  measure_inter_eq_zero_of_restrict h
+  simpa [set_of_and, inter_comm] using measure_inter_eq_zero_of_restrict h
 end
 
 lemma ae_restrict_iff' {s : set α} {p : α → Prop} (hp : measurable_set s) :

src/measure_theory/set_integral.lean

@@ -435,6 +435,12 @@ begin
   exact measure.map_mono g measure.restrict_le_self
 end
 
+lemma set_integral_map_of_closed_embedding [topological_space α] [borel_space α]
+  {β} [measurable_space β] [topological_space β] [borel_space β]
+  {g : α → β} {f : β → E} {s : set β} (hs : measurable_set s) (hg : closed_embedding g) :
+  ∫ y in s, f y ∂(measure.map g μ) = ∫ x in g ⁻¹' s, f (g x) ∂μ :=
+by rw [measure.restrict_map hg.measurable hs, integral_map_of_closed_embedding hg]
+
 lemma norm_set_integral_le_of_norm_le_const_ae {C : ℝ} (hs : μ s < ∞)
   (hC : ∀ᵐ x ∂μ.restrict s, ∥f x∥ ≤ C) :
   ∥∫ x in s, f x ∂μ∥ ≤ C * (μ s).to_real :=