Every graphon space embeds isometrically in the unit-interval graphon space

Every graphon on an arbitrary probability carrier is at cut distance zero from a graphon on (I, volume) (exists_graphon_unitInterval_cutDist_eq_zero, Janson, Theorem 7.1). This file fixes such a unit-interval representative for each strict graphon and descends the assignment to the cut-distance quotients: the resulting map toGraphonSpaceI : GraphonSpace Ω μ → GraphonSpaceI is an isometry, and it is the identity on GraphonSpaceI itself.

The embedding is the bridge from the canonical carrier back to arbitrary fixed carriers: every fixed-carrier graphon space is isometric to a subspace of the canonical one, so the metric properties of GraphonSpaceI that pass to subspaces -- total boundedness in the first place -- hold on every fixed-carrier graphon space. The embedding also preserves homomorphism densities; see homDensityOnSpace_toGraphonSpaceI in GraphonSpace/HomDensity.lean.

Over an atomless standard Borel carrier the embedding is onto: such a carrier maps measure-preservingly onto (I, volume) (MeasureTheory.Measure.exists_measurePreserving_of_nullSingleton), so every graphon, on any carrier, is at cut distance zero from a graphon on it. The graphon space over such a carrier is then isometric to the unit-interval graphon space, and every metric property of GraphonSpaceI -- compactness in the first place -- transfers to it.

Main definitions

• TauCeti.DenseGraphLimits.Graphon.unitIntervalRepr -- a unit-interval graphon at cut distance zero from a given graphon on an arbitrary probability carrier;
• TauCeti.DenseGraphLimits.toGraphonSpaceI -- the induced map on graphon spaces;
• TauCeti.DenseGraphLimits.isometryEquivGraphonSpaceI -- over an atomless standard Borel carrier, the induced map as an isometry equivalence.

Main results

• TauCeti.DenseGraphLimits.Graphon.cutDist_unitIntervalRepr_left and TauCeti.DenseGraphLimits.Graphon.cutDist_unitIntervalRepr_right -- the representative has the same cut distance to every graphon as the original;
• TauCeti.DenseGraphLimits.Graphon.isometry_unitIntervalRepr -- taking representatives is an isometry of strict graphons;
• TauCeti.DenseGraphLimits.isometry_toGraphonSpaceI -- the induced map is an isometry;
• TauCeti.DenseGraphLimits.toGraphonSpaceI_eq_self -- on the unit-interval graphon space the induced map is the identity;
• TauCeti.DenseGraphLimits.exists_graphon_cutDist_eq_zero -- every graphon is at cut distance zero from a graphon on a given atomless standard Borel carrier;
• TauCeti.DenseGraphLimits.toGraphonSpaceI_surjective -- over an atomless standard Borel carrier the induced map is onto.

References

• S. Janson, Graphons, cut norm and distance, couplings and rearrangements, NYJM Monographs 4 (2013), Theorem 7.1 and Theorem A.7.

