theorem
Integration.fundamental_theorem_of_calculus
(f : ℝ → ℝ)
(a b : ℝ)
(hab : a ≤ b)
(hf : ContinuousOn f (Set.Icc a b))
:
Fundamental Theorem of Calculus. Let f ∈ C([a,b]). Then:
(1) (Evaluation form) For every differentiable F : ℝ → ℝ with F' = f on [a,b],
∫_a^b f = F(b) - F(a).
(2) (Antiderivative form) The function G(x) := ∫_a^x f is differentiable on [a,b]
with derivative G'(x) = f(x) at every point x ∈ [a,b].
theorem
Integration.integration_by_parts
(f g : ℝ → ℝ)
(a b : ℝ)
(hab : a ≤ b)
(hf : ContDiffOn ℝ 1 f (Set.Icc a b))
(hg : ContDiffOn ℝ 1 g (Set.Icc a b))
:
Integration by Parts. If f, g : ℝ → ℝ are continuously differentiable on [a,b]
(i.e. f, g ∈ C¹([a,b])), then
∫_a^b f'(x) g(x) dx = f(b) g(b) - f(a) g(a) - ∫_a^b f(x) g'(x) dx.
theorem
Integration.change_of_variables
(f φ : ℝ → ℝ)
(a b : ℝ)
(hab : a ≤ b)
(hφ : ContDiffOn ℝ 1 φ (Set.Icc a b))
(hφ_pos : ∀ x ∈ Set.Icc a b, 0 < deriv φ x)
(hf : ContinuousOn f (Set.Icc (φ a) (φ b)))
:
Change of Variables. Let φ : ℝ → ℝ be continuously differentiable on [a,b] with
φ' > 0 everywhere on [a,b], and let f be continuous on [φ(a), φ(b)]. Then
∫_{φ(a)}^{φ(b)} f(u) du = ∫_a^b f(φ(x)) · φ'(x) dx.