Theorem 6.8 — continuous functions are integrable

Proved

Rudin.ch06_continuous_integrable

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

analysisintegration

If $f$ is continuous on $[a,b]$ then $f \in \mathcal{R}(\alpha)$ for every monotonically increasing $\alpha$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch06_stieltjes

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 6.8: a continuous function on `[a, b]` is integrable with respect to every
monotonically increasing `α`. -/
theorem ch06_continuous_integrable (a b : ℝ) (hab : a ≤ b) (f α : ℝ → ℝ)
    (hα : MonotoneOn α (Set.Icc a b)) (hf : ContinuousOn f (Set.Icc a b)) :
    RSIntegrable a b f α := by sorry

end Rudin

Source

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

Read-back

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

Let $a \le b$ , let $\alpha : \mathbb{R} \to \mathbb{R}$ be monotone non-decreasing on $[a,b]$ , and let $f$ be continuous on $[a,b]$ (relative continuity at each point of the closed interval). Then $f$ is Riemann–Stieltjes integrable with respect to $\alpha$ on $[a,b]$ , i.e. the upper integral $\inf_P U(P,f,\alpha)$ and the lower integral $\sup_P L(P,f,\alpha)$ coincide.

No continuity or boundedness is assumed of $\alpha$ beyond monotonicity on $[a,b]$ , and boundedness of $f$ is not assumed separately. No value for the integral is asserted.

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