Theorem 6.21 — the fundamental theorem of calculus

Disproved

Rudin.ch06_fundamental_theorem

by Lucas · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisintegration

If $f \in \mathcal{R}$ on $[a,b]$ and there is a differentiable function $F$ on $[a,b]$ with $F' = f$ , then $\int_a^b f(x)\,dx = F(b) - F(a)$ . No continuity of $f$ is assumed: integrability plus the existence of an antiderivative suffices.

Preamble

import Mathlib
import Definitions.Def_Rudin_ch06_stieltjes

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 6.21 (the fundamental theorem of calculus): if `f ∈ ℛ` on `[a, b]` and there
is a differentiable function `F` on `[a, b]` with `F' = f`, then
`∫ₐᵇ f dx = F b - F a`. -/
theorem ch06_fundamental_theorem (a b : ℝ) (hab : a ≤ b) (f F : ℝ → ℝ)
    (hf : RiemannIntegrable a b f)
    (hF : ∀ x ∈ Set.Icc a b, HasDerivAt F (f x) x) :
    RiemannIntegral a b f = F b - F a := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 6, p. 134, Theorem 6.21

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Let $a \le b$ and let $f, F : \mathbb{R}\to\mathbb{R}$ satisfy:

$f$ is Riemann integrable on $[a,b]$ — its upper and lower integrals (with integrator the identity) over $[a,b]$ are equal;
at every point $x \in [a,b]$ , $F$ is differentiable with derivative exactly $f(x)$ , the differentiability being two-sided and required also at the endpoints $a$ and $b$ .

Then

\int_a^b f \;=\; F(b) - F(a),

where the left-hand side is the integral as defined in this bundle, namely the upper integral $\inf_P \sum_i \bigl(\sup_{[x_i,x_{i+1}]} f\bigr)(x_{i+1}-x_i)$ over partitions of $[a,b]$ — which equals the lower integral by the integrability hypothesis.

Continuity of $f$ is not assumed, and the degenerate case $a = b$ is included (both sides are then $0$ ).

Human review

Endorsed by Community (Bot) · Sep 14, 2026
Endorsed by Lucas · Sep 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph