Theorem 6.12(b,c,d) — monotonicity, additivity in the interval, and the basic bound

Disproved

Rudin.ch06_monotonicity_and_bounds

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

analysisintegration

For $f, g \in \mathcal{R}(\alpha)$ on $[a,b]$ : if $f \le g$ on $[a,b]$ then $\int f\,d\alpha \le \int g\,d\alpha$ ; for $c \in [a,b]$ , $f$ is integrable on $[a,c]$ and on $[c,b]$ and the two integrals add up to the integral over $[a,b]$ ; and if $|f| \le M$ then $\left|\int_a^b f\,d\alpha\right| \le M(\alpha(b) - \alpha(a))$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch06_stieltjes

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 6.12(b), (c), (d): the integral is monotone in the integrand, additive over
adjacent intervals, and bounded by `M (α b - α a)` when `|f| ≤ M`. -/
theorem ch06_monotonicity_and_bounds (a b : ℝ) (hab : a ≤ b) (f g α : ℝ → ℝ)
    (hα : MonotoneOn α (Set.Icc a b))
    (hf : RSIntegrable a b f α) (hg : RSIntegrable a b g α) :
    ((∀ x ∈ Set.Icc a b, f x ≤ g x) → RSIntegral a b f α ≤ RSIntegral a b g α) ∧
    (∀ c ∈ Set.Icc a b, RSIntegrable a c f α ∧ RSIntegrable c b f α ∧
      RSIntegral a c f α + RSIntegral c b f α = RSIntegral a b f α) ∧
    (∀ M : ℝ, (∀ x ∈ Set.Icc a b, |f x| ≤ M) →
      |RSIntegral a b f α| ≤ M * (α b - α a)) := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 6, p. 128, Theorem 6.12(b), (c), (d)

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$ and $g$ both be Riemann–Stieltjes integrable with respect to $\alpha$ on $[a,b]$ . Then three assertions hold together, where $\int$ denotes the upper integral (the definition of the integral in this bundle):

Monotonicity. If $f(x) \le g(x)$ for every $x \in [a,b]$ , then $\displaystyle\int_a^b f\,d\alpha \le \int_a^b g\,d\alpha$ .
Additivity over subintervals. For every $c \in [a,b]$ : $f$ is integrable with respect to $\alpha$ on $[a,c]$ , $f$ is integrable with respect to $\alpha$ on $[c,b]$ , and

\int_a^c f\,d\alpha + \int_c^b f\,d\alpha = \int_a^b f\,d\alpha .

Bound. For every real $M$ : if $|f(x)| \le M$ for all $x \in [a,b]$ , then

\Bigl| \int_a^b f\,d\alpha \Bigr| \;\le\; M\bigl(\alpha(b) - \alpha(a)\bigr).

In item 3 the bound $M$ is universally quantified and the hypothesis is on $[a,b]$ only. No separate boundedness hypothesis on $f$ or $g$ is imposed in the premises of the theorem itself.

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