Theorem 11.17 — suprema and upper limits of measurable functions

Proved

Rudin.ch11_measurable_limits

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

analysismeasure-theory

If $f_1, f_2, \dots$ are measurable, then $\sup_n f_n$ and $\limsup_n f_n$ are measurable. As in Rudin the functions take values in the extended half-line, so both are always defined.

Preamble

import Mathlib
import Definitions.Def_Rudin_ch11_L2

open Filter Topology MeasureTheory
open scoped ENNReal

Formal statement

namespace Rudin

/-- Rudin, Theorem 11.17: the pointwise supremum and the upper limit of a sequence of measurable
functions are measurable.  As in Rudin the functions take values in the extended half-line, so
that the supremum and the upper limit are always defined. -/
theorem ch11_measurable_limits {X : Type*} [MeasurableSpace X] (f : ℕ → X → ℝ≥0∞)
    (hf : ∀ n, Measurable (f n)) :
    Measurable (fun x => ⨆ n, f n x) ∧
      Measurable (fun x => limsup (fun n => f n x) atTop) := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 11, p. 311, Theorem 11.17

Read-back

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

Let $X$ be a measurable space and let $f_0,f_1,\dots : X \to [0,\infty]$ be functions into the extended nonnegative reals, each measurable. Then both:

the pointwise supremum $x \mapsto \sup_n f_n(x)$ is measurable;
the pointwise upper limit $x \mapsto \limsup_{n\to\infty} f_n(x)$ is measurable.

Both suprema and upper limits are taken in $[0,\infty]$ , where they always exist, so no boundedness hypothesis is needed. No measure is involved — this is purely about measurability with respect to the $\sigma$ -algebra of $X$ and the Borel structure of $[0,\infty]$ .

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