noncomputable def TauCeti.DenseGraphLimits.Graphon.unitIntervalRepr {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : Graphon (↑unitInterval) MeasureTheory.volume

A graphon on the unit interval at cut distance zero from W, for W on an arbitrary probability carrier.

The representative is an arbitrary choice; cutDist_unitIntervalRepr_left and cutDist_unitIntervalRepr_right show that no cut distance depends on it.

Equations

• W.unitIntervalRepr = ⋯.choose

theorem TauCeti.DenseGraphLimits.Graphon.cutDist_unitIntervalRepr {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : cutDist W W.unitIntervalRepr = 0

The unit-interval representative is at cut distance zero from the graphon it represents.

@[simp]

theorem TauCeti.DenseGraphLimits.Graphon.cutDist_unitIntervalRepr_left {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω} {μ' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] (W : Graphon Ω μ) (X : Graphon Ω' μ') : cutDist W.unitIntervalRepr X = cutDist W X

The unit-interval representative has the same cut distance to every graphon as the original graphon.

@[simp]

theorem TauCeti.DenseGraphLimits.Graphon.cutDist_unitIntervalRepr_right {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω} {μ' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] (X : Graphon Ω' μ') (W : Graphon Ω μ) : cutDist X W.unitIntervalRepr = cutDist X W

Every graphon has the same cut distance to the unit-interval representative as to the original graphon.

theorem TauCeti.DenseGraphLimits.Graphon.isometry_unitIntervalRepr {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] : Isometry unitIntervalRepr

Taking unit-interval representatives is an isometry for the cut-distance pseudometrics on strict graphons.

noncomputable def TauCeti.DenseGraphLimits.toGraphonSpaceI {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] : GraphonSpace Ω μ → GraphonSpaceI

The map from the graphon space over an arbitrary probability carrier to the unit-interval graphon space, sending the class of a graphon to the class of its unit-interval representative: the descent of the isometry Graphon.unitIntervalRepr to the cut-distance quotients.

It is an isometry (isometry_toGraphonSpaceI).

Equations

• TauCeti.DenseGraphLimits.toGraphonSpaceI = SeparationQuotient.map TauCeti.DenseGraphLimits.Graphon.unitIntervalRepr

@[simp]

theorem TauCeti.DenseGraphLimits.toGraphonSpaceI_mk {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : toGraphonSpaceI (SeparationQuotient.mk W) = SeparationQuotient.mk W.unitIntervalRepr

The embedding sends the class of a graphon to the class of its unit-interval representative.

theorem TauCeti.DenseGraphLimits.isometry_toGraphonSpaceI {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] : Isometry toGraphonSpaceI

Every graphon space embeds isometrically in the unit-interval graphon space.

@[simp]

theorem TauCeti.DenseGraphLimits.toGraphonSpaceI_eq_self (x : GraphonSpaceI) : toGraphonSpaceI x = x

On the unit-interval graphon space the embedding is the identity.

theorem TauCeti.DenseGraphLimits.exists_graphon_cutDist_eq_zero {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] (μ : MeasureTheory.Measure Ω) {μ' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] [StandardBorelSpace Ω] [MeasureTheory.NullSingletonClass μ] (V : Graphon Ω' μ') : ∃ (W : Graphon Ω μ), cutDist V W = 0

Every graphon is represented on every atomless standard Borel carrier: a graphon on an arbitrary probability carrier is at cut distance zero from a graphon on (Ω, μ) whenever Ω is standard Borel and μ has no atoms.

This generalizes exists_graphon_unitInterval_cutDist_eq_zero, which represents every graphon on the particular atomless carrier (I, volume), to every atomless standard Borel carrier.

theorem TauCeti.DenseGraphLimits.toGraphonSpaceI_surjective {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace Ω] [MeasureTheory.NullSingletonClass μ] : Function.Surjective toGraphonSpaceI

Over an atomless standard Borel carrier the embedding into the unit-interval graphon space is onto.

noncomputable def TauCeti.DenseGraphLimits.isometryEquivGraphonSpaceI {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace Ω] [MeasureTheory.NullSingletonClass μ] : GraphonSpace Ω μ ≃ᵢ GraphonSpaceI

The graphon space over an atomless standard Borel carrier is isometric to the unit-interval graphon space, through the embedding toGraphonSpaceI.

Equations

• TauCeti.DenseGraphLimits.isometryEquivGraphonSpaceI = { toEquiv := Equiv.ofBijective TauCeti.DenseGraphLimits.toGraphonSpaceI ⋯, isometry_toFun := ⋯ }

@[simp]

theorem TauCeti.DenseGraphLimits.coe_isometryEquivGraphonSpaceI {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace Ω] [MeasureTheory.NullSingletonClass μ] : ⇑isometryEquivGraphonSpaceI = toGraphonSpaceI

The isometry equivalence acts as the embedding toGraphonSpaceI.

@[simp]

theorem TauCeti.DenseGraphLimits.isometryEquivGraphonSpaceI_symm_mk_eq_mk_iff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace Ω] [MeasureTheory.NullSingletonClass μ] (V : Graphon (↑unitInterval) MeasureTheory.volume) (W : Graphon Ω μ) : isometryEquivGraphonSpaceI.symm (SeparationQuotient.mk V) = SeparationQuotient.mk W ↔ cutDist V W = 0

The inverse isometry sends the class of a unit-interval graphon V to the class of any graphon on (Ω, μ) at cut distance zero from V.