Theorem 6.20 — the integral as an antiderivative

Proved

Rudin.ch06_integral_derivative

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

analysisintegration

Let $f \in \mathcal{R}$ on $[a,b]$ and put $F(x) = \int_a^x f(t)\,dt$ . Then $F$ is continuous on $[a,b]$ , and at every interior point $x_0$ where $f$ is continuous, $F$ is differentiable with $F'(x_0) = f(x_0)$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch06_stieltjes

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 6.20: if `f ∈ ℛ` on `[a, b]` and `F x = ∫ₐˣ f dt`, then `F` is continuous
on `[a, b]`; and if `f` is continuous at a point `x₀` of `[a, b]` then `F` is differentiable
at `x₀` with `F'(x₀) = f(x₀)`. -/
theorem ch06_integral_derivative (a b : ℝ) (hab : a ≤ b) (f : ℝ → ℝ)
    (hf : RiemannIntegrable a b f) (hfb : ∃ M, ∀ x ∈ Set.Icc a b, |f x| ≤ M) :
    ContinuousOn (fun x => RiemannIntegral a x f) (Set.Icc a b) ∧
    ∀ x₀ ∈ Set.Ioo a b, ContinuousAt f x₀ →
      HasDerivAt (fun x => RiemannIntegral a x f) (f x₀) x₀ := by sorry

end Rudin

Source

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

Read-back

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

Let $a \le b$ and let $f : \mathbb{R}\to\mathbb{R}$ be Riemann integrable on $[a,b]$ (upper integral $=$ lower integral with integrator the identity) and bounded on $[a,b]$ . Define $F(x) = \int_a^x f$ , the Riemann integral of $f$ over $[a,x]$ as defined in this bundle (the upper integral with integrator the identity; note that for $x < a$ no partition of $[a,x]$ exists, so the value there is whatever the convention yields). Then:

$F$ is continuous on $[a,b]$ (relative continuity at each point of the closed interval);
for every $x_0$ in the open interval $(a,b)$ : if $f$ is continuous at $x_0$ (as a function on all of $\mathbb{R}$ ), then $F$ is differentiable at $x_0$ with derivative exactly $f(x_0)$ .

Part 2 is an implication for each interior point; the endpoints are excluded, and one-sided derivatives there are not claimed. Integrability of $f$ on the subintervals $[a,x]$ is not assumed separately.

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