The cut distance of two graphons

The cut distance of two graphons is

δ□(U, W) = inf { ‖overlayDiff U W π‖□ | π a coupling of the two carriers },

the infimum, over couplings of the two carriers, of the cut norm of the overlaid difference. This file defines it and develops the part of its theory that does not need the triangle inequality.

Coupling-primary, and cross-carrier by construction. U and W live on different probability spaces, and nothing here asks them to be standard Borel or atomless — a coupling always exists (isCoupling_prod), so the infimum is over a nonempty set of nonnegative reals and is a genuine infimum rather than a junk value. The competing definition, an infimum over measure-preserving maps into a common carrier, is not more general: it agrees with this one over standard Borel carriers, which is a separate later target.

The triangle inequality is not proved here. On arbitrary carriers it is Janson's Lemma 6.5, whose proof reduces the gluing of two couplings to the finite case by step-graphon approximation, and the roadmap makes that reduction a milestone of its own. Everything below — nonnegativity, the [0, 1] range, symmetry, reflexivity, and the common-carrier upper bound — is independent of it.

Symmetry is a swap of couplings, not a rearrangement. cutDist_comm holds on arbitrary carriers because Prod.swap turns a coupling of μ₁, μ₂ into one of μ₂, μ₁ and negates the overlaid difference, and the cut norm is even and drops along a pushforward (cutNorm_le_cutNorm_comap). No common carrier and no measurable-isomorphism hypothesis appears.

Main definitions

• TauCeti.DenseGraphLimits.cutDist — the infimum of the overlaid cut norms over couplings of the two carriers.

Main results

• cutDist_le and le_cutDist are the introduction and elimination rules for the infimum, and exists_isCoupling_cutNorm_lt produces a coupling beating any strict upper bound;
• cutDist_nonneg and cutDist_le_one are the range;
• cutDist_comm is symmetry;
• cutNorm_overlayDiff_map_prodMk computes the overlaid cut norm of a coupling induced by two measure-preserving maps, and cutDist_le_cutNorm_sub_of_measurePreserving bounds the cut distance by that value; cutDist_le_cutNorm_sub is its identity case, and cutDist_self follows;
• cutDist_le_cutDist_comap_right compares the cut distance with its value against a measure-preserving pullback of the right-hand graphon;
• cutNorm_overlayDiff_diagonalCoupling computes the value the diagonal coupling contributes to that infimum: it is exactly the same-carrier cut norm of the difference.

Implementation

The private implementation set couplingCutNorms is named rather than inlined because both csInf rules need it: cutDist_le needs the set to be bounded below and le_cutDist needs it to be nonempty, and those two facts are stated about it once instead of being unfolded at each use. The definition carries the IsFiniteMeasure evidence supplied by a coupling explicitly, in the @ form, because an existentially quantified witness cannot supply an instance by unification. Since IsFiniteMeasure is a Prop class, that instance is interchangeable with any other by proof irrelevance, and callers holding [IsProbabilityMeasure π] may use the lemmas below with the ordinary cutNorm π on the nose.

References

• S. Janson, Graphons, cut norm and distance, couplings and rearrangements, NYJM Monographs 4 (2013), §6 — the coupling definition of the cut distance, and Lemma 6.5 for the triangle inequality on arbitrary carriers.
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), §8.2.
• Roadmap: TauCetiRoadmap/DenseGraphLimits/README.md, Layer 1 — the coupling-primary, cross-carrier cutDist and its basic laws; the signature follows TauCetiRoadmap/DenseGraphLimits/Suggested.lean, with the two carrier measures implicit as in overlayDiff. The triangle inequality, the GraphonSpace quotient, and the agreement with the measure-preserving-map form are separate targets and are not built here.

noncomputable def TauCeti.DenseGraphLimits.cutDist {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] (U : Graphon Ω₁ μ₁) (W : Graphon Ω₂ μ₂) : ℝ

The cut distance of two graphons: the infimum, over couplings of their carriers, of the cut norm of the overlaid difference.

The two graphons may live on different probability spaces, and no standard Borel or atomless hypothesis is imposed on either.

Equations

• TauCeti.DenseGraphLimits.cutDist U W = sInf (TauCeti.DenseGraphLimits.couplingCutNorms✝ U W)

theorem TauCeti.DenseGraphLimits.cutDist_le {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] (U : Graphon Ω₁ μ₁) (W : Graphon Ω₂ μ₂) {π : MeasureTheory.Measure (Ω₁ × Ω₂)} (hπ : MeasureTheory.IsCoupling μ₁ μ₂ π) : cutDist U W ≤ cutNorm π (overlayDiff U W π)

The cut distance is at most the overlaid cut norm along any coupling: the introduction rule for the infimum.

theorem TauCeti.DenseGraphLimits.le_cutDist {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] {c : ℝ} (U : Graphon Ω₁ μ₁) (W : Graphon Ω₂ μ₂) (h : ∀ (π : MeasureTheory.Measure (Ω₁ × Ω₂)) (hπ : MeasureTheory.IsCoupling μ₁ μ₂ π), c ≤ cutNorm π (overlayDiff U W π)) : c ≤ cutDist U W

To bound the cut distance from below it suffices to bound every overlaid cut norm from below: the elimination rule for the infimum.

theorem TauCeti.DenseGraphLimits.exists_isCoupling_cutNorm_lt {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] (U : Graphon Ω₁ μ₁) (W : Graphon Ω₂ μ₂) {c : ℝ} (h : cutDist U W < c) : ∃ (π : MeasureTheory.Measure (Ω₁ × Ω₂)) (hπ : MeasureTheory.IsCoupling μ₁ μ₂ π), cutNorm π (overlayDiff U W π) < c

