The atomless standard-Borel measure-isomorphism theorem (Rokhlin campaign, R1) #
This file builds, from the ground up, the measure-theoretic core that the graphon program's
four corrected Rokhlin cores (exists_common_coupling_maps, cutNormDiff_pullback_le,
exists_controlled_cell_alignment in Graphon/CutDistance.lean;
exists_mpEquiv_cutNormDiff_lt_add in Graphon/Overlay.lean) all reduce to (see
docs/rokhlin-scoping.md §7–8). All four are proved (campaigns R2 + R3, 2026-07-09;
see docs/overlay-scoping.md for the overlay), so the graphon program carries no live
measure-theory obligation:
An atomless standard-Borel probability space
(α, μ)is measure-preservingly isomorphic mod 0 to([0,1], Lebesgue).
Hypotheses are stated via NullSingletonClass μ (every singleton is null). In an arbitrary
measurable space that is weaker than atomlessness; on the standard-Borel spaces of this file
the two coincide, and the prose uses "atomless" in that sense.
It is deliberately independent of graphons — pure Mathlib-style measure theory, and a
plausible upstreaming target (the Architect import supplies only the @[blueprint]
annotation attribute; strip it when upstreaming).
Roadmap (R1) #
- R1b
continuous_cdf_of_noAtoms— the CDF of an atomless probability measure onℝis continuous. PROVED. - R1c
cdf_map_eq_volume_restrict— the probability integral transform: the CDF pushes an atomless probability measure onℝto Lebesgue measure on[0,1]. PROVED. - R1d the quantile map is a mod-0 inverse of the CDF (a.e. inverse both directions). PROVED.
- R1e transport a general atomless standard-Borel probability space to the real line via
embeddingReal, then assemble the mod-0 iso (atomless_standardBorel_mod0MeasureIso_unitInterval). PROVED. - R2.0 the mod-0 → everywhere upgrade (
Mod0MeasureIso.toMeasurableEquiv), via null-reservoir patching andexists_uncountable_null_measurableSet. PROVED.
R2/R3 then derive the four cores by conjugating through the isomorphism — all complete.
R1b — CDF continuity from null singletons. The cumulative distribution function of a
null-singleton probability measure on ℝ is continuous. (A general CDF is only
right-continuous; the left jumps are exactly the singleton masses,
cdf ν x − leftLim (cdf ν) x = ν {x}, which vanish.)
R1c — the probability integral transform (crux). For an atomless probability measure
ν on ℝ, its CDF pushes ν forward to Lebesgue measure on the unit interval:
(cdf ν)_* ν = volume.restrict (Icc 0 1).
Proof: by ext_of_Iic it suffices to match (cdf ν)_* ν (Iic y) with volume.restrict (Icc 0 1) (Iic y) for every y. The former is ν {x | cdf ν x ≤ y}; the latter is volume (Iic y ∩ Icc 0 1). For y < 1 both equal ENNReal.ofReal y (cdf_sublevel_measure, and Iic y ∩ Icc 0 1 = Icc 0 y); for y ≥ 1 both equal 1 (the sublevel set is univ since cdf ≤ 1 ≤ y, and
Iic y ∩ Icc 0 1 = Icc 0 1).
R1d — the quantile map as a mod-0 inverse of the CDF #
R1d — the quantile (generalized-inverse) map. cdfQuantile ν u is the least x whose
CDF value is at least u. By the ℝ conventions sInf ∅ = sInf univ = 0, it equals 0 for
u ≤ 0 (the sublevel set is all of ℝ) and for u > 1 (the sublevel set is empty); on the
open interval Ioo 0 1 it is a genuine two-sided inverse of the (continuous) CDF.
Equations
- Graphon.MeasureIso.cdfQuantile ν u = sInf {x : ℝ | u ≤ ↑(ProbabilityTheory.cdf ν) x}
Instances For
R1d — measurability of the quantile map. Although cdfQuantile ν is not globally
monotone (it drops back to 0 outside [0,1]), each sublevel set {u | cdfQuantile ν u ≤ c}
splits, by the region of u, into the manifestly measurable pieces coming from the constant
value 0 on Iic 0 ∪ Ioi 1, the Galois identity on Ioo 0 1, and the single point {1}.
R1d — first a.e. inverse. On [0,1] (equipped with Lebesgue measure) the CDF is a left
inverse of the quantile: cdf ν (cdfQuantile ν u) = u for a.e. u, since the exceptional set
lies in the volume-null pair {0, 1}.
R1d — the quantile transform (the isomorphism identity). The quantile pushes Lebesgue
measure on [0,1] forward to ν. By ext_of_Iic it suffices to match Iic-measures: the
preimage cdfQuantile ν ⁻¹' Iic t ∩ Icc 0 1 agrees, up to the null pair {0, 1}, with
Ioc 0 (cdf ν t) (Galois identity on Ioo 0 1), whose volume is cdf ν t = ν (Iic t).
R1d — second a.e. inverse. The quantile is a left inverse of the CDF ν-a.e.:
cdfQuantile ν (cdf ν x) = x for a.e. x. Since cdf ν x > 0 a.e.-ν (the left tail
{cdf ≤ 0} is ν-null) we get cdfQuantile ν (cdf ν x) ≤ x a.e.; combined with the equal
pushforwards map (cdfQuantile ν ∘ cdf ν) ν = ν (via the two transport identities) and the
monotone bounded arctan test, the a.e. inequality is forced to an a.e. equality.
R1e — the mod-0 measure isomorphism, packaged and assembled #
We package a measure-preserving isomorphism mod 0 as a bundled Mod0MeasureIso structure
(two measurable maps that push each measure to the other and are mutually inverse a.e.), prove
it composes (Mod0MeasureIso.trans), instantiate it on the real line via the CDF/quantile pair
(realMod0MeasureIso), and transport a general atomless standard-Borel probability space to the
real line via embeddingReal (embeddingRealMod0MeasureIso). Composing the two yields the main
theorem: every atomless standard-Borel probability space is isomorphic mod 0 to
([0,1], Lebesgue) (atomless_standardBorel_mod0MeasureIso_unitInterval).
R1e — a measure-preserving isomorphism mod 0. A pair of measurable maps toFun, invFun
that push μ and ν onto each other and are two-sided inverses almost everywhere.
- toFun : α → β
- invFun : β → α
- measurable_toFun : Measurable self.toFun
- measurable_invFun : Measurable self.invFun
Instances For
R1e — composition of mod-0 isomorphisms. The a.e.-inverse identities are chained by
pulling each factor's a.e. identity back through the other map, using that the pushforward
equalities make the maps QuasiMeasurePreserving (so ν-a.e. statements become μ-a.e.
statements after precomposition, via QuasiMeasurePreserving.ae_eq).
Equations
Instances For
R1e — the real-line instance. The CDF/quantile pair of an atomless probability measure
ν on ℝ is a mod-0 isomorphism between (ℝ, ν) and ([0,1], Lebesgue).
Equations
- One or more equations did not get rendered due to their size.
Instances For
R1e — the standard-Borel embedding instance. A standard-Borel space α measurably embeds
into ℝ via embeddingReal; that embedding is a mod-0 isomorphism from (α, μ) to the
pushforward (ℝ, map (embeddingReal α) μ). The right inverse holds ν-a.e. because ν is
concentrated on the range of the embedding.
Equations
- One or more equations did not get rendered due to their size.
Instances For
R1e — the atomless standard-Borel measure-isomorphism theorem. Every atomless
standard-Borel probability space (α, μ) is measure-preservingly isomorphic mod 0 to
([0,1], Lebesgue). Assembled by embedding α into ℝ and composing with the real-line
CDF/quantile isomorphism of the (atomless, probability) pushforward measure.
Brick 1 — parameterized patching lemma (R2.0a). Upgrade a mod-0 isomorphism to a genuine
measure-preserving MeasurableEquiv, assuming two null uncountable reservoir sets are already in
hand — one on each side. The reservoirs are removed from the a.e.-defined bijection region so that
both leftover "defect" sets become uncountable standard-Borel spaces, hence Borel-isomorphic via
measurableEquivOfNotCountable; gluing that Borel isomorphism onto the honest bijection produces an
everywhere ≃ᵐ that still agrees with toFun/invFun almost everywhere (so it is measure
preserving). This isolates all the MeasurableEquiv-gluing and a.e.-transfer bookkeeping from the
reservoir construction (Brick 2).
Brick 2 — null reservoir lemma (R2.0b). Every atomless standard-Borel probability space
contains an uncountable Borel set of measure zero. This is the reservoir fed to Brick 1. (Stated
without a "⊆ A" constraint: Brick 1 removes the reservoir from its bijection region regardless,
so the reservoir need not live inside any prescribed conull set — a strengthening of hypotheses
that makes the construction cleaner.)
Brick 3 — the mod-0 → measure-preserving MeasurableEquiv upgrade (R2.0). Every mod-0
isomorphism between atomless standard-Borel probability spaces upgrades to a genuine everywhere
measure-preserving MeasurableEquiv that still agrees with the original maps almost everywhere.
Assembled from Brick 2 (a null uncountable reservoir on each side) and Brick 1 (the null-patch
gluing). This is the graphon-independent theorem the R2 cell-alignment/mpEquiv cores consume.