Step graphons are dense in graphon space #
exists_stepGraphon_cutDist_le approximates a graphon by a step graphon in cut distance. This
file transports that approximation to the metric space GraphonSpace Ω μ, where cut distance is a
genuine metric on the separation quotient: the classes of step graphons on measurable finite
partitions form a dense subset.
Density is stated for an arbitrary carrier, since nothing here inspects it: the approximation is the one supplied by Frieze--Kannan weak regularity, and the passage to the quotient only uses that the distance of two classes is the cut distance of any two representatives.
Main results #
TauCeti.DenseGraphLimits.dense_stepGraphon-- step graphons are dense in graphon space.
References #
- L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), §9.2.
theorem
TauCeti.DenseGraphLimits.dense_stepGraphon
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
:
Dense
{x : GraphonSpace Ω μ | ∃ (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), x = SeparationQuotient.mk (stepGraphon P hP val hsymm)}
Step graphons are dense in graphon space.