feat(analysis/special_functions/integrals): integral_comp for f : ℝ → ℝ (#7216)

In #7103 I added lemmas to deal with integrals of the form `c • ∫ x in a..b, f (c * x + d)`. However, it came to my attention that, with those lemmas, `simp` can only handle such integrals if they use `•`, not `*`. To solve this problem and enable computation of these integrals by `simp`, I add versions of the aforementioned `integral_comp` lemmas specialized with `f : ℝ → ℝ` and label them with `simp`.

Author: benjamindavidson

src/analysis/special_functions/integrals.lean

@@ -28,20 +28,64 @@ variables {a b : ℝ}
 
 namespace interval_integral
 open measure_theory
-variables {f : ℝ → ℝ} {μ ν : measure ℝ} [locally_finite_measure μ]
+variables {f : ℝ → ℝ} {μ ν : measure ℝ} [locally_finite_measure μ] (c d : ℝ)
 
 @[simp]
-lemma integral_const_mul (c : ℝ) : ∫ x in a..b, c * f x = c * ∫ x in a..b, f x :=
+lemma integral_const_mul : ∫ x in a..b, c * f x = c * ∫ x in a..b, f x :=
 integral_smul c
 
 @[simp]
-lemma integral_mul_const (c : ℝ) : ∫ x in a..b, f x * c = (∫ x in a..b, f x) * c :=
+lemma integral_mul_const : ∫ x in a..b, f x * c = (∫ x in a..b, f x) * c :=
 by simp only [mul_comm, integral_const_mul]
 
 @[simp]
-lemma integral_div (c : ℝ) : ∫ x in a..b, f x / c = (∫ x in a..b, f x) / c :=
+lemma integral_div : ∫ x in a..b, f x / c = (∫ x in a..b, f x) / c :=
 integral_mul_const c⁻¹
 
+@[simp]
+lemma mul_integral_comp_mul_right : c * ∫ x in a..b, f (x * c) = ∫ x in a*c..b*c, f x :=
+smul_integral_comp_mul_right f c
+
+@[simp]
+lemma mul_integral_comp_mul_left : c * ∫ x in a..b, f (c * x) = ∫ x in c*a..c*b, f x :=
+smul_integral_comp_mul_left f c
+
+@[simp]
+lemma inv_mul_integral_comp_div : c⁻¹ * ∫ x in a..b, f (x / c) = ∫ x in a/c..b/c, f x :=
+inv_smul_integral_comp_div f c
+
+@[simp]
+lemma mul_integral_comp_mul_add : c * ∫ x in a..b, f (c * x + d) = ∫ x in c*a+d..c*b+d, f x :=
+smul_integral_comp_mul_add f c d
+
+@[simp]
+lemma mul_integral_comp_add_mul : c * ∫ x in a..b, f (d + c * x) = ∫ x in d+c*a..d+c*b, f x :=
+smul_integral_comp_add_mul f c d
+
+@[simp]
+lemma inv_mul_integral_comp_div_add : c⁻¹ * ∫ x in a..b, f (x / c + d) = ∫ x in a/c+d..b/c+d, f x :=
+inv_smul_integral_comp_div_add f c d
+
+@[simp]
+lemma inv_mul_integral_comp_add_div : c⁻¹ * ∫ x in a..b, f (d + x / c) = ∫ x in d+a/c..d+b/c, f x :=
+inv_smul_integral_comp_add_div f c d
+
+@[simp]
+lemma mul_integral_comp_mul_sub : c * ∫ x in a..b, f (c * x - d) = ∫ x in c*a-d..c*b-d, f x :=
+smul_integral_comp_mul_sub f c d
+
+@[simp]
+lemma mul_integral_comp_sub_mul : c * ∫ x in a..b, f (d - c * x) = ∫ x in d-c*b..d-c*a, f x :=
+smul_integral_comp_sub_mul f c d
+
+@[simp]
+lemma inv_mul_integral_comp_div_sub : c⁻¹ * ∫ x in a..b, f (x / c - d) = ∫ x in a/c-d..b/c-d, f x :=
+inv_smul_integral_comp_div_sub f c d
+
+@[simp]
+lemma inv_mul_integral_comp_sub_div : c⁻¹ * ∫ x in a..b, f (d - x / c) = ∫ x in d-b/c..d-a/c, f x :=
+inv_smul_integral_comp_sub_div f c d
+
 @[simp]
 lemma interval_integrable_pow (n : ℕ) : interval_integrable (λ x, x^n) μ a b :=
 (continuous_pow n).interval_integrable a b

src/measure_theory/interval_integral.lean

@@ -355,7 +355,7 @@ by { simp only [interval_integral, integral_neg], abel }
   ∫ x in a..b, f x - g x ∂μ = ∫ x in a..b, f x ∂μ - ∫ x in a..b, g x ∂μ :=
 by simpa only [sub_eq_add_neg] using (integral_add hf hg.neg).trans (congr_arg _ integral_neg)
 
-lemma integral_smul (r : ℝ) : ∫ x in a..b, r • f x ∂μ = r • ∫ x in a..b, f x ∂μ :=
+@[simp] lemma integral_smul (r : ℝ) : ∫ x in a..b, r • f x ∂μ = r • ∫ x in a..b, f x ∂μ :=
 by simp only [interval_integral, integral_smul, smul_sub]
 
 lemma integral_const' (c : E) :
@@ -389,23 +389,23 @@ begin
   { simp [(show 0 < c, from h), mul_div_cancel, hc, abs_of_pos] }
 end
 
-@[simp] lemma integral_comp_mul_right' (c) :
+@[simp] lemma smul_integral_comp_mul_right (c) :
   c • ∫ x in a..b, f (x * c) = ∫ x in a*c..b*c, f x :=
 by by_cases hc : c = 0; simp [hc]
 
 @[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
 
-@[simp] lemma integral_comp_mul_left' (c) :
+@[simp] lemma smul_integral_comp_mul_left (c) :
   c • ∫ x in a..b, f (c * x) = ∫ x in c*a..c*b, f x :=
 by by_cases hc : c = 0; simp [hc]
 
 @[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)
 
-@[simp] lemma integral_comp_div' (c) :
+@[simp] lemma inv_smul_integral_comp_div (c) :
   c⁻¹ • ∫ x in a..b, f (x / c) = ∫ x in a/c..b/c, f x :=
 by by_cases hc : c = 0; simp [hc]
 
@@ -421,39 +421,39 @@ calc  ∫ x in a..b, f (x + 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]
 
-@[simp] lemma integral_comp_mul_add' (c d) :
+@[simp] lemma smul_integral_comp_mul_add (c d) :
   c • ∫ x in a..b, f (c * x + d) = ∫ x in c*a+d..c*b+d, f x :=
 by by_cases hc : c = 0; simp [hc]
 
 @[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
 
-@[simp] lemma integral_comp_add_mul' (c d) :
+@[simp] lemma smul_integral_comp_add_mul (c d) :
   c • ∫ x in a..b, f (d + c * x) = ∫ x in d+c*a..d+c*b, f x :=
 by by_cases hc : c = 0; simp [hc]
 
 @[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
 
-@[simp] lemma integral_comp_div_add' (c d) :
+@[simp] lemma inv_smul_integral_comp_div_add (c d) :
   c⁻¹ • ∫ x in a..b, f (x / c + d) = ∫ x in a/c+d..b/c+d, f x :=
 by by_cases hc : c = 0; simp [hc]
 
 @[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
 
-@[simp] lemma integral_comp_add_div' (c d) :
+@[simp] lemma inv_smul_integral_comp_add_div (c d) :
   c⁻¹ • ∫ x in a..b, f (d + x / c) = ∫ x in d+a/c..d+b/c, f x :=
 by by_cases hc : c = 0; simp [hc]
 
 @[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)
 
-@[simp] lemma integral_comp_mul_sub' (c d) :
+@[simp] lemma smul_integral_comp_mul_sub (c d) :
   c • ∫ x in a..b, f (c * x - d) = ∫ x in c*a-d..c*b-d, f x  :=
 by by_cases hc : c = 0; simp [hc]
 
@@ -465,23 +465,23 @@ begin
   simp only [inv_neg, smul_neg, neg_neg, neg_smul],
 end
 
-@[simp] lemma integral_comp_sub_mul' (c d) :
+@[simp] lemma smul_integral_comp_sub_mul (c d) :
   c • ∫ x in a..b, f (d - c * x) = ∫ x in d-c*b..d-c*a, f x  :=
 by by_cases hc : c = 0; simp [hc]
 
 @[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
 
-@[simp] lemma integral_comp_div_sub' (c d) :
+@[simp] lemma inv_smul_integral_comp_div_sub (c d) :
   c⁻¹ • ∫ x in a..b, f (x / c - d) = ∫ x in a/c-d..b/c-d, f x  :=
 by by_cases hc : c = 0; simp [hc]
 
 @[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
 
-@[simp] lemma integral_comp_sub_div' (c d) :
+@[simp] lemma inv_smul_integral_comp_sub_div (c d) :
   c⁻¹ • ∫ x in a..b, f (d - x / c) = ∫ x in d-b/c..d-a/c, f x :=
 by by_cases hc : c = 0; simp [hc]
 

test/integration.lean

@@ -46,8 +46,7 @@ example : ∫ x in 0..2, -exp (-x) = exp (-2) - 1 := by norm_num
 example : ∫ x in 1..2, exp (5*x - 5) = 1/5 * (exp 5 - 1) := by norm_num
 example : ∫ x in 0..π, cos (x/2) = 2 := by norm_num
 example : ∫ x in 0..π/4, sin (2*x) = 1/2 := by norm_num [mul_div_comm, mul_one_div]
-example (ω φ : ℝ) : ω * ∫ θ in 0..π, sin (ω*θ + φ) = cos φ - cos (ω*π + φ) :=
-  by { rw ← smul_eq_mul, simp }
+example (ω φ : ℝ) : ω * ∫ θ in 0..π, sin (ω*θ + φ) = cos φ - cos (ω*π + φ) := by simp
 
 /- some examples may require a bit of algebraic massaging -/
 example {L : ℝ} (h : L ≠ 0) : ∫ x in 0..2/L*π, sin (L/2 * x) = 4 / L :=