Frieze--Kannan weak regularity for graphons

This file proves the weak regularity lemma for strict graphons. Starting from the indiscrete finite partition, a cut-norm witness for the current block-average defect cuts every part along two measurable sets. The common refinement has at most four times as many parts, while the Pythagoras identity for graphonPartitionEnergy and Cauchy--Schwarz show that its energy rises by strictly more than ε². Since the energy stays in [0, 1], the process stops after at most ⌈1 / ε²⌉ steps.

Null parts need no special case: Finpartition.bipartition omits empty sets but retains nonempty null sets, and stepGraphonAvg uses Mathlib's zero set-average convention on their rectangles.

Main results

• TauCeti.DenseGraphLimits.exists_refinement_energy_add_sq_lt is the quantitative refinement step: a bad cut-norm approximation yields an energy gain of more than ε² while multiplying the number of parts by at most four;
• TauCeti.DenseGraphLimits.exists_partition_cutNorm_le_or_energy_add_mul_sq_lt is the refinement invariant for iteration from an arbitrary measurable partition;
• TauCeti.DenseGraphLimits.weak_regularity_frieze_kannan is the weak regularity theorem, with complexity 4 ^ (Nat.ceil (1 / ε ^ 2)).

References

• A. Frieze and R. Kannan, Quick approximation to matrices and applications, Combinatorica 19 (1999), 175--220.
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), §9.2.
• The refinement-and-energy iteration follows Graphon/Regularity.lean in cameronfreer/graphon (Apache 2.0) at commit 6eccca5bbe5c9df46d7129bf59575b8b9b1d6699, adapted here to Mathlib Finpartition, strict block-average graphons, and the Pythagoras energy API. The iteration count differs from that route's ⌈1 / ε²⌉ + 1: there the energy gain of a bad step is only ≥ ε², while here the cut-norm witness is squared strictly, so the gain is > ε² and ⌈1 / ε²⌉ steps already contradict the energy bound.

theorem TauCeti.DenseGraphLimits.exists_refinement_energy_add_sq_lt {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (P : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p) (W : Graphon Ω μ) {ε : ℝ} (hε : 0 ≤ ε) (hbad : ε < cutNorm μ (W.toSymmKernel - (stepGraphonAvg P hP W).toSymmKernel)) : ∃ (Q : Finpartition Set.univ) (hQ : ∀ q ∈ Q.parts, MeasurableSet q), Q ≤ P ∧ Q.parts.card ≤ 4 * P.parts.card ∧ graphonPartitionEnergy μ P hP W + ε ^ 2 < graphonPartitionEnergy μ Q hQ W

A cut-norm defect larger than ε produces a measurable common refinement with at most four times as many parts and graphon partition energy more than ε² larger.

theorem TauCeti.DenseGraphLimits.exists_partition_cutNorm_le_or_energy_add_mul_sq_lt {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) {ε : ℝ} (hε : 0 ≤ ε) (n : ℕ) (P : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p) : ∃ (Q : Finpartition Set.univ) (hQ : ∀ q ∈ Q.parts, MeasurableSet q), Q ≤ P ∧ Q.parts.card ≤ 4 ^ (n + 1) * P.parts.card ∧ (cutNorm μ (W.toSymmKernel - (stepGraphonAvg Q hQ W).toSymmKernel) ≤ ε ∨ graphonPartitionEnergy μ P hP W + ↑(n + 1) * ε ^ 2 < graphonPartitionEnergy μ Q hQ W)

Iteration invariant. Given a measurable partition P and n + 1 refinement steps, there is a measurable refinement with at most 4 ^ (n + 1) times as many parts whose block averages either approximate W to within ε in cut norm, or — when every one of those steps was actually taken — carry energy strictly more than (n + 1) * ε ^ 2 above P's.

theorem TauCeti.DenseGraphLimits.weak_regularity_frieze_kannan {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) {ε : ℝ} (hε : 0 < ε) : ∃ (P : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p), P.parts.card ≤ 4 ^ ⌈1 / ε ^ 2⌉₊ ∧ cutNorm μ (W.toSymmKernel - (stepGraphonAvg P hP W).toSymmKernel) ≤ ε

Frieze--Kannan weak regularity. Every graphon has a measurable block-average step graphon within ε in cut norm, on a partition with at most 4 ^ ⌈1 / ε²⌉ parts.