Prove2Me

Theorem 6.17, sharpened — upper and lower integrals against a density

Proved
Rudin.ch06_upper_lower_integral_density

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

analysisintegration

A sharpening of Rudin's Theorem 6.17, in which the conclusion is separated from any integrability assumption on the integrand.

Let α\alpha be monotonically increasing on [a,b][a,b] and differentiable at every point of [a,b][a,b], with derivative α′\alpha' bounded on [a,b][a,b] and Riemann integrable there, and let ff be bounded on [a,b][a,b]. Then the upper integrals of ff against dαd\alpha and of fα′f\alpha' against dxdx coincide, and so do the two lower integrals:

∫ab‾f dα=∫ab‾f(x)α′(x) dx,∫ab‾f dα=∫ab‾f(x)α′(x) dx.\overline{\int_a^b} f\,d\alpha = \overline{\int_a^b} f(x)\alpha'(x)\,dx, \qquad \underline{\int_a^b} f\,d\alpha = \underline{\int_a^b} f(x)\alpha'(x)\,dx.

Theorem 6.17 follows in one step: f∈R(α)f \in \mathcal{R}(\alpha) means that the two integrals on the left agree, fα′∈Rf\alpha' \in \mathcal{R} means that the two on the right agree, and the displayed identities make these conditions equivalent and identify the common values. Stating the identity at the level of upper and lower integrals is the more usable form, since it applies to an integrand that is not assumed integrable, exactly as the analogous sharpening of Theorem 6.12(c) does for additivity over adjacent intervals.

Formalization note. The boundedness of α′\alpha' is stated explicitly because in this development the upper and lower integrals are ordinary suprema and infima of sets of reals, which return a default value on unbounded sets; Rudin's class R\mathcal{R} consists of bounded functions by convention (Definitions 6.1 and 6.2).

Preamble
import Mathlib
import Definitions.Def_Rudin_ch06_stieltjes

open Filter Topology
Formal statement
namespace Rudin

/-- Rudin, Theorem 6.17, sharpened: for a monotonically increasing, differentiable `α` whose
derivative is bounded and Riemann-integrable on `[a, b]`, and a bounded `f`, the upper integral of
`f dα` equals the upper integral of `f α' dx`, and the lower integrals likewise agree; no
integrability of `f` is assumed. -/
theorem ch06_upper_lower_integral_density (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 α))
    (hα'b : ∃ K, ∀ x ∈ Set.Icc a b, |deriv α x| ≤ K)
    (hf : ∃ M, ∀ x ∈ Set.Icc a b, |f x| ≤ M) :
    upperIntegral a b f α = upperIntegral a b (fun x => f x * deriv α x) id ∧
    lowerIntegral a b f α = lowerIntegral a b (fun x => f x * deriv α x) id := by sorry

end Rudin
Source
Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 6, p. 131, Theorem 6.17 (sharpened to upper and lower integrals, with the standing boundedness hypotheses of Definitions 6.1-6.2 made explicit)

View graph