Approximating a graphon by a finite weighted graph

Frieze--Kannan weak regularity approximates a graphon in cut norm by the block averages of a measurable finite partition. This file turns that into an approximation in cut distance by a finite object: the block matrix of the approximating step graphon, read as a graphon on the discrete probability space of its blocks.

The cut distance never increases along a measure-preserving pullback (cutDist_comap_right), and a step graphon is the pullback of its block matrix along the part-index map, so a step graphon and its finite matrix are at cut distance zero. Step graphons are therefore dense in the cut metric, and so are finite weighted graphs on a vertex set whose size depends only on the accuracy. Rounding the two weightings of such a finite weighted graph onto a grid, so that finitely many candidates remain, is TauCeti.Combinatorics.DenseGraphLimits.CutMetric.OfMatrixGrid.

Main results

• TauCeti.DenseGraphLimits.exists_stepGraphon_cutDist_le -- every graphon is within ε in cut distance of a step graphon on a measurable finite partition with at most 4 ^ ⌈1/ε²⌉ parts;
• TauCeti.DenseGraphLimits.exists_ofMatrix_cutDist_le -- every graphon is within ε in cut distance of a finite weighted graph on any vertex set of size at least 4 ^ ⌈1/ε²⌉.

References

• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), §9.2 -- weighted graphs are dense in the space of graphons.

theorem TauCeti.DenseGraphLimits.exists_stepGraphon_cutDist_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) {ε : ℝ} (hε : 0 < ε) : ∃ (P : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p) (val : ↥P.parts → ↥P.parts → ↑(Set.Icc 0 1)) (hsymm : ∀ (p q : ↥P.parts), val p q = val q p), P.parts.card ≤ 4 ^ ⌈1 / ε ^ 2⌉₊ ∧ cutDist W (stepGraphon P hP val hsymm) ≤ ε

Step graphons are dense in the cut metric, with the Frieze--Kannan part count: every graphon is within ε in cut distance of a step graphon on a measurable finite partition with at most 4 ^ (⌈1 / ε²⌉) parts.

theorem TauCeti.DenseGraphLimits.exists_ofMatrix_cutDist_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) {ε : ℝ} (hε : 0 < ε) {n : ℕ} (hn : 4 ^ ⌈1 / ε ^ 2⌉₊ ≤ n) : ∃ (g : Ω → Fin n) (_ : Measurable g) (b : Fin n → Fin n → ↑(Set.Icc 0 1)) (hb : ∀ (i j : Fin n), b i j = b j i), cutDist W (Graphon.ofMatrix (MeasureTheory.Measure.map g μ) b hb) ≤ ε

Every graphon is within ε in cut distance of a finite weighted graph, on any vertex set of size at least the Frieze--Kannan bound 4 ^ (⌈1 / ε²⌉): the block matrix of a Frieze--Kannan approximation, carrying the block measures as vertex weights.

The vertex weights are the pushforward of μ along the block-index map g, so they are the measures of the blocks; vertices beyond the blocks carry weight zero. Allowing any large enough vertex set, rather than exactly the number of blocks, keeps the carrier of the approximation independent of the graphon.