Null set

A null set is a set to which a chosen measure assigns exactly zero mass. The measure must be named: the same set can be null for one measure and carry all the mass of another.

Null does not mean empty, logically impossible, or merely very unlikely. It means one precise equation,

where \(N\) is the set and \(\mu\) is the measure.

Start with one point in the unit interval

Let the outcome space be \(\Omega=[0,1]\), equipped with the uniform probability measure \(\mu\). For every interval \((a,b)\) inside \([0,1]\), its probability is its length \(b-a\).

Consider the singleton

To find its measure, trap it inside an interval whose length can be made as small as we like. For every integer \(n\ge 2\), set

The point \(1/2\) lies in every \(I_n\), and the interval has length

Because \(N\subseteq I_n\), monotonicity of a measure gives

The only nonnegative number below every \(1/n\) is zero. Therefore

The shrinking intervals are not the null set. They are measurable covers with positive but vanishing mass. Their job is to squeeze the unknown mass of the singleton between zero and numbers that approach zero.

A finite die is the nearby nonexample

Now let \(\Omega=\{1,2,3,4,5,6\}\) be a fair six-sided die, and use its uniform probability measure \(\mathbb P\). The singleton \(\{6\}\) has

so it is not null. In fact, every nonempty event for this die contains at least one face and therefore has probability at least \(1/6\). The empty set is the die’s only null set.

The interval singleton and the die singleton each contain exactly one point. Their cardinalities agree, but their measures do not. Counting points is not how a general measure determines whether a set is null.

The exact definition

Let \((\Omega,\mathcal F,\mu)\) be a measure space. Here \(\Omega\) is the underlying set, \(\mathcal F\) is its collection of measurable sets, and \(\mu\) assigns mass to those sets. A measurable set \(N\in\mathcal F\) is a \(\mu\)-null set when

Many authors also call any subset of such a set \(\mu\)-null. This broader usage is harmless for measure calculations because if \(A\subseteq N\) and \(\mu(N)=0\), then monotonicity forces \(\mu(A)=0\). Whether every such subset is itself measurable is a separate question about whether the measure space has been completed.

The subscript matters. With \(N=\{1/2\}\), let \(\lambda\) denote uniform measure on \([0,1]\), and let \(\delta_{1/2}\) denote the Dirac probability measure that puts all mass at \(1/2\). Then

The set did not change. The measure did.

Two closure rules do most of the work

Subsets inherit zero mass

If \(A\subseteq N\) and \(N\) is \(\mu\)-null, then

so \(\mu(A)=0\). This is the rule used in the shrinking-cover example and in many formal proofs: first place a complicated exceptional set inside a null cover, then transfer zero mass to the smaller set.

Countable unions stay null

If \(N_0,N_1,N_2,\ldots\) are all \(\mu\)-null, countable subadditivity gives

Therefore their union is null. This explains why a countable set such as \(\mathbb Q\cap[0,1]\) has uniform measure zero: enumerate its points and take a countable union of null singletons.

Countability is essential. The interval is the union of all of its singletons,

but this is an uncountable union, and the interval has uniform measure one. The countable-union theorem cannot be applied to that display.

Measure zero is not logical impossibility

Use the canonical realization

Its exact fiber at \(1/2\) satisfies

The first statement is about membership in this particular sample map’s range. The second is about mass. By contrast, the empty event contains no outcome at all.

This distinction becomes especially important when moving between a model and physical measurement. An atomless real probability law assigns zero probability to every singleton. That law alone does not say whether a particular singleton fiber is empty; it records only that the fiber has zero mass. Finite-resolution instruments report intervals, and those intervals can have positive probability.

There is no universal numerical threshold at which “small” becomes “null.” Null means exactly zero.

From null sets to almost-everywhere statements

A property \(P(\omega)\) holds almost everywhere with respect to \(\mu\) precisely when its failure set is null:

For the interval example, the statement \(x\ne1/2\) fails only on the null set \(\{1/2\}\), so it holds almost everywhere. For the fair die, “the roll is not six” fails on a set of probability \(1/6\), so it does not hold almost surely.

Countable unions let us combine countably many almost-everywhere statements. If statement \(k\) fails only on \(N_k\), then all statements hold simultaneously outside \(\bigcup_k N_k\), which is still null. The analogous claim for an uncountable family needs additional structure and is not a free consequence of the null-set rules.

In Lean: zero mass is the definition

Mathlib does not require a special bundled “null set” object for the basic calculation. It writes the defining equality directly.

μ N = 0

Run a finite null-set ledger locally

The continuous singleton proof uses real analysis, but the logical distinction between nonempty and zero mass already appears on a four-element weighted carrier. Give the two named ghost elements weight zero, give the other two elements weights two and three, and read every weight in fifths. The singleton set containing ghostA is visibly nonempty while its mass is zero. This ledger compares set membership with measure; it does not assert that a sampling mechanism returns a zero-weight ghost.

Save the following as /tmp/NullSetTutorial.lean:

import Std

inductive Atom where
  | ghostA
  | ghostB
  | left
  | right
deriving Repr, DecidableEq

abbrev Event := Atom → Bool

def atoms : List Atom := [.ghostA, .ghostB, .left, .right]

