Measure theory and integration

The Riemann integral is built for continuous functions on intervals, and it behaves badly under limits. Enumerate the rationals of $[0, 1]$ as $q_1, q_2, \dots$ and let $f_n$ be the indicator of $\{q_1, \dots, q_n\}$. Each $f_n$ is Riemann integrable with integral $0$, the sequence increases, and its pointwise limit is the Dirichlet function $\mathbf 1_{\Q \cap [0, 1]}$, whose upper Riemann sums are all $1$ and lower sums all $0$. A monotone limit of integrable functions with integrals $0$ has no Riemann integral.

This is not a curiosity. Fourier series, solutions of differential equations and probability all produce functions as limits, and analysis needs a space of integrable functions that is complete: Cauchy sequences should converge to something integrable. Henri Lebesgue's thesis (1902) supplied it. His idea, in his own later image, is the shopkeeper's: to count the takings, do not add coins in the order they arrived (the Riemann sum over the domain); sort them by value and multiply each value by how many coins have it. For a function, that means slicing the range and asking for the size of each set $\{x : f(x) > t\}$. That requires a notion of size — a measure — for sets far wilder than intervals.

For a hump-shaped function the two pictures give the same number. They part ways for wild functions. For the Dirichlet function, the vertical strips never settle down, but the horizontal picture is easy: the set where $\mathbf 1_\Q > t$ is $\Q \cap [0, 1]$ for $0 \le t < 1$, a countable set, and a countable set ought to have size $0$. So the Lebesgue integral of the Dirichlet function is $0$.

Three questions organise the subject. Which sets get a size? Not all of them: Vitali's construction below produces a subset of $\R$ that cannot be given any translation-invariant, countably additive length. How do we build the size function? By approximating from outside with countably many intervals (outer measure) and keeping the sets that split every other set additively (Carathéodory). What do we gain? Countable additivity of the measure becomes, for integrals, the convergence theorems: under monotonicity or domination, $\lim \int f_n = \int \lim f_n$.

From countable additivity: $\mu$ is monotone, countably subadditive ($\mu(\bigcup E_j) \le \sum \mu(E_j)$ for any $E_j$), continuous from below ($E_1 \subseteq E_2 \subseteq \cdots$ implies $\mu(\bigcup E_n) = \lim \mu(E_n)$), and continuous from above when $\mu(E_1) < \infty$. The Borel σ-algebra $\mathcal B(X)$ of a topological space is the smallest σ-algebra containing the open sets. A property holds almost everywhere (a.e.) if it fails only on a set of measure $0$, a null set.

Every measurable $f \ge 0$ is the increasing limit of the simple functions

which round $f$ down to the dyadic grid of mesh $2^{-n}$ and cap it at $n$. This is the "slice the range" picture made precise.

Hölder's inequality $\int |fg| \le \|f\|_p \|g\|_q$ for $1/p + 1/q = 1$, and Minkowski's inequality $\|f + g\|_p \le \|f\|_p + \|g\|_p$, follow from Young's inequality $ab \le a^p/p + b^q/q$ (Folland, §6.1); Minkowski makes $\|\cdot\|_p$ a norm on $L^p$.

The same recipe — a premeasure on an algebra of simple sets, extended by outer measure and Carathéodory — builds Lebesgue measure on $\R^n$ (from boxes), Lebesgue–Stieltjes measures $\mu((a, b]) = F(b) - F(a)$ for increasing right-continuous $F$ (the distributions of probability), product measures, and Hausdorff measures. Lebesgue measure is translation invariant, and up to a constant factor it is the only translation-invariant measure on $\mathcal B(\R)$ that is finite on bounded sets.

Throughout, $(X, \mathcal M, \mu)$ is a measure space. Two facts follow at once from the definitions: the integral is monotone ($0 \le f \le g$ implies $\int f \le \int g$), and for a simple $\varphi \ge 0$ the map $A \mapsto \int_A \varphi \, d\mu = \sum_i c_i \mu(A \cap E_i)$ is a measure on $\mathcal M$, hence continuous from below.

Applied to the partial sums, monotone convergence gives $\int \sum_n g_n = \sum_n \int g_n$ for measurable $g_n \ge 0$ — termwise integration of non-negative series with no further hypothesis. With the dyadic approximations $\varphi_n \uparrow f$ it also shows that the integral is additive, $\int (f + g) = \int f + \int g$, because it is additive on simple functions.

In the examples above no integrable $g$ dominates, and the conclusion fails. Dominated convergence also justifies differentiation under the integral sign: if $\partial_t F(x, t)$ exists and $|\partial_t F(x, t)| \le g(x)$ with $g$ integrable, then $\frac{d}{dt} \int F(x, t) \, dx = \int \partial_t F(x, t) \, dx$ (apply dominated convergence to difference quotients, bounded by $g$ via the mean value theorem).

About the proof. The product measure comes from the premeasure on finite unions of rectangles via Carathéodory. One proves the formula for indicators of rectangles, extends it to all of $\mathcal M \otimes \mathcal N$ with the monotone class lemma (this is where σ-finiteness enters, through continuity from above), then to simple functions by linearity, to non-negative functions by monotone convergence, and to integrable functions by splitting $f = f^+ - f^-$. Details: Folland, §2.5, or Stein–Shakarchi, Ch. 2 §3. In practice one uses Tonelli on $|f|$ to check integrability and then Fubini to compute.

Both hypotheses are needed:

• Integrability. On $\N \times \N$ with counting measure let $a_{m,n} = 1$ if $m = n$, $a_{m,n} = -1$ if $m = n + 1$, and $0$ otherwise. Every column sums to $0$ and every row except the first sums to $0$, so $\sum_n \sum_m a_{m,n} = 0$ while $\sum_m \sum_n a_{m,n} = 1$. Here $\sum |a_{m,n}| = \infty$. (A continuous version: $(x^2 - y^2)/(x^2 + y^2)^2$ on $(0, 1)^2$ has iterated integrals $\pm \pi/4$.)
• σ-finiteness. Let $\mu$ be Lebesgue measure and $\nu$ counting measure on $[0, 1]$, and $f = \mathbf 1_{\{x = y\}}$. Then $\int \!\! \int f \, d\nu \, d\mu = \int 1 \, d\mu = 1$ but $\int \!\! \int f \, d\mu \, d\nu = \int 0 \, d\nu = 0$.

The subsequence cannot be avoided. The typewriter sequence — indicators of $[0, 1]$, then $[0, \tfrac12], [\tfrac12, 1]$, then the four quarters, and so on — tends to $0$ in $L^1$ (the integrals are the interval lengths), but at every $x \in [0, 1]$ it takes the value $1$ infinitely often. When $p = 2$, $L^2(\mu)$ is a Hilbert space with $\langle f, g \rangle = \int f \bar g \, d\mu$; it is the stage for Fourier analysis and quantum mechanics.

Lebesgue's criterion sharpens this: a bounded function on $[a, b]$ is Riemann integrable exactly when its set of discontinuities is null. Improper Riemann integrals are another matter: $\int_0^\infty \frac{\sin x}{x} \, dx = \frac\pi2$ exists as an improper Riemann integral, but $\frac{\sin x}{x} \notin \mathcal L^1(0, \infty)$ because $\int_0^\infty \frac{|\sin x|}{x} \, dx = \infty$. The Lebesgue integral is an absolute integral.

Mathlib's measure theory is one of its largest and most used libraries: probability theory, the Fourier transform and the integration on manifolds are all built on it. Its volume on ℝ is Lebesgue measure, constructed from outer measure with Carathéodory's criterion via Stieltjes functions, exactly as above. It extends length:

/-- Lebesgue measure extends length: `λ([a, b]) = b − a` (as an extended non-negative real;
`ENNReal.ofReal` sends negative numbers to `0`, so the formula also covers `b < a`). Mathlib
constructs `volume` on `ℝ` by Carathéodory's criterion and proves this as `Real.volume_Icc`. -/
theorem volume_Icc (a b : ℝ) : volume (Icc a b) = ENNReal.ofReal (b - a) :=
  Real.volume_Icc

The lesson's proof that $\Q$ is null — a countable union of null singletons — and Mathlib's general statement for countable sets:

/-- **The rationals form a Lebesgue-null set.** `ℚ ⊂ ℝ` is the countable union of the
singletons `{q}`, each of measure `0`; by countable subadditivity the union has measure `0`.
This is the lesson's proof, using Mathlib's `measure_iUnion_null` (a countable union of null
sets is null) and `Real.volume_singleton`. -/
theorem volume_rat_eq_zero : volume (range ((↑) : ℚ → ℝ)) = 0 := by
  rw [← iUnion_singleton_eq_range]
  exact measure_iUnion_null fun q => Real.volume_singleton

/-- More generally, every countable subset of `ℝ` is Lebesgue-null (`Set.Countable.measure_zero`;
the hypothesis Mathlib needs is that singletons are null). The converse is false: the Cantor
set is uncountable and null. -/
theorem countable_null {s : Set ℝ} (hs : s.Countable) : volume s = 0 :=
  hs.measure_zero volume

Mathlib writes ∫⁻ x, f x ∂μ for the integral of a function into $[0, \infty]$ (the "lintegral", defined as the supremum over simple functions below $f$) and ∫ x, f x ∂μ for the Bochner integral of integrable functions into a Banach space. Markov's inequality, proved here by comparing $f$ with the simple function $\varepsilon \mathbf 1_{\{f \ge \varepsilon\}}$ (the step used in the Riemann–Lebesgue comparison above):

/-- **Markov's inequality.** For a measurable `f : α → [0, ∞]` and `ε ∈ [0, ∞]`,
`ε · μ{f ≥ ε} ≤ ∫ f dμ`. Proof: the simple function `ε · 1_{f ≥ ε}` lies below `f`, and its
integral is `ε · μ{f ≥ ε}`; integrals are monotone. (Mathlib: `mul_meas_ge_le_lintegral`.) -/
theorem markov {α : Type*} [MeasurableSpace α] (μ : Measure α) {f : α → ℝ≥0∞}
    (hf : Measurable f) (ε : ℝ≥0∞) : ε * μ {x | ε ≤ f x} ≤ ∫⁻ x, f x ∂μ := by
  have hs : MeasurableSet {x | ε ≤ f x} := measurableSet_le measurable_const hf
  calc ε * μ {x | ε ≤ f x} = ∫⁻ x, {x | ε ≤ f x}.indicator (fun _ => ε) x ∂μ :=
        (lintegral_indicator_const hs ε).symm
    _ ≤ ∫⁻ x, f x ∂μ := by
        apply lintegral_mono
        intro x
        by_cases hx : ε ≤ f x
        · simpa [indicator_of_mem (show x ∈ {x | ε ≤ f x} from hx)] using hx
        · simp [indicator_of_notMem (show x ∉ {x | ε ≤ f x} from hx)]

The convergence theorems are library theorems. Note the different hypotheses: monotone convergence needs no integrability, dominated convergence needs one integrable bound for all $n$.

/-- **Monotone convergence theorem** (Beppo Levi). If `0 ≤ f₀ ≤ f₁ ≤ ⋯` are measurable, then
`∫ sup fₙ = sup ∫ fₙ`. No integrability hypothesis is needed for non-negative functions. This is
Mathlib's `lintegral_iSup`. -/
theorem monotone_convergence {α : Type*} [MeasurableSpace α] (μ : Measure α)
    {f : ℕ → α → ℝ≥0∞} (hf : ∀ n, Measurable (f n)) (hmono : Monotone f) :
    ∫⁻ x, ⨆ n, f n x ∂μ = ⨆ n, ∫⁻ x, f n x ∂μ :=
  lintegral_iSup hf hmono

/-- **Dominated convergence theorem** (Lebesgue). If `Fₙ → f` almost everywhere and
`‖Fₙ‖ ≤ g` almost everywhere for one integrable `g`, then `∫ Fₙ → ∫ f`. This is Mathlib's
`tendsto_integral_of_dominated_convergence`. -/
theorem dominated_convergence {α : Type*} [MeasurableSpace α] (μ : Measure α)
    {F : ℕ → α → ℝ} {f g : α → ℝ} (hF : ∀ n, AEStronglyMeasurable (F n) μ)
    (hg : Integrable g μ) (hbound : ∀ n, ∀ᵐ x ∂μ, ‖F n x‖ ≤ g x)
    (hlim : ∀ᵐ x ∂μ, Tendsto (fun n => F n x) atTop (𝓝 (f x))) :
    Tendsto (fun n => ∫ x, F n x ∂μ) atTop (𝓝 (∫ x, f x ∂μ)) :=
  tendsto_integral_of_dominated_convergence g hF hg hbound hlim

The escaping-mass sequence $f_n = n \mathbf 1_{(0, 1/n)}$, formalised and analysed from scratch: every integral is $1$, every pointwise limit is $0$. Together these two theorems show formally that the hypotheses of the convergence theorems cannot simply be dropped.

/-- The "escaping mass" sequence `fₙ = n · 1_(0, 1/n)`: a tower of height `n` over an interval
of length `1/n`. -/
noncomputable def escapingMass (n : ℕ) : ℝ → ℝ≥0∞ :=
  (Ioo (0 : ℝ) (1 / n)).indicator fun _ => (n : ℝ≥0∞)

/-- Every `fₙ` (with `n ≥ 1`) has integral exactly `1`: the integral of `c · 1_A` is
`c · λ(A)`, and here `n · (1/n) = 1`. -/
theorem escapingMass_lintegral {n : ℕ} (hn : 1 ≤ n) : ∫⁻ x, escapingMass n x = 1 := by
  have hn' : (n : ℝ) ≠ 0 := by positivity
  rw [escapingMass, lintegral_indicator_const measurableSet_Ioo, Real.volume_Ioo, sub_zero,
    ← ENNReal.ofReal_natCast, ← ENNReal.ofReal_mul (Nat.cast_nonneg n), mul_one_div_cancel hn',
    ENNReal.ofReal_one]

/-- …yet `fₙ(x) → 0` for **every** `x ∈ ℝ`: if `x ≤ 0` every term is `0`; if `x > 0`, then as
soon as `n > 1/x` we have `x ∉ (0, 1/n)`, so `fₙ(x) = 0`. Hence `∫ lim fₙ = 0 ≠ 1 = lim ∫ fₙ`:
there is no integrable dominating function and the sequence is not monotone. -/
theorem escapingMass_tendsto_zero (x : ℝ) :
    Tendsto (fun n => escapingMass n x) atTop (𝓝 0) := by
  -- It suffices that `fₙ(x) = 0` for all large `n`.
  apply tendsto_const_nhds.congr'
  rcases le_or_gt x 0 with hx | hx
  · -- `x ≤ 0`: `x` is never in `(0, 1/n)`.
    refine Eventually.of_forall fun n => ?_
    have hmem : x ∉ Ioo (0 : ℝ) (1 / n) := fun h => (not_lt.2 hx) h.1
    show (0 : ℝ≥0∞) = escapingMass n x
    rw [escapingMass, indicator_of_notMem hmem]
  · -- `x > 0`: choose `N > 1/x`; for `n ≥ N` we have `1/n ≤ x`.
    obtain ⟨N, hN⟩ := exists_nat_gt (1 / x)
    filter_upwards [eventually_ge_atTop N] with n hn
    have hNpos : (0 : ℝ) < N := lt_trans (by positivity) hN
    have hnpos : (0 : ℝ) < n := lt_of_lt_of_le hNpos (by exact_mod_cast hn)
    have hle : 1 / (n : ℝ) ≤ x := by
      rw [div_le_iff₀ hnpos]
      have h1 : 1 < N * x := by rwa [div_lt_iff₀ hx] at hN
      nlinarith [show (N : ℝ) ≤ n by exact_mod_cast hn]
    have hmem : x ∉ Ioo (0 : ℝ) (1 / n) := fun h => (not_lt.2 hle) h.2
    show (0 : ℝ≥0∞) = escapingMass n x
    rw [escapingMass, indicator_of_notMem hmem]

