Theorem 6.5 — the lower integral is at most the upper integral

Proved

Rudin.ch06_lower_le_upper

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

analysisintegration

For a bounded $f$ and a monotonically increasing $\alpha$ on $[a,b]$ , $\underline{\int_a^b} f\,d\alpha \le \overline{\int_a^b} f\,d\alpha$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch06_stieltjes

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 6.5: for a bounded `f` and a monotonically increasing `α`, the lower
integral never exceeds the upper integral. -/
theorem ch06_lower_le_upper (a b : ℝ) (hab : a ≤ b) (f α : ℝ → ℝ)
    (hα : MonotoneOn α (Set.Icc a b)) (hf : ∃ M, ∀ x ∈ Set.Icc a b, |f x| ≤ M) :
    lowerIntegral a b f α ≤ upperIntegral a b f α := by sorry

end Rudin

Source

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

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]$ (some real $M$ with $|f(x)| \le M$ there). Then

\underline{\int_a^b} f\,d\alpha \;\le\; \overline{\int_a^b} f\,d\alpha ,

where the lower integral is the supremum of all lower sums over partitions of $[a,b]$ and the upper integral is the infimum of all upper sums, both computed as real suprema/infima with the convention that an empty or unbounded set of values yields $0$ .

The degenerate case $a = b$ is included by the hypothesis $a \le b$ ; there the only partitions have all division points equal to $a$ .

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