Measurable function

A measurable function respects the information declared observable on its source and target. Every allowed yes-or-no question about the reported value must turn into an allowed yes-or-no question about the original outcome.

The word refers to the measurable structures around a function, not merely to the formula used to compute it.

Start with a die-to-parity map

Let

be the possible results of one die roll. Suppose the source records only parity. Write

and give \(\Omega\) the event family

This is the parity-only measurable space from the neighboring entry. Its four sets are the only source events available to this model.

Let the target be

with every subset of \(Y\) measurable. Define the parity function

by

There are only four target events, so we can check every one:

Every allowed target question pulls back to an allowed source question. Therefore \(p\) is measurable for these chosen structures.

A contrasting exact-face readout

Keep the same parity-only source \((\Omega,\mathcal F)\). Let the target also be \(\Omega\), but give the target every subset as a measurable event. Define the exact-face readout

The formula is the identity. Nevertheless, the target singleton \(\{2\}\) is measurable while

Thus \(r\) is not measurable from the parity-only source to the full exact-face target.

Nothing is wrong with the set \(\{2\}\), and nothing is wrong with the identity formula. The mismatch lies between the source and target information structures. If the source also carried every subset as a measurable event, the same identity formula would be measurable.

The definition

Let \((\Omega,\mathcal F)\) and \((Y,\mathcal G)\) be measurable spaces. A function

is measurable when

for every target set \(B\). The preimage

collects the source outcomes that make the target event \(B\) occur.

The superscript \(-1\) in \(f^{-1}(B)\) does not assert that \(f\) has an inverse function. Every function has a preimage operation on sets, even when the function is many-to-one. The die parity map is many-to-one, yet its preimages are perfectly well-defined.

Measurability uses preimages rather than forward images because inverse images preserve complements and countable unions exactly:

and

Those identities align with the closure rules of sigma algebras.

A formula is not a measurability proof

Writing down \(f(\omega)\) defines a function. It does not by itself establish how target events pull back through the chosen measurable spaces.

This separation is explicit in Lean. A term f : Ω → Y is the function. A separate term hf : Measurable f is a proof about that function under the measurable-space instances currently attached to Ω and Y.

The project’s RandomMatrix base type follows the same pattern: it is only an outcome-to-matrix function. The theorem that the map is measurable is a distinct hypothesis or a field of a richer bundle.

Why probability laws need this condition

A pushforward measure assigns a target event \(B\) the source mass of \(f^{-1}(B)\). The familiar equation is

For the right side to be available for every measurable target event, those preimages must be measurable source events. This is why the project’s probability-law interfaces carry measurability explicitly instead of treating an arbitrary function as though it automatically induced a probability distribution .

A measurable space alone chooses admissible sets. A measure later assigns sizes to them. Measurability of \(f\) does not itself choose either a source measure or a probability law.

Measurable is not the same as continuous or integrable

These properties answer different questions.

In the usual Borel measurable spaces on \(\mathbb R\), the step function

is measurable but is not continuous at zero. Measurability permits this jump because the preimages of Borel target sets remain Borel.

For a different separation, put counting measure on \(\mathbb N\). The constant function \(g(n)=1\) is measurable because every subset is measurable, but it is not integrable over all of \(\mathbb N\):

So measurability is necessary for ordinary integration theory, but it is not a finite-integral estimate.

In Lean

The pinned Mathlib definition is almost a word-for-word rendering of the paper definition.

Measurable f

Here is the exact definition from the pinned Mathlib source:

def Measurable [MeasurableSpace α] [MeasurableSpace β] (f : α → β) : Prop :=
  ∀ ⦃t : Set β⦄, MeasurableSet t → MeasurableSet (f ⁻¹' t)

The bridge uses the page’s names \(\Omega\), \(Y\), and \(B\); the library uses generic type names α, β, and target-set name t. Renaming bound variables does not change the proposition.

The random-matrix foundation then packages a structured use of this general definition. This is the exact checked project theorem:

theorem measurable_iff_entries (X : RandomMatrix Ω ι κ 𝕜) :
    Measurable X ↔ ∀ i j, Measurable fun ω ↦ X ω i j := by
  rw [measurable_comap_iff]
  change Measurable (fun ω i j ↦ X ω i j) ↔ _
  simp only [measurable_pi_iff]

It says that a matrix-valued function is measurable exactly when every scalar entry function is measurable. The target matrix measurable space is built entry by entry, so the theorem turns one structured pullback condition into a family of coordinate conditions.

Pull back all four parity events locally

Lean Core does not include Mathlib’s measure theory, but a small Std program can compute the page’s complete finite preimage table. Here false means odd and true means even. Save this as /tmp/MeasurableFunctionScratch.lean on a normal Mac or Linux computer:

import Std

namespace MeasurableFunctionScratch

def faces : List Nat := [1, 2, 3, 4, 5, 6]

def parity (face : Nat) : Bool :=
  face % 2 == 0

def preimage (event : Bool → Bool) : List Nat :=
  faces.filter (fun face => event (parity face))

def targetEvents : List (Bool → Bool) :=
  [fun _ => false,
   fun isEven => !isEven,
   fun isEven => isEven,
   fun _ => true]

def sourceAllowed (event : List Nat) : Bool :=
  event == [] ||
  event == [1, 3, 5] ||
  event == [2, 4, 6] ||
  event == faces

def pulledBackEvents : List (List Nat) :=
  targetEvents.map preimage

def exactFaceTwo : List Nat :=
  faces.filter (fun face => face == 2)

#eval pulledBackEvents
#eval pulledBackEvents.map sourceAllowed
#eval exactFaceTwo
#eval sourceAllowed exactFaceTwo

example : pulledBackEvents =
    [[], [1, 3, 5], [2, 4, 6], [1, 2, 3, 4, 5, 6]] := by decide
example : pulledBackEvents.map sourceAllowed =
    [true, true, true, true] := by decide
example : exactFaceTwo = [2] := by decide
example : sourceAllowed exactFaceTwo = false := by decide

end MeasurableFunctionScratch

Type these commands exactly:

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

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

[[], [1, 3, 5], [2, 4, 6], [1, 2, 3, 4, 5, 6]]
[true, true, true, true]
[2]
false

The first two lines exhaust every event in the two-value target and show that all four preimages belong to the parity-only source family. The last two lines reproduce the exact-face counterexample. This computes the finite set ledger; it does not replace a proof of Mathlib’s general Measurable f proposition.

Full project check

This Mathlib-backed file exposes the definition through a single target event and then asks Lean for the project’s coordinatewise theorem. This full project check uses the repository’s pinned Lean and Mathlib dependencies and may require substantial disk space and memory.

import NonlinearDynamics.Random.RandomMatrices.Basic

universe u v

variable {Ω : Type u} {Y : Type v}
variable [MeasurableSpace Ω] [MeasurableSpace Y]
variable (f : Ω → Y)

#check Measurable
#check MeasurableSet
#check Set.preimage
#check NonlinearDynamics.Random.RandomMatrix.measurable_iff_entries

example (hf : Measurable f) {B : Set Y} (hB : MeasurableSet B) :
    MeasurableSet (f ⁻¹' B) := by
  exact hf hB

Read the example from left to right. The input hf is the complete measurability proof. The input hB certifies one target event. Applying hf to hB returns the required proof that the preimage is a measurable source event.

cd formalization
lake env lean -DwarningAsError=true NonlinearDynamics/Random/RandomMatrices/Basic.lean

Boundaries and nonclaims

• Measurability is relative to both measurable spaces. The same underlying formula can be measurable for one pair and nonmeasurable for another.
• A preimage is not an inverse function. No bijectivity is required.
• Checking a few convenient target events is not generally enough. The die example is complete only because all four target events were listed.
• Measurability uses inverse images. Forward images of measurable sets need not be measurable without additional hypotheses.
• A measurable function need not be continuous or integrable.
• A proof of Measurable f does not select a measure, assign probabilities, or prove an almost-everywhere statement.

Where to continue

The measurable space page builds the source and target event families used here. The pushforward measure page follows the preimage into the law construction. The almost-everywhere page explains what changes when a property may fail on a null set.

Further reading

Mathlib’s measurable-space definitions give the exact pinned definition used above. Olav Kallenberg’s Foundations of Modern Probability develops measurable mappings before using them to define random elements and their distributions.