Finite Frieze–Kannan weak regularity

Every finite graph G on V has a partition P of its vertices into at most 4 ^ ⌈1 / ε²⌉ parts whose stepped prediction is within ε * (card V) ^ 2 of the true number of edges on every rectangle, that is, whose cut discrepancy G.cutDiscrepancy P is at most ε * (card V) ^ 2 (SimpleGraph.frieze_kannan). The bound on the number of parts does not depend on G or on card V.

The proof is an energy increment argument for the size-weighted energy SimpleGraph.weightedEnergy.

• A refinement whose energy gap is at most ε changes every stepped prediction by at most √ε * (card V) ^ 2 (SimpleGraph.abs_steppedCount_sub_steppedCount_le). This is the absolute-deviation bound SimpleGraph.weightedDensityDeviation_abs_le, summed against the trace masses of the rectangle.
• If P has a rectangle (A, B) with deviation more than ε * (card V) ^ 2, cutting every part of P along A and B gives a refinement with at most four times as many parts on which the rectangle is predicted exactly. By the first point its energy exceeds that of P by more than ε² (SimpleGraph.exists_refinement_weightedEnergy_add_sq_lt).
• The energy lies in [0, 1], so after ⌈1 / ε²⌉ refinement steps the cut discrepancy is small. Starting from an arbitrary partition gives the refining form SimpleGraph.frieze_kannan_refining.

The argument is finite and self-contained: it does not pass through graphons or the analytic cut norm.

Main results

• SimpleGraph.abs_steppedCount_sub_steppedCount_le: an energy gap bounds the change of the stepped predictions.
• SimpleGraph.exists_refinement_weightedEnergy_add_sq_lt: the energy increment step.
• SimpleGraph.frieze_kannan_refining: weak regularity refining a given partition.
• SimpleGraph.frieze_kannan and SimpleGraph.frieze_kannan_cutDiscrepancy: the finite Frieze–Kannan theorem, in rectangle form and in cut discrepancy form.

References

• A. Frieze, R. Kannan, Quick approximation to matrices and applications, Combinatorica 19 (1999).
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), §9.2.
• The increment step and its iteration follow the graphon form of the theorem, TauCeti.DenseGraphLimits.exists_refinement_energy_add_sq_lt and TauCeti.DenseGraphLimits.weak_regularity_frieze_kannan, with Tau Ceti's finite size-weighted energy in place of the graphon partition energy.
• The theorem names follow RegularityLemmata/Graph/FriezeKannan.lean in cameronfreer/regularity-lemmata at commit 315ef979f55f31cc43cd791302519d9a34cc2dc0, where frieze_kannan, frieze_kannan_refining and frieze_kannan_cutDiscrepancy are stated for directed relations.

theorem SimpleGraph.abs_steppedCount_sub_steppedCount_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {P Q : Finpartition Finset.univ} (h : Q ≤ P) {ε : ℝ} (hgap : G.weightedEnergy Q - G.weightedEnergy P ≤ ε) (A B : Finset V) : |G.steppedCount Q A B - G.steppedCount P A B| ≤ √ε * ↑(Fintype.card V) ^ 2

Energy gap controls stepped predictions. If Q refines P and the energy gap G.weightedEnergy Q - G.weightedEnergy P is at most ε, then on every rectangle the stepped predictions of Q and P differ by at most √ε * (card V) ^ 2.

theorem SimpleGraph.exists_refinement_weightedEnergy_add_sq_lt {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) {ε : ℝ} (hε : 0 ≤ ε) (hbad : ε * ↑(Fintype.card V) ^ 2 < G.cutDiscrepancy P) : ∃ Q ≤ P, Q.parts.card ≤ 4 * P.parts.card ∧ G.weightedEnergy P + ε ^ 2 < G.weightedEnergy Q

Energy increment. If the cut discrepancy of P exceeds ε * (card V) ^ 2, then cutting the parts of P along a witnessing rectangle gives a refinement with at most four times as many parts whose energy exceeds that of P by more than ε².

theorem SimpleGraph.frieze_kannan_refining {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P₀ : Finpartition Finset.univ) {ε : ℝ} (hε : 0 < ε) : ∃ P ≤ P₀, P.parts.card ≤ 4 ^ ⌈1 / ε ^ 2⌉₊ * P₀.parts.card ∧ G.cutDiscrepancy P ≤ ε * ↑(Fintype.card V) ^ 2

Frieze–Kannan weak regularity, refining form. For ε > 0, every partition P₀ of the vertices of G is refined by a partition with at most 4 ^ ⌈1 / ε²⌉ times as many parts whose cut discrepancy is at most ε * (card V) ^ 2.

theorem SimpleGraph.frieze_kannan_cutDiscrepancy {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {ε : ℝ} (hε : 0 < ε) : ∃ (P : Finpartition Finset.univ), P.parts.card ≤ 4 ^ ⌈1 / ε ^ 2⌉₊ ∧ G.cutDiscrepancy P ≤ ε * ↑(Fintype.card V) ^ 2

Finite Frieze–Kannan weak regularity, cut discrepancy form. For ε > 0, the vertices of G have a partition into at most 4 ^ ⌈1 / ε²⌉ parts whose cut discrepancy is at most ε * (card V) ^ 2.

theorem SimpleGraph.frieze_kannan {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {ε : ℝ} (hε : 0 < ε) : ∃ (P : Finpartition Finset.univ), P.parts.card ≤ 4 ^ ⌈1 / ε ^ 2⌉₊ ∧ ∀ (A B : Finset V), |↑(G.interedges A B).card - G.steppedCount P A B| ≤ ε * ↑(Fintype.card V) ^ 2

Finite Frieze–Kannan weak regularity. For ε > 0, the vertices of G have a partition P into at most 4 ^ ⌈1 / ε²⌉ parts such that, for all vertex sets A and B, the number of edges from A to B is within ε * (card V) ^ 2 of its stepped prediction G.steppedCount P A B.