Theorem 6.12(a) — linearity of the integral

Proved

Rudin.ch06_linearity

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

analysisintegration

If $f, g \in \mathcal{R}(\alpha)$ and $c$ is a constant, then $f + g \in \mathcal{R}(\alpha)$ with $\int (f+g)\,d\alpha = \int f\,d\alpha + \int g\,d\alpha$ , and $cf \in \mathcal{R}(\alpha)$ with $\int cf\,d\alpha = c\int f\,d\alpha$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch06_stieltjes

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 6.12(a): the integrable functions form a vector space and the integral is
linear on it. -/
theorem ch06_linearity (a b : ℝ) (hab : a ≤ b) (f g α : ℝ → ℝ) (c : ℝ)
    (hα : MonotoneOn α (Set.Icc a b))
    (hf : RSIntegrable a b f α) (hg : RSIntegrable a b g α)
    (hfb : ∃ M, ∀ x ∈ Set.Icc a b, |f x| ≤ M) (hgb : ∃ M, ∀ x ∈ Set.Icc a b, |g x| ≤ M) :
    RSIntegrable a b (fun x => f x + g x) α ∧
    RSIntegral a b (fun x => f x + g x) α = RSIntegral a b f α + RSIntegral a b g α ∧
    RSIntegrable a b (fun x => c * f x) α ∧
    RSIntegral a b (fun x => c * f x) α = c * RSIntegral a b f α := by sorry

end Rudin

Source

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

Read-back

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

Let $a \le b$ , let $f, g, \alpha : \mathbb{R}\to\mathbb{R}$ and let $c \in \mathbb{R}$ . Assume $\alpha$ is monotone non-decreasing on $[a,b]$ ; $f$ and $g$ are each Riemann–Stieltjes integrable with respect to $\alpha$ on $[a,b]$ (their upper and lower integrals coincide); and each of $f$ , $g$ is bounded on $[a,b]$ (each with its own bound). Then all four of the following hold:

$f+g$ is integrable with respect to $\alpha$ on $[a,b]$ ;
$\displaystyle \int_a^b (f+g)\,d\alpha = \int_a^b f\,d\alpha + \int_a^b g\,d\alpha$ ;
$c\,f$ is integrable with respect to $\alpha$ on $[a,b]$ ;
$\displaystyle \int_a^b c f\,d\alpha = c \int_a^b f\,d\alpha$ .

Here every occurrence of $\int_a^b \cdot\, d\alpha$ denotes the upper integral of the function in question (the definition used throughout this bundle), which for integrable functions is the common value of the upper and lower integrals. The scalar $c$ is an arbitrary real, positive, negative or zero.

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