Theorem 6.4 — refinement moves the sums together

Proved

Rudin.ch06_refinement

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

analysisintegration

If $P'$ is a refinement of $P$ then $L(P,f,\alpha) \le L(P',f,\alpha)$ and $U(P',f,\alpha) \le U(P,f,\alpha)$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch06_stieltjes

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 6.4: refining a partition increases the lower sum and decreases the upper
sum. -/
theorem ch06_refinement (a b : ℝ) (hab : a ≤ b) (f α : ℝ → ℝ)
    (hα : MonotoneOn α (Set.Icc a b)) (hf : ∃ M, ∀ x ∈ Set.Icc a b, |f x| ≤ M)
    (P P' : Partition a b) (hrefine : Refines P' P) :
    lowerSum f α P ≤ lowerSum f α P' ∧ upperSum f α P' ≤ upperSum f α P := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 6, p. 122, Definition 6.3 and Theorem 6.4

Read-back

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

Let $a \le b$ be reals, $f, \alpha : \mathbb{R} \to \mathbb{R}$ with $\alpha$ monotone non-decreasing on $[a,b]$ and $f$ bounded on $[a,b]$ (there is a real $M$ with $|f(x)| \le M$ for all $x \in [a,b]$ ). Let $P$ and $P'$ be partitions of $[a,b]$ such that $P'$ refines $P$ , i.e. every division point of $P$ occurs as a division point of $P'$ . Then

L(P,f,\alpha) \;\le\; L(P',f,\alpha) \qquad\text{and}\qquad U(P',f,\alpha) \;\le\; U(P,f,\alpha),

where $U$ and $L$ are the upper and lower sums $\sum_i \bigl(\sup_{[x_i,x_{i+1}]} f\bigr)\Delta\alpha_i$ and $\sum_i \bigl(\inf_{[x_i,x_{i+1}]} f\bigr)\Delta\alpha_i$ over the subintervals of the respective partition (suprema and infima of real sets, returning $0$ on empty or unbounded sets).

Monotonicity of $\alpha$ is assumed only on $[a,b]$ , boundedness of $f$ only on $[a,b]$ ; nothing is assumed outside. The inequalities are non-strict.

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