Cut Distance for Graphons #
This file defines the cut distance (also called cut metric) between graphons, which is the fundamental metric for graphon convergence theory.
Main definitions #
Graphon.cutNormDiff- The cut norm of the difference‖U - W‖_□Graphon.cutDistance- The cut distanceδ□(U, W) = inf_{φ,ψ} ‖U^φ - W^ψ‖_□(two-sided)
Main results #
Graphon.cutDistance_self-δ□(W, W) = 0Graphon.cutDistance_nonneg-0 ≤ δ□(U, W)
Implementation notes #
The cut distance is defined as an infimum over measure-preserving maps. In general, one needs to consider maps from a common probability space to both graphons.
The cut distance is a pseudometric: δ□(U, W) = 0 does not imply U = W, but
rather that U and W are weakly isomorphic (differ only by measure-preserving
reparametrization).
References #
- [L. Lovász, Large Networks and Graph Limits][lovasz2012], Section 8.2.2
Rectangle integral of difference #
The integral of the difference of two graphons over a measurable rectangle S × T.
Equations
Instances For
Rectangle integral of difference equals difference of rectangle integrals.
Cut norm of difference #
The cut norm of the difference of two graphons.
‖U - W‖_□ = sup_{S,T measurable} |∫_{S×T} (U - W)|
Since graphons take values in [0,1], their difference takes values in [-1,1].
Equations
- U.cutNormDiff W = ⨆ (S : Set α), ⨆ (_ : MeasurableSet S), ⨆ (T : Set α), ⨆ (_ : MeasurableSet T), |U.rectIntegralDiff W S T|
Instances For
Cut norm difference is non-negative.
Helper: absolute value of rectangle integral difference is bounded by 1.
Rectangle integral difference is bounded by cut norm difference.
Cut norm difference with self is zero.
Cut norm difference is symmetric.
Cut norm difference is bounded by 1.
Since U, W ∈ [0,1], we have U - W ∈ [-1,1], so |∫(U-W)| ≤ μ(S×T) ≤ 1.
Rectangle integral difference satisfies the triangle inequality.
Cut norm difference satisfies the triangle inequality.
Weighted integrals of differences #
Weighted integral of graphon difference bounded by cut norm difference (indicator case).
For measurable sets S, T: |∫∫ 1_S(x) 1_T(y) (U(x,y) - W(x,y)) dμ(x) dμ(y)| ≤ ‖U - W‖_□
This follows directly from the cut norm definition.
General weighted integral of graphon difference bounded by cut norm difference.
For f, g : α → [0, 1] measurable and graphons U, W: |∫∫ f(x) g(y) (U(x,y) - W(x,y)) dμ(x) dμ(y)| ≤ ‖U - W‖_□
Uses nested layer cake: first on f (reducing to indicator case), then on g. This is Lemma 10.21 in Lovász [2012].
Cut distance #
The cut distance between two graphons on the same probability space.
δ□(U, W) = inf_{φ,ψ} ‖U^φ - W^ψ‖_□
where the infimum is over all measure-preserving maps φ, ψ : α → α.
Design note: This two-sided definition reparametrizes BOTH graphons, making symmetry trivial by construction (swap φ and ψ). This matches the standard definition in Lovász which uses measure-preserving maps from a common probability space to both graphon spaces.
The one-sided definition inf_φ ‖U - W^φ‖_□ requires [StandardBorelSpace α] to prove
symmetry (via invertibility of measure-preserving maps). The two-sided definition avoids
this requirement while giving the same value on standard Borel spaces.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Cut distance is non-negative.
The set defining cut distance is nonempty (identity maps always work).
Cut distance of a graphon to itself is zero.
Cut distance is bounded by cut norm difference (using identity maps).
Cut distance is bounded by 1.
Scoping: the former exists_common_extension monolith was unprovable as stated #
See docs/rokhlin-scoping.md. The old monolithic Rokhlin stub bundled three conjuncts, two
of which are false as written; it has now been deleted and replaced by four corrected,
consumer-shaped cores (exists_common_coupling_maps, cutNormDiff_pullback_le,
exists_controlled_cell_alignment in this file; exists_mpEquiv_cutNormDiff_lt_add in
Graphon/Overlay.lean, whose overlay proof needs the downstream regularity lemma), each a
standard consequence of the atomless standard-Borel measure-isomorphism theorem. All four are
now proved (campaigns R2 + R3). The two lemmas below
certify the "measure-obvious" necessity facts that forced those corrections; the historical
counterexamples:
Map alignment via bijections is FALSE.
(α, μ) = ([0,1], λ),ψ₁ = id,φ₂ =the doubling mapx ↦ 2x mod 1: the demanded a.e.-injectiveχ₁withχ₁ =ᵐ φ₂ ∘ χ₂cannot equal the essentially 2-to-1φ₂ ∘ χ₂. The honest fact is a coupling with measure-preserving maps (exists_common_coupling_maps), used with the pullback contractioncutNormDiff_pullback_le.Arbitrary-partition alignment is FALSE unless the cell measures match — certified by
mp_align_forces_equal_measure. The honest form is equal-measure cell alignment (exists_controlled_cell_alignment,[NullSingletonClass μ]).Controlled cell alignment needs
[NullSingletonClass μ](atom counterexample; one-sided necessity bymp_maps_into_forces_measure_le).Conjunct 1 (map alignment via bijections) is FALSE. Take
(α, μ) = ([0,1], λ),ψ₁ = id,φ₂ =the doubling mapx ↦ 2x mod 1(both measure-preserving). The conclusion demands a measurable-equiv (a.e.-injective)χ₁withχ₁ =ᵐ φ₂ ∘ χ₂, butφ₂ ∘ χ₂is essentially 2-to-1, so on the conull agreement set a positive-measure set of collision pairs contradicts injectivity. The classical fact is a coupling statement with measure-preserving maps (not automorphisms ofα). The doubling counterexample is left as prose (formalizing the doubling map's 2-to-1-ness is not cheap and off the critical path).Conjunct 2 (arbitrary-partition alignment) is FALSE unless the cell measures match — certified by
mp_align_forces_equal_measurebelow. Counterexample:P = {A, Aᶜ}withμ A = 1/2andQ = trivialPartition(whose only cell has measure1).Conjunct 3 (controlled cell alignment) needs
[NullSingletonClass μ]. With atoms it fails even at equal measures: on{a,b,c}withμ = (1/2, 1/4, 1/4), no measure-preserving bijection maps the two-atom cell{b,c}into the one-atom cell{a}.mp_maps_into_forces_measure_lecertifies the one-sided measure necessity that underlies the cell-matching hypotheses.
Refutation support (conjunct 2). A measure-preserving e that aligns S with T
symmetrically (μ(S \ e⁻¹T) = 0 and μ(e⁻¹T \ S) = 0) forces μ S = μ T. Hence partition
alignment is impossible unless the two partitions have matching cell measures.
Refutation support (conjunct 3). If a measure-preserving e maps S a.e. into T,
then μ S ≤ μ T. For injective cell families whose measures sum to the whole space this forces
equality; with atoms present, equal measures are not enough to realize the map (see the scoping
note above), which is why the corrected cell-alignment lemma assumes [NullSingletonClass μ].
Common coupling of two measure-preserving maps (corrected Rokhlin consequence 1).
Given measure-preserving maps ψ₁, φ₂ : α → α on an atomless standard Borel probability
space, there are measure-preserving maps χ₁, χ₂ : α → α with ψ₁ ∘ χ₁ =ᵐ φ₂ ∘ χ₂.
This replaces the false exists_common_extension_maps: demanding χ₁, χ₂ be bijections
is unprovable (take ψ₁ = id, φ₂ = doubling — a bijection cannot equal an essentially
2-to-1 map a.e.; see the scoping note). The honest statement is a coupling: build the
relatively-independent joining of ψ₁, φ₂ over their common factor on α × α, then re-type
it onto α via the measure-isomorphism theorem — which needs [NullSingletonClass μ]. Interface for
cutDistance_triangle (used together with the pullback contraction
cutNormDiff_pullback_le, since χ₁, χ₂ are maps, not measure-preserving bijections).
Controlled cell alignment (corrected Rokhlin consequence 3). Given injective indexed
families of cells from two partitions with matching measures, over an atomless standard
Borel probability space, there is a measure-preserving bijection mapping each cell ι_S i
a.e. into ι_T i.
This is the honest, true form of the third conjunct of the old exists_common_extension
stub: it adds [NullSingletonClass μ] (necessary — see the atom counterexample in the scoping note and
mp_maps_into_forces_measure_le) and is now a standalone obligation resting only on the
measure-isomorphism theorem (campaign phase R1), not on the unprovable monolithic stub. It is
the sole cell-matching interface used by the inverse-counting route.
Cut norm difference is invariant under applying the same MeasurableEquiv to both graphons.
If e : α ≃ᵐ α is measure-preserving, then ‖U^e − W^e‖□ = ‖U − W‖□
The key insight: applying bijectivity of e, the sup over measurable S, T of |∫{S×T} (U^e − W^e)| equals the sup over measurable S', T' (images under e) of |∫{S'×T'} (U − W)|, which ranges over all measurable sets.
Pullback contracts the cut norm. For a measure-preserving map φ (not necessarily a
bijection), ‖U^φ − W^φ‖_□ ≤ ‖U − W‖_□.
Unlike cutNormDiff_pullback_measurableEquiv (equality, for bijections), this only requires
φ to be measure-preserving. Proof idea: writing the rectangle integrals of the pulled-back
kernels via the disintegration of μ along φ, each indicator 1_S becomes the conditional
probability E[1_S ∣ φ] ∈ [0,1], so the pulled-back cut norm is a weighted cut norm with
[0,1]-weights, which the cut norm dominates (abs_weighted_integral_diff_le). This is the
map-level companion the corrected coupling triangle needs; it rests on the standard-Borel
disintegration (campaign phase R1/R2).
Cut distance from a graphon to its pullback by a MP bijection is zero.
For any graphon V and measure-preserving bijection e, δ□(V, V^e) = 0.
Proof: Use φ = id and ψ = e⁻¹ as witnesses in the cutDistance infimum.
Then V^id = V and (V^e)^{e⁻¹} = V^{e ∘ e⁻¹} = V^id = V,
so ‖V − V‖_□ = 0.
For any ε > 0, there exist measure-preserving maps achieving cutDistance + ε.
Triangle inequality for cut distance on standard Borel spaces.
δ□(U, W) ≤ δ□(U, V) + δ□(V, W)
This is the key property making cut distance a pseudometric.
Proof: For any ε > 0:
- Choose (φ₁, ψ₁) with ‖U^φ₁ − V^ψ₁‖_□ < d(U,V) + ε
- Choose (φ₂, ψ₂) with ‖V^φ₂ − W^ψ₂‖_□ < d(V,W) + ε
- By Rokhlin's theorem, align ψ₁ and φ₂ via bijections χ₁, χ₂
- Compose maps and use cutNormDiff_triangle to get d(U,W) ≤ d(U,V) + d(V,W) + 2ε
- Take ε → 0.
Depends on: MeasurePreserving.exists_common_coupling_maps (corrected coupling, needs
[NullSingletonClass μ]) and cutNormDiff_pullback_le (pullback contraction).
Cut distance is symmetric.
δ□(U, W) = δ□(W, U)
With the two-sided definition, this is immediate by swapping φ and ψ and using the symmetry of cutNormDiff. No StandardBorelSpace needed!