Limits of L¹-Cauchy graphon sequences

A sequence of graphons whose kernels have an L¹ Cauchy modulus tending to zero converges in cut distance to a graphon. A summably fast subsequence and Mathlib's completeness machinery for eLpNorm produce an almost-everywhere pointwise limit. The pointwise limit remains symmetric and [0, 1]-valued, so exists_graphon_repr turns its almost-everywhere class back into a strict graphon. Finally, the cut norm is bounded by the L¹ norm.

This form is designed for graphon compactness arguments: after representatives of a Cauchy subsequence have been realigned, this result supplies the limiting strict graphon.

Main results

• TauCeti.DenseGraphLimits.exists_graphon_tendsto_eLpNorm_of_tendsto_eLpNorm_bound constructs a strict graphon L¹ limit from an L¹ Cauchy modulus tending to zero.
• TauCeti.DenseGraphLimits.cutDist_le_eLpNorm_one_toReal bounds cut distance by L¹ distance.
• TauCeti.DenseGraphLimits.exists_graphon_tendsto_cutDist_of_tendsto_eLpNorm_bound is the resulting cut-distance convergence.

References

• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), §9.3.
• L. Lovász and B. Szegedy, Szemerédi's Lemma for the Analyst, GAFA 17 (2007), §5.

theorem TauCeti.DenseGraphLimits.exists_graphon_tendsto_eLpNorm_of_tendsto_eLpNorm_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : ℕ → Graphon Ω μ) {B : ℕ → ENNReal} (hB : Filter.Tendsto B Filter.atTop (nhds 0)) (hCauchy : ∀ (N n m : ℕ), N ≤ n → N ≤ m → MeasureTheory.eLpNorm ((fun (z : Ω × Ω) => (W n) z.1 z.2) - fun (z : Ω × Ω) => (W m) z.1 z.2) 1 (μ.prod μ) ≤ B N) : ∃ (Wlim : Graphon Ω μ), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm ((fun (z : Ω × Ω) => (W n) z.1 z.2) - fun (z : Ω × Ω) => Wlim z.1 z.2) 1 (μ.prod μ)) Filter.atTop (nhds 0)

A graphon sequence with an L¹ Cauchy modulus tending to zero has a strict graphon limit in L¹.

The bound B N controls every pair of terms whose indices are at least N. A summably fast subsequence gives an almost-everywhere pointwise limit through Mathlib's Lp completeness machinery; the closed conditions of symmetry and range [0, 1] pass to that limit.

theorem TauCeti.DenseGraphLimits.cutDist_le_eLpNorm_one_toReal {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (U W : Graphon Ω μ) : cutDist U W ≤ (MeasureTheory.eLpNorm ((fun (z : Ω × Ω) => U z.1 z.2) - fun (z : Ω × Ω) => W z.1 z.2) 1 (μ.prod μ)).toReal

The cut distance between two graphons on the same probability space is bounded by the real L¹ seminorm of the difference of their uncurried functions.

theorem TauCeti.DenseGraphLimits.exists_graphon_tendsto_cutDist_of_tendsto_eLpNorm_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : ℕ → Graphon Ω μ) {B : ℕ → ENNReal} (hB : Filter.Tendsto B Filter.atTop (nhds 0)) (hCauchy : ∀ (N n m : ℕ), N ≤ n → N ≤ m → MeasureTheory.eLpNorm ((fun (z : Ω × Ω) => (W n) z.1 z.2) - fun (z : Ω × Ω) => (W m) z.1 z.2) 1 (μ.prod μ) ≤ B N) : ∃ (Wlim : Graphon Ω μ), Filter.Tendsto (fun (n : ℕ) => cutDist (W n) Wlim) Filter.atTop (nhds 0)

A graphon sequence with an L¹ Cauchy modulus tending to zero converges in cut distance to a strict graphon. This is the cut-distance consequence of exists_graphon_tendsto_eLpNorm_of_tendsto_eLpNorm_bound.