Theorem 6.6 — the $\varepsilon$ criterion for integrability

Proved

Rudin.ch06_riemann_criterion

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

analysisintegration

A bounded $f$ satisfies $f \in \mathcal{R}(\alpha)$ on $[a,b]$ if and only if for every $\varepsilon > 0$ there is a partition $P$ with $U(P,f,\alpha) - L(P,f,\alpha) < \varepsilon$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch06_stieltjes

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 6.6: a bounded `f` is integrable with respect to a monotonically increasing
`α` on `[a, b]` if and only if for every `ε > 0` there is a partition `P` with
`U(P, f, α) - L(P, f, α) < ε`. -/
theorem ch06_riemann_criterion (a b : ℝ) (hab : a ≤ b) (f α : ℝ → ℝ)
    (hα : MonotoneOn α (Set.Icc a b)) (hf : ∃ M, ∀ x ∈ Set.Icc a b, |f x| ≤ M) :
    RSIntegrable a b f α ↔
      ∀ ε : ℝ, 0 < ε → ∃ P : Partition a b, upperSum f α P - lowerSum f α P < ε := by sorry

end Rudin

Source

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

Read-back

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

Let $a \le b$ , let $\alpha$ be monotone non-decreasing on $[a,b]$ and let $f$ be bounded on $[a,b]$ . Then the following are equivalent:

the upper and lower integrals of $f$ against $\alpha$ over $[a,b]$ are equal (this is what integrability means here);
for every real $\varepsilon > 0$ there exists a partition $P$ of $[a,b]$ with

U(P,f,\alpha) - L(P,f,\alpha) < \varepsilon .

The difference is required to be strictly less than $\varepsilon$ , and the partition may depend on $\varepsilon$ . Both directions are 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

Theorem 6.6 — the ε\varepsilonε criterion for integrability

Theorem 6.6 — the $\varepsilon$ criterion for integrability