feat(measure_theory/interval_integral): make integral_comp lemmas com…

…putable by simp (#7010)

A follow-up to #6795,  enabling the computation of integrals of the form `∫ x in a..b, f (c * x + d)` by `simp`, where `f` is a function whose integral is already in mathlib and `c` and `d` are any real constants such that `c ≠ 0`.



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

src/measure_theory/interval_integral.lean

@@ -376,7 +376,7 @@ section comp
 
 variables {a b c : ℝ} (f : ℝ → E)
 
-lemma integral_comp_mul_right (hc : c ≠ 0) :
+@[simp] 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
   have A : closed_embedding (λ x, x * c) := (homeomorph.mul_right' c hc).closed_embedding,
@@ -389,63 +389,63 @@ begin
   { simp [(show 0 < c, from h), mul_div_cancel, hc, abs_of_pos] }
 end
 
-lemma integral_comp_mul_left (hc : c ≠ 0) :
+@[simp] 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 f hc
 
-lemma integral_comp_div (hc : c ≠ 0) :
+@[simp] 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_add_right (d : ℝ) :
+@[simp] 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 [interval_integral, set_integral_map_of_closed_embedding _ A]
 ... = ∫ x in a+d..b+d, f x : by rw [real.map_volume_add_right]
 
-lemma integral_comp_mul_add (hc : c ≠ 0) (d : ℝ) :
+@[simp] 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 : ℝ) :
+@[simp] 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 : ℝ) :
+@[simp] 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 : ℝ) :
+@[simp] 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 : ℝ) :
+@[simp] 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 : ℝ) :
+@[simp] 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
   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 : ℝ) :
+@[simp] 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 : ℝ) :
+@[simp] 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 : ℝ) :
+@[simp] 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 : ℝ) :
+@[simp] 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