The triangle inequality for graphon cut distance

This file proves the triangle inequality for the coupling-primary cut distance on arbitrary probability carriers. The central finite-middle case glues two couplings over a countable intermediate carrier and pulls all three overlaid kernels back to the glued probability space, where their difference telescopes. Exact invariance of the cut norm under measure-preserving pullback then returns the estimate to the original couplings.

For an arbitrary intermediate carrier, Frieze--Kannan weak regularity replaces the middle graphon by a finite step graphon. Its finite set of blocks is the countable middle carrier to which the gluing argument applies, and stability of cut distance under cut-norm approximation removes the replacement error. This avoids imposing standard-Borel or atomlessness hypotheses on any of the three carriers.

The triangle inequality is the last pseudometric law still missing, so this file also equips the strict graphons on a fixed probability carrier with the cut-distance pseudometric.

Main results

• TauCeti.DenseGraphLimits.cutDist_triangle proves the triangle inequality on arbitrary probability carriers.
• TauCeti.DenseGraphLimits.cutDist_congr_left and TauCeti.DenseGraphLimits.cutDist_congr_right say that graphons at cut distance zero have the same cut distance to every graphon.
• TauCeti.DenseGraphLimits.cutDist_comap_right states that reading the right-hand graphon along a measure-preserving map leaves the cut distance unchanged.
• TauCeti.DenseGraphLimits.Graphon.instPseudoMetricSpace is the cut-distance pseudometric on strict graphons over one carrier, and TauCeti.DenseGraphLimits.Graphon.dist_eq_cutDist identifies its distance with cutDist.

References

• S. Janson, Graphons, cut norm and distance, couplings and rearrangements, NYJM Monographs 4 (2013), Lemma 6.5.
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), Section 8.2.
• Roadmap: TauCetiRoadmap/DenseGraphLimits/README.md, Layer 1 — the arbitrary-carrier triangle inequality and the fixed-carrier pseudometric. The cutDist_triangle signature follows TauCetiRoadmap/DenseGraphLimits/Suggested.lean.

theorem TauCeti.DenseGraphLimits.cutDist_triangle {Ω₁ : Type u_1} {Ω₂ : Type u_2} {Ω₃ : Type u_3} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] [MeasurableSpace Ω₃] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} {μ₃ : MeasureTheory.Measure Ω₃} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] [MeasureTheory.IsProbabilityMeasure μ₃] (U : Graphon Ω₁ μ₁) (W : Graphon Ω₂ μ₂) (X : Graphon Ω₃ μ₃) : cutDist U X ≤ cutDist U W + cutDist W X

The coupling-primary graphon cut distance satisfies the triangle inequality on arbitrary probability carriers.

theorem TauCeti.DenseGraphLimits.cutDist_congr_left {Ω₁ : Type u_1} {Ω₂ : Type u_2} {Ω₃ : Type u_3} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] [MeasurableSpace Ω₃] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} {μ₃ : MeasureTheory.Measure Ω₃} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] [MeasureTheory.IsProbabilityMeasure μ₃] {U : Graphon Ω₁ μ₁} {U' : Graphon Ω₂ μ₂} (h : cutDist U U' = 0) (W : Graphon Ω₃ μ₃) : cutDist U W = cutDist U' W

The cut distance factors through vanishing cut distance in its left argument: two graphons at cut distance zero, on arbitrary probability carriers, are at the same cut distance from every graphon. This is the zero-distance analogue of cutDist_congr_ae_left.

theorem TauCeti.DenseGraphLimits.cutDist_congr_right {Ω₁ : Type u_1} {Ω₂ : Type u_2} {Ω₃ : Type u_3} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] [MeasurableSpace Ω₃] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} {μ₃ : MeasureTheory.Measure Ω₃} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] [MeasureTheory.IsProbabilityMeasure μ₃] {W : Graphon Ω₂ μ₂} {W' : Graphon Ω₃ μ₃} (h : cutDist W W' = 0) (U : Graphon Ω₁ μ₁) : cutDist U W = cutDist U W'

The cut distance factors through vanishing cut distance in its right argument: every graphon is at the same cut distance from two graphons at cut distance zero, on arbitrary probability carriers. This is the zero-distance analogue of cutDist_congr_ae_right.

theorem TauCeti.DenseGraphLimits.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.comap f ⋯ μ₂') = cutDist U W

Reading the right-hand graphon along a measure-preserving map f : Ω₂' → Ω₂ leaves the cut distance unchanged: cutDist U (W.comap f hf.measurable μ₂') = cutDist U W.

Together with cutDist_comm this says that the cut distance only depends on a graphon through its measure-preserving pullbacks, on arbitrary probability carriers; the inequality ≥ alone is cutDist_le_cutDist_comap_right, and needs no triangle inequality.

@[instance_reducible]

noncomputable instance TauCeti.DenseGraphLimits.Graphon.instPseudoMetricSpace {Ω : Type u_4} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] : PseudoMetricSpace (Graphon Ω μ)

The coupling cut distance gives strict graphons on one probability carrier a pseudometric.

Distinct strict representatives can have distance zero, for example after a measure-preserving rearrangement, so this is intentionally not a MetricSpace.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.DenseGraphLimits.Graphon.dist_eq_cutDist {Ω : Type u_4} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (U W : Graphon Ω μ) : dist U W = cutDist U W

The distance between strict graphons on one carrier is their coupling cut distance.