Theorem 6.17 — reduction to a Riemann integral

Disproved

Rudin.ch06_reduction_to_riemann

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

analysisintegration

Let $\alpha$ increase monotonically on $[a,b]$ , be differentiable there with $\alpha' \in \mathcal{R}$ , and let $f$ be bounded. Then $f \in \mathcal{R}(\alpha)$ if and only if $f\alpha' \in \mathcal{R}$ , and in that case $\int_a^b f\,d\alpha = \int_a^b f(x)\alpha'(x)\,dx$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch06_stieltjes

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 6.17: let `α` increase monotonically with `α'` Riemann-integrable on
`[a, b]`, and let `f` be bounded.  Then `f ∈ ℛ(α)` if and only if `f α' ∈ ℛ`, and in that
case `∫ f dα = ∫ f α' dx`. -/
theorem ch06_reduction_to_riemann (a b : ℝ) (hab : a ≤ b) (f α : ℝ → ℝ)
    (hα : MonotoneOn α (Set.Icc a b))
    (hαd : ∀ x ∈ Set.Icc a b, HasDerivAt α (deriv α x) x)
    (hα' : RiemannIntegrable a b (deriv α))
    (hf : ∃ M, ∀ x ∈ Set.Icc a b, |f x| ≤ M) :
    (RSIntegrable a b f α ↔ RiemannIntegrable a b (fun x => f x * deriv α x)) ∧
    (RSIntegrable a b f α →
      RSIntegral a b f α = RiemannIntegral a b (fun x => f x * deriv α x)) := by sorry

end Rudin

Source

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

Read-back

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

Let $a \le b$ and $f, \alpha : \mathbb{R} \to \mathbb{R}$ . Assume:

$\alpha$ is monotone non-decreasing on $[a,b]$ ;
at every $x \in [a,b]$ , $\alpha$ is differentiable with derivative equal to the value $\alpha'(x)$ of the total derivative operator (so $\alpha'$ is the genuine derivative on the whole closed interval);
$\alpha'$ is Riemann integrable on $[a,b]$ in the sense of this bundle (upper integral $=$ lower integral with integrator the identity);
$f$ is bounded on $[a,b]$ .

Then both:

$f$ is Riemann–Stieltjes integrable with respect to $\alpha$ on $[a,b]$ if and only if the product $x \mapsto f(x)\,\alpha'(x)$ is Riemann integrable on $[a,b]$ ;
if $f$ is Riemann–Stieltjes integrable with respect to $\alpha$ , then

\int_a^b f\,d\alpha \;=\; \int_a^b f(x)\,\alpha'(x)\,dx ,

both sides being the corresponding upper integrals.

The equality in 2 is asserted only under the integrability hypothesis stated there.

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