Tonelli's theorem (Mathlib states it for s-finite measures, a class containing the σ-finite ones), the Riesz–Fischer theorem as a CompleteSpace instance on Mathlib's Lp (a type of a.e.-equivalence classes), and the first Borel–Cantelli lemma:

/-- **Tonelli's theorem.** For a measurable `f : α × β → [0, ∞]` and σ-finite (in Mathlib:
s-finite) measures, the integral over the product equals either iterated integral. This is
Mathlib's `lintegral_prod`. -/
theorem tonelli {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] (μ : Measure α)
    (ν : Measure β) [SFinite ν] (f : α × β → ℝ≥0∞) (hf : AEMeasurable f (μ.prod ν)) :
    ∫⁻ z, f z ∂μ.prod ν = ∫⁻ x, ∫⁻ y, f (x, y) ∂ν ∂μ :=
  lintegral_prod f hf

/-- **Riesz–Fischer.** For `1 ≤ p ≤ ∞`, the space `Lᵖ(μ)` (functions modulo equality almost
everywhere) is complete, hence a Banach space. Mathlib provides the instance
`MeasureTheory.Lp.instCompleteSpace`. -/
theorem lp_complete {α : Type*} [MeasurableSpace α] (μ : Measure α) (p : ℝ≥0∞)
    [Fact (1 ≤ p)] : CompleteSpace (Lp ℝ p μ) :=
  inferInstance