def label : Atom → String
  | .ghostA => "ghost-a"
  | .ghostB => "ghost-b"
  | .left => "left"
  | .right => "right"

def spreadWeight : Atom → Nat
  | .ghostA | .ghostB => 0
  | .left => 2
  | .right => 3

def diracAtGhostA : Atom → Nat
  | .ghostA => 5
  | _ => 0

def mass (weight : Atom → Nat) (event : Event) : Nat :=
  atoms.foldl (fun total atom =>
    if event atom then total + weight atom else total) 0

def singleton (chosen : Atom) : Event :=
  fun atom => decide (atom = chosen)

def ghostUnion : Event :=
  fun atom => decide (atom = .ghostA ∨ atom = .ghostB)

def ghostAWithLeft : Event :=
  fun atom => decide (atom = .ghostA ∨ atom = .left)

def members (event : Event) : List String :=
  (atoms.filter event).map label

#eval members (singleton .ghostA)
#eval mass spreadWeight (singleton .ghostA)
#eval mass diracAtGhostA (singleton .ghostA)
#eval mass spreadWeight ghostUnion
#eval mass spreadWeight ghostAWithLeft

example : members (singleton .ghostA) = ["ghost-a"] := by native_decide
example : mass spreadWeight ghostUnion = 0 := by native_decide
example : mass spreadWeight ghostAWithLeft = 2 := by native_decide

Type exactly:

source "$HOME/.elan/env"
elan run leanprover/lean4:v4.32.0 lean /tmp/NullSetTutorial.lean

This exact worksheet was executed successfully with Lean 4.32.0. It printed:

["ghost-a"]
0
5
0
2

The first two lines jointly certify the key boundary: the event has one member but zero fifth-units of spreadWeight. The third line changes only the measure; the same singleton now carries all five units. The fourth line shows that the union of the two zero-weight singleton events is still null. The last line adds left, so the event acquires mass (2/5).

Here Atom → Bool is a small executable representation of event membership, mass adds the weights of the selected atoms, and each example asks Lean’s kernel to check a finite equality. This Std worksheet does not formalize Lebesgue measure, the shrinking-cover argument, or Mathlib’s general countable-union theorem. Those belong to the project-backed worksheet below.

Try the exact measure theorems in the repository

Two Mathlib lemmas encode the closure rules from the previous section. measure_mono_null transfers zero mass from a set to any subset, and measure_iUnion_null combines a countable family of null sets. In a clone with the repository’s pinned Lean and Mathlib dependencies installed, a human can type this worksheet:

import NonlinearDynamics.Random.RandomCocycles.SubadditiveKingman

open MeasureTheory Set

#check measure_mono_null
#check measure_iUnion_null

example {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    {A N : Set Ω} (hAN : A ⊆ N) (hN : μ N = 0) :
    μ A = 0 :=
  measure_mono_null hAN hN

example {Ω ι : Type*} [MeasurableSpace Ω] [Countable ι]
    (μ : Measure Ω) (N : ι → Set Ω)
    (hN : ∀ i, μ (N i) = 0) :
    μ (⋃ i, N i) = 0 :=
  measure_iUnion_null hN

#check NonlinearDynamics.Random.RandomCocycles.IsIntegrableSubadditiveProcessCandidate.measure_centeredRationalLowerDeviationExhaustionSet_eq_zero

#check NonlinearDynamics.Random.RandomCocycles.IsIntegrableSubadditiveProcessCandidate.measure_centeredLowerLiminfDeviationSet_eq_zero

The first two #check commands ask Lean to report Mathlib’s theorem types. Each example then supplies all arguments explicitly, and Lean’s kernel checks the resulting proof term. [Countable ι] is the important gate on the second example; without it, the union theorem would be false.

The final two commands point to checked project declarations. In SubadditiveKingman.lean, the rational lower-deviation exhaustion is a countable union. Its proof uses measure_iUnion_null to show the union is null. The next theorem places a real lower-liminf deviation set inside that exhaustion and uses measure_mono_null to transfer zero mass to the subset. This is the same two-step architecture as the paper argument: build a null cover, then descend to the event of interest.

cd formalization
lake env lean -DwarningAsError=true NonlinearDynamics/Random/RandomCocycles/SubadditiveKingman.lean

Boundaries worth keeping visible

Where to continue

The measurable space entry explains which sets are available as measurable events. The almost-everywhere entry turns a null failure set into a quantified statement. The probability distribution (law) entry shows how a random object moves probability onto its value space, and the pushforward measure entry develops that construction directly.

For the project-scale use of countable null covers, continue to Rational slack, lower-deviation events, and ergodic null selection. That Deep Dive explains why rational thresholds supply a countable family and how the resulting null event enters the log-positive Kingman argument.

References

Mathlib contributors. Outer-measure foundations, Mathlib 4 documentation. This is the official implementation reference for measure_mono_null, measure_iUnion_null_iff, and the measure_iUnion_null alias used by the project.

Olav Kallenberg. Foundations of Modern Probability, third edition, Springer, 2021. This develops null events, almost-everywhere reasoning, and probability measures in a standard measure-theoretic setting.

Project source. SubadditiveKingman.lean contains the checked countable-union and subset-null proof architecture described in the Lean section.