Any strict upper bound on the cut distance is beaten by some coupling. This is the form in which a cut-distance hypothesis is used: it turns an infimum into an explicit coupling.

theorem TauCeti.DenseGraphLimits.cutDist_nonneg {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] (U : Graphon Ω₁ μ₁) (W : Graphon Ω₂ μ₂) : 0 ≤ cutDist U W

The cut distance is nonnegative.

theorem TauCeti.DenseGraphLimits.cutDist_le_one {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] (U : Graphon Ω₁ μ₁) (W : Graphon Ω₂ μ₂) : cutDist U W ≤ 1

The cut distance of two graphons is at most 1: the independent coupling already realises a value at most 1, since the overlaid difference is [-1, 1]-valued and the carrier is a probability space.

theorem TauCeti.DenseGraphLimits.cutDist_comm {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] (U : Graphon Ω₁ μ₁) (W : Graphon Ω₂ μ₂) : cutDist U W = cutDist W U

The cut distance is symmetric.

This holds on arbitrary probability carriers: a coupling of μ₁ and μ₂ swaps to one of μ₂ and μ₁, so the two infima range over matching sets of values.

theorem TauCeti.DenseGraphLimits.cutNorm_overlayDiff_map_prodMk {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] {Ω : Type u_3} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (U : Graphon Ω₁ μ₁) (W : Graphon Ω₂ μ₂) {f : Ω → Ω₁} {g : Ω → Ω₂} (hf : Measurable f) (hg : Measurable g) {π : MeasureTheory.Measure (Ω₁ × Ω₂)} [MeasureTheory.IsFiniteMeasure π] (hπ : MeasureTheory.MeasurePreserving (fun (x : Ω) => (f x, g x)) μ π) : cutNorm π (overlayDiff U W π) = cutNorm μ (U.comap f hf μ - W.comap g hg μ)

A measure induced by two maps gives the cut norm of the difference of the two pullbacks. Pulling the overlaid difference back along x ↦ (f x, g x) gives the difference of the pullbacks. Invariance under this measure-preserving map then identifies the two cut norms.

theorem TauCeti.DenseGraphLimits.cutDist_le_cutNorm_sub_of_measurePreserving {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] {Ω : Type u_3} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (U : Graphon Ω₁ μ₁) (W : Graphon Ω₂ μ₂) {f : Ω → Ω₁} {g : Ω → Ω₂} (hf : MeasureTheory.MeasurePreserving f μ μ₁) (hg : MeasureTheory.MeasurePreserving g μ μ₂) : cutDist U W ≤ cutNorm μ (U.comap f ⋯ μ - W.comap g ⋯ μ)

A common carrier bounds the cut distance. If f and g are measure preserving from a common finite-measure space onto the two carriers, then the cut distance is at most the ordinary cut norm of the difference of the two pullbacks.

This is the inequality that makes the measure-preserving-map picture an upper bound for the coupling-primary one: the graph of (f, g) pushes μ forward to a coupling (isCoupling_map_prodMk), and the overlaid difference along it pulls back to the plain difference of the pullback kernels. That the infimum over such pairs is equal to the cut distance is a separate, later target, and needs standard Borel carriers.

theorem TauCeti.DenseGraphLimits.cutDist_le_cutDist_comap_right {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] {Ω₂' : Type u_4} [MeasurableSpace Ω₂'] {μ₂' : MeasureTheory.Measure Ω₂'} [MeasureTheory.IsProbabilityMeasure μ₂'] (U : Graphon Ω₁ μ₁) (W : Graphon Ω₂ μ₂) {f : Ω₂' → Ω₂} (hf : MeasureTheory.MeasurePreserving f μ₂' μ₂) : cutDist U W ≤ cutDist U (W.comap f ⋯ μ₂')

Reading the right-hand graphon along a measure-preserving map does not decrease the cut distance: if f : Ω₂' → Ω₂ is measure preserving, then cutDist U W ≤ cutDist U (W.comap f hf.measurable μ₂').

The two sides are in fact equal; the reverse inequality needs the triangle inequality and is TauCeti.DenseGraphLimits.cutDist_comap_right in TauCeti.Combinatorics.DenseGraphLimits.CutMetric.Triangle.

theorem TauCeti.DenseGraphLimits.cutDist_le_cutNorm_sub {Ω : Type u_3} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (U W : Graphon Ω μ) : cutDist U W ≤ cutNorm μ (U.toSymmKernel - W.toSymmKernel)

The cut distance of two graphons on one carrier is at most the cut norm of their difference. It is the identity case of cutDist_le_cutNorm_sub_of_measurePreserving, realised by the diagonal coupling.

The reverse inequality is false: two graphons that differ by a measure-preserving rearrangement of the carrier are at cut distance zero while their difference can have cut norm bounded away from zero.

@[simp]

theorem TauCeti.DenseGraphLimits.cutNorm_overlayDiff_diagonalCoupling {Ω : Type u_3} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (U W : Graphon Ω μ) : cutNorm (MeasureTheory.diagonalCoupling μ) (overlayDiff U W (MeasureTheory.diagonalCoupling μ)) = cutNorm μ (U.toSymmKernel - W.toSymmKernel)

The diagonal coupling realises the same-carrier cut norm. Of all the couplings the cut distance takes an infimum over, the diagonal one contributes exactly ‖U - W‖□.

@[simp]

theorem TauCeti.DenseGraphLimits.cutDist_self {Ω : Type u_3} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (U : Graphon Ω μ) : cutDist U U = 0

The cut distance of a graphon to itself is zero.