/-- **First Borel–Cantelli lemma.** If `∑ μ(Aₙ) < ∞`, then almost every point lies in only
finitely many `Aₙ`: `μ(limsup Aₙ) = 0`. This is Mathlib's `measure_limsup_atTop_eq_zero`. -/
theorem borel_cantelli {α : Type*} [MeasurableSpace α] (μ : Measure α) {A : ℕ → Set α}
    (hA : ∑' n, μ (A n) ≠ ∞) : μ (limsup A atTop) = 0 :=
  measure_limsup_atTop_eq_zero hA

Not formalised here: the Carathéodory construction and the Heine–Borel argument for $\lambda^*([a, b])$ (Mathlib has both, as MeasureTheory.OuterMeasure.caratheodory and StieltjesFunction.outer_Ioc), the proofs of the convergence theorems and of Riesz–Fischer (we cite Mathlib's), and the comparison with the Riemann integral (Mathlib relates intervalIntegral to antiderivatives through the fundamental theorem of calculus rather than through Riemann sums).

The first experiment builds the stages of the Cantor set with exact fractions. It confirms the lengths $(2/3)^n$, checks that $1/4 = 0.\overline{02}_3$ survives every stage computed without ever being an endpoint (so the Cantor set is more than its endpoints), and exhibits the injection from $0/1$-strings that drives the uncountability proof.

"""The Cantor set: uncountably many points, total length zero.

Builds the stages C_n of the middle-thirds Cantor set with exact rational
arithmetic: C_n is a union of 2^n closed intervals of total length (2/3)^n.
It then checks that 1/4 survives every stage computed although it is never an
endpoint, and shows the injection from 0/1-sequences into the Cantor set
(binary digit b -> ternary digit 2b) that makes it uncountable. Exact
arithmetic for finitely many stages; the limits are the lesson's proofs.
"""

from fractions import Fraction

def cantor_stage(n):
    """The 2^n closed intervals (a, b) of the n-th stage C_n, as Fractions."""
    if n < 0:
        raise ValueError("n must be non-negative")
    intervals = [(Fraction(0), Fraction(1))]
    for _ in range(n):
        new = []
        for a, b in intervals:
            third = (b - a) / 3
            new.append((a, a + third))
            new.append((b - third, b))
        intervals = new
    return intervals

def total_length(intervals):
    """Sum of the lengths of disjoint intervals."""
    return sum((b - a for a, b in intervals), Fraction(0))

def in_stage(x, n):
    """True if the rational x lies in C_n (checked by the ternary rule)."""
    x = Fraction(x)
    if not 0 <= x <= 1:
        return False
    for _ in range(n):
        if Fraction(1, 3) < x < Fraction(2, 3):
            return False
        x = 3 * x if x <= Fraction(1, 3) else 3 * x - 2
    return True

def ternary_digits(x, k):
    """The first k ternary digits of a rational x in [0, 1)."""
    x = Fraction(x)
    digits = []
    for _ in range(k):
        x *= 3
        d = int(x)
        digits.append(d)
        x -= d
    return digits

def endpoints(n):
    """All endpoints of the intervals of C_n."""
    return {e for interval in cantor_stage(n) for e in interval}

def bits_to_cantor_point(bits):
    """The point sum 2*b_i / 3^i of the Cantor set coded by the bits b_i."""
    return sum((Fraction(2 * b, 3 ** (i + 1)) for i, b in enumerate(bits)),
               Fraction(0))

def first_stage_below(threshold):
    """Least n with (2/3)^n < threshold."""
    n, length = 0, Fraction(1)
    while length >= threshold:
        n, length = n + 1, length * Fraction(2, 3)
    return n

def main():
    print("Stages of the Cantor set (exact arithmetic)")
    print(f"{'n':>3} {'intervals':>10} {'total length':>20} {'decimal':>10}")
    for n in [0, 1, 2, 3, 5, 10, 20]:
        stage = cantor_stage(n) if n <= 12 else None
        length = total_length(stage) if stage else Fraction(2, 3) ** n
        count = len(stage) if stage else 2 ** n
        print(f"{n:>3} {count:>10} {str(length):>20} {float(length):>10.6f}")
    print(f"Length below 1/1000 from stage n = {first_stage_below(Fraction(1, 1000))}.")
    print()
    quarter = Fraction(1, 4)
    print("Is 1/4 in the Cantor set?")
    print("  ternary digits of 1/4:", "".join(map(str, ternary_digits(quarter, 12))),
          "...")
    print(f"  in every stage C_n for n <= 40: {all(in_stage(quarter, n) for n in range(41))}")
    print(f"  an endpoint of some C_n, n <= 12: {quarter in endpoints(12)}")
    print("  (endpoints have denominators 3^n, and 4 is not a power of 3)")
    print()
    strings = [[(m >> i) & 1 for i in range(10)] for m in range(2 ** 10)]
    points = {bits_to_cantor_point(s) for s in strings}
    print("0/1 strings -> Cantor points by b -> ternary digit 2b:")
    print(f"  {len(strings)} strings of length 10 give {len(points)} distinct points,")
    print(f"  all in C_10: {all(in_stage(p, 10) for p in points)}")
    print()
    print("Epistemic status: exact rational arithmetic for finitely many stages")
    print("and strings. It shows that C is covered by intervals of total length")
    print("(2/3)^n for the n computed. That C is null (it lies in every C_n) and")
    print("that the injection on infinite sequences makes it uncountable are the")
    print("lesson's proofs, not consequences of this finite check.")

if __name__ == "__main__":
    main()