theorem intervalIntegral_deriv_eq_sub {a b : ℝ} {F f : ℝ → ℝ} (hab : a ≤ b) (hcont : ContinuousOn F (Set.Icc a b)) (hderiv : ∀ x ∈ Set.Ioo a b, HasDerivAt F (f x) x) (hinteg : IntervalIntegrable f MeasureTheory.volume a b) : ∫ (x : ℝ) in a..b, f x = F b - F a

Theorem 5.3.1 (Fundamental theorem of calculus, first form). If F is continuous on [a, b], differentiable on (a, b) with derivative f, and f is Riemann integrable on [a, b], then ∫_{a}^{b} f = F b - F a.

theorem integral_square_unit_interval : ∫ (x : ℝ) in 0..1, x ^ 2 = 1 / 3

Example 5.3.2: By the fundamental theorem of calculus, ∫_0^1 x^2 \\, dx = 1 / 3 using the antiderivative x ↦ x^3 / 3.

theorem fundamental_theorem_of_calculus_second {a b : ℝ} {f : ℝ → ℝ} (hinteg : IntervalIntegrable f MeasureTheory.volume a b) : ContinuousOn (fun (x : ℝ) => ∫ (t : ℝ) in a..x, f t) (Set.Icc a b) ∧ ∀ {c : ℝ}, c ∈ Set.Ioo a b → ContinuousAt f c → HasDerivAt (fun (x : ℝ) => ∫ (t : ℝ) in a..x, f t) (f c) c

Theorem 5.3.3 (Fundamental theorem of calculus, second form). If f is Riemann integrable on [a, b] and F x = ∫_{a}^{x} f, then F is continuous on [a, b], and whenever f is continuous at c ∈ (a, b) the function F is differentiable at c with derivative F' c = f c.

theorem intervalIntegral_change_of_variables {a b c d : ℝ} {f g : ℝ → ℝ} (hab : a ≤ b) (hg_diff : ContDiffOn ℝ 1 g (Set.Icc a b)) (hf_cont : ContinuousOn f (Set.Icc c d)) (hg_maps : Set.MapsTo g (Set.Icc a b) (Set.Icc c d)) : ∫ (x : ℝ) in a..b, f (g x) * deriv g x = ∫ (s : ℝ) in g a..g b, f s

Theorem 5.3.5 (Change of variables). If g : [a,b] → ℝ is continuously differentiable and maps [a,b] into [c,d], and f : [c,d] → ℝ is continuous, then ∫_{a}^{b} f (g x) * g' x = ∫_{g a}^{g b} f.

theorem integral_mul_cos_square_root_pi : ∫ (x : ℝ) in 0..√Real.pi, x * Real.cos (x ^ 2) = 0

Example 5.3.6: Using the substitution g(x) = x^2 and that the derivative of sin is cos, ∫_0^{√π} x * cos (x^2) = 0.

theorem not_integrable_log_abs_div_x_on_neg_one_one : ¬MeasureTheory.IntegrableOn (fun (x : ℝ) => Real.log |x| / x) (Set.Icc (-1) 1) MeasureTheory.volume

Example 5.3.7: The naive substitution g x = log |x| for ∫_{-1}^{1} (log |x|) / x fails because the integrand is unbounded and not continuous at 0, so the integral over [-1,1] is not well-defined as a Riemann (Lebesgue) integral.