feat(measure_theory/interval_integral): integration by substitution /…

… change of variables (#7273)

Given that `f` has a derivative at `f'` everywhere on `interval a b`,
`∫ x in a..b, (g ∘ f) x * f' x = ∫ x in f a..f b, g x`.

Co-authored by @ADedecker

src/measure_theory/interval_integral.lean

@@ -73,6 +73,23 @@ an `FTC_filter` pair of filters around `b`. If `f` has finite limits `ca` and `c
   o(∥∫ x in ua..va, (1:ℝ) ∂μ∥ + ∥∫ x in ub..vb, (1:ℝ) ∂μ∥)` as `ua` and `va` tend to `la` while
 `ub` and `vb` tend to `lb`.
 
+### FTC-2 and corollaries
+
+We use FTC-1 to prove several versions of FTC-2 for the Lebesgue measure, using a similar naming
+scheme as for the versions of FTC-1. They include:
+* `interval_integral.integral_eq_sub_of_has_deriv_right_of_le` - most general version, for functions
+  with a right derivative
+* `interval_integral.integral_eq_sub_of_has_deriv_at'` - version for functions with a derivative on
+  an open set
+* `interval_integral.integral_deriv_eq_sub'` - version that is easiest to use when computing the
+  integral of a specific function
+
+We then derive additional integration techniques from FTC-2:
+* `interval_integral.integral_mul_deriv_eq_deriv_mul` - integration by parts
+* `interval_integral.integral_comp_mul_deriv'` - integration by substitution
+
+Many applications of these theorems can be found in the file `analysis.special_functions.integrals`.
+
 ## Implementation notes
 
 ### Avoiding `if`, `min`, and `max`
@@ -1479,7 +1496,8 @@ lemma deriv_within_integral_left
 /-!
 ### Fundamental theorem of calculus, part 2
 
-This section contains theorems pertaining to FTC-2 for interval integrals. -/
+This section contains theorems pertaining to FTC-2 for interval integrals.
+-/
 
 variable {f' : ℝ → E}
 
@@ -1623,4 +1641,32 @@ begin
   { exact (hcv.mul hcu').interval_integrable },
 end
 
+/-!
+### Integration by substitution / Change of variables
+-/
+
+theorem integral_comp_mul_deriv' {f f' g : ℝ → ℝ}
+  (hf : ∀ x ∈ interval a b, has_deriv_at f (f' x) x)
+  (hf' : continuous_on f' (interval a b))
+  (hg : ∀ x ∈ f '' (interval a b), continuous_at g x)
+  (hgm : ∀ x ∈ f '' (interval a b), measurable_at_filter g (𝓝 x)) :
+  -- TODO: prove that the integral of any integrable function is continuous and use here to remove
+  -- assumption `hgm`
+  ∫ x in a..b, (g ∘ f) x * f' x = ∫ x in f a..f b, g x :=
+let hg' := continuous_at.continuous_on hg in
+have h : ∀ x ∈ interval a b, has_deriv_at (λ u, ∫ t in f a..f u, g t) ((g ∘ f) x * f' x) x,
+{ intros x hx,
+  have hs := interval_subset_interval_left hx,
+  exact (integral_has_deriv_at_right (hg'.mono $ trans (intermediate_value_interval $
+    has_deriv_at.continuous_on $ λ y hy, hf y $ hs hy) $ image_subset f hs).interval_integrable
+      (hgm (f x) ⟨x, hx, rfl⟩) $ hg (f x) ⟨x, hx, rfl⟩).comp _ (hf x hx) },
+by simp_rw [integral_eq_sub_of_has_deriv_at h $ (hg'.comp (has_deriv_at.continuous_on hf) $
+  subset_preimage_image f _).mul hf', integral_same, sub_zero]
+
+theorem integral_comp_mul_deriv {f f' g : ℝ → ℝ}
+  (h : ∀ x ∈ interval a b, has_deriv_at f (f' x) x)
+  (h' : continuous_on f' (interval a b)) (hg : continuous g) :
+  ∫ x in a..b, (g ∘ f) x * f' x = ∫ x in f a..f b, g x :=
+integral_comp_mul_deriv' h h' (λ x h, hg.continuous_at) (λ x h, hg.measurable.measurable_at_filter)
+
 end interval_integral

test/integration.lean

@@ -67,3 +67,24 @@ example : ∫ x : ℝ in 0..2, 3 * (x + 1) ^ 2 = 26 :=
   by norm_num [integral_comp_add_right (λ x, x ^ 2)]
 example : ∫ x : ℝ in -1..0, (1 + (x + 1) ^ 2)⁻¹ = π/4 :=
   by simp [integral_comp_add_right (λ x, (1 + x ^ 2)⁻¹)]
+
+/-! ### Compositions of functions (aka "change of variables" or "integration by substitution") -/
+
+/- `interval_integral.integral_comp_mul_deriv` can be used to simplify integrals of the form
+  `∫ x in a..b, (g ∘ f) x * f' x`, where `f'` is the derivative of `f`, to `∫ x in f a..f b, g x` -/
+example {a b : ℝ} : ∫ x in a..b, exp (exp x) * exp x = ∫ x in exp a..exp b, exp x :=
+integral_comp_mul_deriv (λ x hx, has_deriv_at_exp x) continuous_on_exp continuous_exp
+
+/- if it is known (to mathlib), the integral of `g` can then be evaluated using `simp`/`norm_num` -/
+example : ∫ x in 0..1, exp (exp x) * exp x = exp (exp 1) - exp 1 :=
+by rw integral_comp_mul_deriv (λ x hx, has_deriv_at_exp x) continuous_on_exp continuous_exp; simp
+
+/- a more detailed example -/
+example : ∫ x in 0..2, exp (x ^ 2) * (2 * x) = exp 4 - 1 :=
+begin                                                    -- let g := exp x, f := x ^ 2, f' := 2 * x
+  rw integral_comp_mul_deriv (λ x hx, _),                -- simplify to ∫ x in f 0..f 2, g x
+  { norm_num },                                          -- compute the integral
+  { exact continuous_on_const.mul continuous_on_id },    -- show that f' is continuous on [0, 2]
+  { exact continuous_exp },                              -- show that g is continuous
+  { simpa using has_deriv_at_pow 2 x },                  -- show that f' = derivative of f on [0, 2]
+end