feat(analysis/special_functions/integrals): integrating linear combinations of functions (#6597)

Together with #6357, this PR makes it possible to compute integrals of the form `∫ x in a..b, c * f x + d * g x` by `simp` (where `c` and `d` are constants and `f` and `g` are functions that are `interval_integrable` on `interval a b`.

Notably, this allows us to compute the integrals of polynomials by `norm_num`. Here's an example, followed by an example of a more random linear combination of `interval_integrable` functions:
```
import analysis.special_functions.integrals
open interval_integral real
open_locale real

example : ∫ x:ℝ in 0..2, 6*x^5 + 3*x^4 + x^3 - 2*x^2 + x - 7 = 1048 / 15 := by norm_num

example : ∫ x:ℝ in 0..1, exp x + 9 * x^8 + x^3 - x/2 + (1 + x^2)⁻¹ = exp 1 + π/4 := by norm_num
```

Author: benjamindavidson

src/analysis/special_functions/integrals.lean

@@ -11,17 +11,17 @@ import measure_theory.interval_integral
 This file contains proofs of the integrals of various simple functions, including `pow`, `exp`,
 `inv`/`one_div`, `sin`, `cos`, and `λ x, 1 / (1 + x^2)`.
 
-With these lemmas, many simple integrals can be computed by `simp` or `norm_num`. Scroll to the
-bottom of the file for examples.
+With these lemmas, many simple integrals can be computed by `simp` or `norm_num`.
 
-This file is incomplete; we are working on expanding it.
+This file is still being developed.
 -/
 
 open real set interval_integral
 variables {a b : ℝ}
 
 namespace interval_integral
-variable {f : ℝ → ℝ}
+open measure_theory
+variables {f : ℝ → ℝ} {μ ν : measure ℝ} [locally_finite_measure μ]
 
 @[simp]
 lemma integral_const_mul (c : ℝ) : ∫ x in a..b, c * f x = c * ∫ x in a..b, f x :=
@@ -35,6 +35,67 @@ by simp only [mul_comm, integral_const_mul]
 lemma integral_div (c : ℝ) : ∫ x in a..b, f x / c = (∫ x in a..b, f x) / c :=
 integral_mul_const c⁻¹
 
+@[simp]
+lemma interval_integrable_pow (n : ℕ) : interval_integrable (λ x, x^n) μ a b :=
+(continuous_pow n).interval_integrable a b
+
+@[simp]
+lemma interval_integrable_id : interval_integrable (λ x, x) μ a b :=
+continuous_id.interval_integrable a b
+
+@[simp]
+lemma interval_integrable_const (c : ℝ) : interval_integrable (λ x, c) μ a b :=
+continuous_const.interval_integrable a b
+
+@[simp]
+lemma interval_integrable.const_mul (c : ℝ) (h : interval_integrable f ν a b) :
+  interval_integrable (λ x, c * f x) ν a b :=
+by convert h.smul c
+
+@[simp]
+lemma interval_integrable.mul_const (c : ℝ) (h : interval_integrable f ν a b) :
+  interval_integrable (λ x, f x * c) ν a b :=
+by simp only [mul_comm, interval_integrable.const_mul c h]
+
+@[simp]
+lemma interval_integrable.div (c : ℝ) (h : interval_integrable f ν a b) :
+  interval_integrable (λ x, f x / c) ν a b :=
+interval_integrable.mul_const c⁻¹ h
+
+lemma interval_integrable_one_div (h : ∀ x : ℝ, x ∈ interval a b → f x ≠ 0)
+  (hf : continuous_on f (interval a b)) :
+  interval_integrable (λ x, 1 / f x) μ a b :=
+(continuous_on_const.div hf h).interval_integrable
+
+@[simp]
+lemma interval_integrable_inv (h : ∀ x : ℝ, x ∈ interval a b → f x ≠ 0)
+  (hf : continuous_on f (interval a b)) :
+  interval_integrable (λ x, (f x)⁻¹) μ a b :=
+by simpa only [one_div] using interval_integrable_one_div h hf
+
+@[simp]
+lemma interval_integrable_exp : interval_integrable exp μ a b :=
+continuous_exp.interval_integrable a b
+
+@[simp]
+lemma interval_integrable_sin : interval_integrable sin μ a b :=
+continuous_sin.interval_integrable a b
+
+@[simp]
+lemma interval_integrable_cos : interval_integrable cos μ a b :=
+continuous_cos.interval_integrable a b
+
+lemma interval_integrable_one_div_one_add_sq : interval_integrable (λ x:ℝ, 1 / (1 + x^2)) μ a b :=
+begin
+  refine (continuous_const.div _ (λ x, _)).interval_integrable a b,
+  { continuity },
+  { nlinarith },
+end
+
+@[simp]
+lemma interval_integrable_inv_one_add_sq : interval_integrable (λ x:ℝ, (1 + x^2)⁻¹) μ a b :=
+by simpa only [one_div] using interval_integrable_one_div_one_add_sq
+
 end interval_integral
 
 @[simp]
@@ -98,8 +159,9 @@ by rw integral_deriv_eq_sub'; norm_num [continuous_on_cos]
 lemma integral_inv_one_add_sq : ∫ x : ℝ in a..b, (1 + x^2)⁻¹ = arctan b - arctan a :=
 begin
   simp only [← one_div],
-  refine integral_deriv_eq_sub' _ _ _ (continuous_const.div _ (λ x, _)).continuous_on;
-  norm_num,
+  refine integral_deriv_eq_sub' _ _ _ (continuous_const.div _ (λ x, _)).continuous_on,
+  { norm_num },
+  { norm_num },
   { continuity },
   { nlinarith },
 end

src/measure_theory/interval_integral.lean

@@ -186,12 +186,12 @@ lemma smul [normed_field 𝕜] [normed_space 𝕜 E] {f : α → E} {a b : α} {
   interval_integrable (r • f) μ a b :=
 ⟨h.1.smul r, h.2.smul r⟩
 
-lemma add [second_countable_topology E] (hf : interval_integrable f μ a b)
-  (hg : interval_integrable g μ a b) : interval_integrable (f + g) μ a b :=
+@[simp] lemma add [second_countable_topology E] (hf : interval_integrable f μ a b)
+  (hg : interval_integrable g μ a b) : interval_integrable (λ x, f x + g x) μ a b :=
 ⟨hf.1.add hg.1, hf.2.add hg.2⟩
 
-lemma sub [second_countable_topology E] (hf : interval_integrable f μ a b)
-  (hg : interval_integrable g μ a b) : interval_integrable (f - g) μ a b :=
+@[simp] lemma sub [second_countable_topology E] (hf : interval_integrable f μ a b)
+  (hg : interval_integrable g μ a b) : interval_integrable (λ x, f x - g x) μ a b :=
 ⟨hf.1.sub hg.1, hf.2.sub hg.2⟩
 
 end interval_integrable
@@ -339,14 +339,14 @@ lemma norm_integral_le_of_norm_le_const {a b C : ℝ} {f : ℝ → E}
   ∥∫ x in a..b, f x∥ ≤ C * abs (b - a) :=
 norm_integral_le_of_norm_le_const_ae $ eventually_of_forall h
 
-lemma integral_add (hf : interval_integrable f μ a b) (hg : interval_integrable g μ a b) :
+@[simp] lemma integral_add (hf : interval_integrable f μ a b) (hg : interval_integrable g μ a b) :
   ∫ x in a..b, f x + g x ∂μ = ∫ x in a..b, f x ∂μ + ∫ x in a..b, g x ∂μ :=
 by { simp only [interval_integral, integral_add hf.1 hg.1, integral_add hf.2 hg.2], abel }
 
 @[simp] lemma integral_neg : ∫ x in a..b, -f x ∂μ = -∫ x in a..b, f x ∂μ :=
 by { simp only [interval_integral, integral_neg], abel }
 
-lemma integral_sub (hf : interval_integrable f μ a b) (hg : interval_integrable g μ a b) :
+@[simp] lemma integral_sub (hf : interval_integrable f μ a b) (hg : interval_integrable g μ a b) :
   ∫ 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)