The metric space of graphons #

The coupling cut distance is a pseudometric on graphons over a fixed probability carrier. This file forms the separation quotient of that pseudometric, identifying two representatives exactly when their cut distance is zero. The quotient carries the resulting genuine metric.

The quotient is fixed-carrier: GraphonSpace Ω μ contains graphons on (Ω, μ). Graphons on different carriers are still compared by the cross-carrier cutDist; they are not bundled into a single universe-level quotient. The abbreviation GraphonSpaceI names the canonical quotient on the unit interval.

Two graphons at cut distance zero — for instance a graphon and any measure-preserving rearrangement of it — are topologically indistinguishable in the cut-metric topology, so the identification that turns the pseudometric into a metric is exactly the separation quotient of the strict graphon type.

Main definitions #

TauCeti.DenseGraphLimits.GraphonSpace is the corresponding fixed-carrier quotient;
TauCeti.DenseGraphLimits.GraphonSpaceI is the quotient over the unit interval;
graphon space carries the Borel σ-algebra of the cut metric, so probability measures on it — the mixing measures of exchangeable graph laws — are available.

Main results #

TauCeti.DenseGraphLimits.dist_graphonSpace_mk_mk computes the quotient distance on representatives;
TauCeti.DenseGraphLimits.graphonSpace_mk_eq_mk_iff characterises equality of representatives.

References #

S. Janson, Graphons, cut norm and distance, couplings and rearrangements, NYJM Monographs 4 (2013), Section 6.
L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), Section 8.2.
Roadmap: TauCetiRoadmap/DenseGraphLimits/README.md, Layer 1 — the fixed-carrier GraphonSpace metric quotient and GraphonSpaceI. The signatures follow TauCetiRoadmap/DenseGraphLimits/Suggested.lean.

source

@[reducible, inline]

abbrev TauCeti.DenseGraphLimits.GraphonSpace (Ω : Type u_2) [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] :

Type u_2

The fixed-carrier graphon space: strict graphons modulo vanishing cut distance.

Equations

TauCeti.DenseGraphLimits.GraphonSpace Ω μ = SeparationQuotient (TauCeti.DenseGraphLimits.Graphon Ω μ)

Instances For

source

@[simp]

theorem TauCeti.DenseGraphLimits.dist_graphonSpace_mk_mk {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (U W : Graphon Ω μ) :

dist (SeparationQuotient.mk U) (SeparationQuotient.mk W) = cutDist U W

The graphon-space distance between representatives is their coupling cut distance.

source

@[simp]

theorem TauCeti.DenseGraphLimits.graphonSpace_mk_eq_mk_iff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (U W : Graphon Ω μ) :

SeparationQuotient.mk U = SeparationQuotient.mk W ↔ cutDist U W = 0

Two representatives determine the same point of graphon space exactly when their coupling cut distance vanishes.

source

@[instance_reducible]

noncomputable instance TauCeti.DenseGraphLimits.instMeasurableSpaceGraphonSpace {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] :

MeasurableSpace (GraphonSpace Ω μ)

Graphon space carries the Borel σ-algebra of the cut metric, so that probability measures on graphon space — mixing measures over graphon classes — are measures for its topology.

Equations