Completeness of unit-interval graphons

Strict graphons on the unit interval form a complete pseudometric space for the cut distance. The realignment theorem below also makes a sequence of graphons with controlled consecutive cut distances available on a common carrier with the same cut-norm control.

Main results

• TauCeti.DenseGraphLimits.exists_isProbabilityMeasure_cutNorm_comap_sub_lt -- realigns a sequence of graphons onto one path-space carrier;
• TauCeti.DenseGraphLimits.Graphon.instCompleteSpaceUnitInterval -- completeness for the cut-distance pseudometric on unit-interval graphons.

References

• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), Theorem 9.23.
• S. Janson, Graphons, cut norm and distance, couplings and rearrangements, NYJM Monographs 4 (2013), Section 6 (cut distance through couplings).

theorem TauCeti.DenseGraphLimits.exists_isProbabilityMeasure_cutNorm_comap_sub_lt {Ω : Type u_1} [MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : ℕ → Graphon Ω μ) {ε : ℕ → ℝ} (hW : ∀ (n : ℕ), cutDist (W n) (W (n + 1)) < ε n) : ∃ (P : MeasureTheory.Measure (ℕ → Ω)) (x : MeasureTheory.IsProbabilityMeasure P), (∀ (n : ℕ), MeasureTheory.MeasurePreserving (fun (x : ℕ → Ω) => x n) P μ) ∧ ∀ (n : ℕ), cutNorm P ((W n).comap (fun (x : ℕ → Ω) => x n) ⋯ P - (W (n + 1)).comap (fun (x : ℕ → Ω) => x (n + 1)) ⋯ P) < ε n

Realignment of a sequence of graphons on one carrier. If consecutive terms of a sequence of graphons on a standard Borel carrier are within cut distance ε n, then there is a probability measure P on the path space ℕ → Ω, whose every coordinate projection is measure preserving onto μ, along which the pulled-back terms are consecutively within ε n in cut norm.

Each pulled-back term is at cut distance zero from the original one (cutDist_comap_right), so the sequence is unchanged up to cut distance, but now lives on one carrier, where the cut norm of a difference is available.

instance TauCeti.DenseGraphLimits.Graphon.instCompleteSpaceUnitInterval : CompleteSpace (Graphon (↑unitInterval) MeasureTheory.volume)

Completeness of unit-interval graphons. Every Cauchy sequence of strict graphons on the unit interval converges in cut distance to a strict unit-interval graphon.