Theorem 6.9 — monotone integrands

Proved

Rudin.ch06_monotone_integrable

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

analysisintegration

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

Preamble

import Mathlib
import Definitions.Def_Rudin_ch06_stieltjes

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 6.9: if `f` is monotone on `[a, b]` and the monotonically increasing
integrator `α` is continuous on `[a, b]`, then `f` is integrable with respect to `α`. -/
theorem ch06_monotone_integrable (a b : ℝ) (hab : a ≤ b) (f α : ℝ → ℝ)
    (hf : MonotoneOn f (Set.Icc a b)) (hα : MonotoneOn α (Set.Icc a b))
    (hαc : ContinuousOn α (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. 126, Theorem 6.9

Read-back

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

Let $a \le b$ and let $f, \alpha : \mathbb{R}\to\mathbb{R}$ satisfy: $f$ is monotone non-decreasing on $[a,b]$ ; $\alpha$ is monotone non-decreasing on $[a,b]$ ; and $\alpha$ is continuous on $[a,b]$ . Then $f$ is Riemann–Stieltjes integrable with respect to $\alpha$ on $[a,b]$ : its upper and lower integrals over that interval agree.

Note that only the non-decreasing case of monotonicity of $f$ is covered — a non-increasing $f$ is not addressed by this statement. No value for the integral is claimed.

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