The graphon space: compact metric quotient of graphons under weak isomorphism (issue #23)

Packages the proved pseudometric theory of cutDistance into a bundled state space (route vetted 2026-07-10):

• a PseudoMetricSpace instance on raw Graphon α μ with dist = cutDistance (the triangle inequality fixes the instance boundary at [StandardBorelSpace α] [NullSingletonClass μ]);
• GraphonSpace α μ := SeparationQuotient (Graphon α μ) — Mathlib's metric separation quotient, NOT a hand-rolled Quotient: the MetricSpace, CompleteSpace, and Nonempty instances come for free, and quotient equality is exactly WeaklyIsomorphic (GraphonSpace.mk_eq_mk_iff);
• CompactSpace (GraphonSpace α μ): total boundedness transfers through the uniformly continuous surjective quotient map (Graphon.totallyBounded is called at ε / 2 because it produces closed-ball nets while Metric.totallyBounded_iff wants open balls) and combines with the transferred completeness;
• the canonical Borel measurable space on the quotient, giving BorelSpace, SecondCountableTopology, PolishSpace, and StandardBorelSpace — the right home for graphon-valued laws. (Raw Graphon α μ deliberately receives NO measurable structure: the quotient is the object that carries random graphons.)
• StandardGraphonSpace — the fixed unit-interval alias for probability-facing APIs, so downstream theorems need not carry base-space typeclasses.

Deferred explicitly (separate campaigns): isometry/transport between quotients over different atomless standard bases (a MeasureIso application), measurable selectors.

@[implicit_reducible]

noncomputable instance Graphon.instPseudoMetricSpace {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] : PseudoMetricSpace (Graphon α μ)

The cut distance as a pseudometric on raw graphons. Not a metric: distance zero is weak isomorphism, not equality — hence the SeparationQuotient below.

Equations

• Graphon.instPseudoMetricSpace = { dist := Graphon.cutDistance, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯, uniformity_dist := ⋯, cobounded_sets := ⋯ }

instance Graphon.instCompleteSpace {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] : CompleteSpace (Graphon α μ)

Raw graphon space is complete: the metric Cauchy predicate is the project's sequential IsCauchy, discharged by the proved complete.

theorem Graphon.totallyBounded_univ {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] : TotallyBounded Set.univ

Raw graphon space is totally bounded (from the proved finite-net theorem, invoked at half radius to convert closed-ball nets into open balls).

@[reducible, inline]

abbrev GraphonSpace (α : Type u_1) [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] : Type u_1

The graphon space: the metric separation quotient of Graphon α μ under cut distance — equivalently, graphons modulo weak isomorphism — as a compact Polish standard-Borel metric space.

Equations

• GraphonSpace α μ = SeparationQuotient (Graphon α μ)

noncomputable def GraphonSpace.mk {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) : GraphonSpace α μ

The class of a graphon in the graphon space.

Equations

• GraphonSpace.mk W = SeparationQuotient.mk W

@[simp]

theorem GraphonSpace.dist_mk {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (U W : Graphon α μ) : dist (mk U) (mk W) = U.cutDistance W

@[simp]

theorem GraphonSpace.mk_eq_mk_iff {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (U W : Graphon α μ) : mk U = mk W ↔ U.WeaklyIsomorphic W

Quotient equality is weak isomorphism: two graphons have the same class iff they are weakly isomorphic (cut distance zero).

theorem GraphonSpace.surjective_mk {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] : Function.Surjective mk

theorem GraphonSpace.uniformContinuous_mk {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] : UniformContinuous mk

theorem GraphonSpace.continuous_mk {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] : Continuous mk

theorem GraphonSpace.totallyBounded_univ {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] : TotallyBounded Set.univ

instance GraphonSpace.instCompactSpace {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] : CompactSpace (GraphonSpace α μ)

Compactness of the graphon space (Lovász–Szegedy): complete + totally bounded.

@[implicit_reducible]

noncomputable instance GraphonSpace.instMeasurableSpace {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] : MeasurableSpace (GraphonSpace α μ)

The canonical Borel measurable structure on the graphon space — the state space for graphon-valued random elements.

Equations

• GraphonSpace.instMeasurableSpace = borel (GraphonSpace α μ)

instance GraphonSpace.instBorelSpace {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] : BorelSpace (GraphonSpace α μ)

@[reducible, inline]

abbrev StandardGraphonSpace : Type

The standard graphon space, over the unit interval with Lebesgue measure: the canonical fixed-domain state space for probability measures on graphons (downstream probability APIs need not carry base-space typeclasses). Base-independence — isometry with GraphonSpace α μ over any atomless standard Borel probability base — is a deferred MeasureIso application.

Equations

• StandardGraphonSpace = GraphonSpace (↑unitInterval) MeasureTheory.volume