Convergence of Graphon Sequences

This file establishes the main theorems characterizing convergence of graphon sequences in cut distance, bringing together the counting lemma, inverse counting lemma, and compactness results.

Main results

• Graphon.converges_iff_homDensity — Cut distance convergence ⟺ hom density convergence
• Graphon.exists_convergent_subsequence — Every sequence has a convergent subsequence (compactness)
• Graphon.isCauchy_iff_isConvergent — Cauchy ⟺ convergent

Implementation notes

This file brings together the key results:

• Counting lemma: cut distance bounds → hom density bounds
• Inverse counting lemma: hom density bounds → cut distance bounds
• Compactness: every sequence has convergent subsequence
• Completeness: Cauchy sequences converge

The main theorem is that the following are equivalent for a graphon sequence (Wₙ):

1. (Wₙ) converges in cut distance to some graphon W
2. (t(F, Wₙ)) converges for all finite graphs F
3. (Wₙ) is Cauchy in cut distance

References

• [L. Lovász, Large Networks and Graph Limits][lovasz2012], Chapter 11

Equivalent characterizations of convergence

def Graphon.IsConvergent {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : ℕ → Graphon α μ) : Prop

A sequence of graphons is convergent in cut distance.

Equations

• Graphon.IsConvergent W = ∃ (V : Graphon α μ), ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, (W n).cutDistance V < ε

def Graphon.HasConvergentHomDensities {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : ℕ → Graphon α μ) : Prop

A sequence of graphons has convergent homomorphism densities for all graphs.

Quantifies over graphs on Fin k for all k : ℕ; this is equivalent to quantifying over all finite types since every Fintype embeds into some Fin k.

Equations

• Graphon.HasConvergentHomDensities W = ∀ (k : ℕ) (F : SimpleGraph (Fin k)) [inst : DecidableRel F.Adj], ∃ (L : ℝ), ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, |Graphon.homDensity F (W n) - L| < ε

theorem Graphon.converges_iff_homDensity {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NoAtoms μ] (W : ℕ → Graphon α μ) : IsConvergent W ↔ HasConvergentHomDensities W

Main theorem: cut distance convergence is equivalent to homomorphism density convergence.

A sequence of graphons converges in cut distance if and only if all homomorphism densities converge.

theorem Graphon.IsConvergent.isCauchy {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] (W : ℕ → Graphon α μ) (h : IsConvergent W) : IsCauchy W

Convergent sequences are Cauchy.

theorem Graphon.IsCauchy.isConvergent {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] (W : ℕ → Graphon α μ) (h : IsCauchy W) : IsConvergent W

Cauchy sequences are convergent (completeness).

theorem Graphon.isCauchy_iff_isConvergent {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] (W : ℕ → Graphon α μ) : IsCauchy W ↔ IsConvergent W

Cauchy ⟺ Convergent (on standard Borel spaces).

Compactness characterization

theorem Graphon.exists_convergent_subsequence {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] (W : ℕ → Graphon α μ) : ∃ (V : Graphon α μ) (φ : ℕ → ℕ), StrictMono φ ∧ ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, (W (φ n)).cutDistance V < ε

Every sequence has a convergent subsequence (sequential compactness).

theorem Graphon.limit_unique {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] (W : ℕ → Graphon α μ) (U V : Graphon α μ) (hU : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, (W n).cutDistance U < ε) (hV : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, (W n).cutDistance V < ε) : U.WeaklyIsomorphic V

The limit of a convergent sequence is unique up to weak isomorphism.

Summary theorems

theorem Graphon.graphLimit_characterization {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NoAtoms μ] (W : ℕ → Graphon α μ) : (IsConvergent W ↔ HasConvergentHomDensities W) ∧ (IsConvergent W ↔ IsCauchy W) ∧ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ IsConvergent (W ∘ φ)

Main Theorem: Characterization of graph limit convergence.

The following are equivalent:

1. Cut distance convergence to some graphon W
2. All homomorphism densities converge
3. The sequence is Cauchy in cut distance

Moreover, any convergent sequence has a unique limit up to weak isomorphism, and every sequence has a convergent subsequence.

Hypothesis: Requires [StandardBorelSpace α] for the Cauchy ↔ Convergent equivalence.