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.
Rokhlin consequence: Two measure-preserving maps into a standard Borel probability space can be "aligned" via measure-preserving bijections, and any two measurable partitions can be aligned by a measure-preserving bijection.
This is a consequence of Rokhlin's theorem: every standard Borel probability space is measure-theoretically isomorphic to [0,1] with Lebesgue measure.
The theorem provides two outputs:
- Map alignment: Given MP maps ψ₁, φ₂ : α → α, there exist MP bijections χ₁, χ₂ such that ψ₁ ∘ χ₁ =ᵐ[μ] φ₂ ∘ χ₂.
- Partition alignment: Given measurable partitions P, Q, there exists a MP bijection e mapping each P-cell a.e. into some Q-cell.
Both follow from the fact that (α, μ) ≅ ([0,1], λ). Map alignment is Kechris [1995], Theorem 17.41. Partition alignment follows because any finite measurable partition of [0,1] can be mapped to any other by a measure-preserving bijection (rearranging intervals).
Sorry: Requires Rokhlin's theorem, which is not yet in Mathlib. This is
well-established mathematics. This is one of three sorry declarations in
the formalization and the only one that requires genuinely new Mathlib
infrastructure. All other Rokhlin consequences (partition transfer,
alignment chains, controlled cell alignment) are derived from this.
The conclusion has three parts:
- Coupling: The two MP maps can be aligned via MP bijections.
- Partition alignment: Each cell of P maps a.e. to some cell of Q.
- Controlled cell alignment: Given a specific measure-matching correspondence between cells, the alignment can be chosen to realize it. This follows from Rokhlin's classification theorem applied cell-by-cell.
Map-alignment consequence of exists_common_extension: given two MP maps,
there exist MP bijections aligning them. This is the interface used by
cutDistance_triangle.
Partition-alignment consequence of exists_common_extension: given two
measurable partitions, there exists a MP bijection mapping each cell of the
first a.e. into a cell of the second.
Controlled cell alignment: given indexed families of cells from two partitions
with matching measures, there exists a MP bijection mapping each cell a.e. to the
corresponding cell. This is a direct consequence of the third conjunct of
exists_common_extension.
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.
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_extension (Rokhlin sorry).
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!