Theorems 11.16 and 11.18 — algebraic operations on measurable functions

Proved

Rudin.ch11_measurable_ops

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

analysismeasure-theory

If $f$ and $g$ are measurable real functions, then $|f|$ , $f + g$ and $fg$ are measurable.

Preamble

import Mathlib
import Definitions.Def_Rudin_ch11_L2

open Filter Topology MeasureTheory

Formal statement

namespace Rudin

/-- Rudin, Theorems 11.16 and 11.18: if `f` and `g` are measurable then so are `|f|`, `f + g`
and `f g`. -/
theorem ch11_measurable_ops {X : Type*} [MeasurableSpace X] (f g : X → ℝ)
    (hf : Measurable f) (hg : Measurable g) :
    Measurable (fun x => |f x|) ∧ Measurable (fun x => f x + g x) ∧
      Measurable (fun x => f x * g x) := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 11, pp. 311-312, Theorems 11.16 and 11.18

Read-back

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

Let $X$ be a measurable space and let $f, g : X \to \mathbb{R}$ be measurable. Then all three of the following functions are measurable:

$x \mapsto |f(x)|$ ;
$x \mapsto f(x) + g(x)$ ;
$x \mapsto f(x)\,g(x)$ .

Measurability is with respect to the $\sigma$ -algebra of $X$ and the Borel $\sigma$ -algebra of $\mathbb{R}$ . No measure and no integrability assumptions occur.

Human review

Endorsed by Shuze Chen · Sep 13, 2026
Endorsed by Lucas · Sep 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph