Stepped counts and the cut discrepancy of a partition

A finite partition P of the vertices of a graph G determines the P-stepped graph: the weighted graph whose weight on a pair of vertices is the edge density of G between their parts. Its number of edges between two vertex sets A and B, G.steppedCount P A B, is the count of edges from A to B that the partition predicts: each pair of parts (C, D) contributes its edge density times the trace masses #(A ∩ C) * #(B ∩ D).

The cut discrepancy G.cutDiscrepancy P is the largest deviation, over all rectangles (A, B), between the true number of edges #(G.interedges A B) and the stepped prediction. It is count-scaled: it is at most (card V) ^ 2, rather than normalized to lie in [0, 1]. A partition whose cut discrepancy is at most ε * (card V) ^ 2 is a weak regular partition in the sense of Frieze and Kannan.

Densities include the diagonal blocks: a part C is paired with itself, with the density G.edgeDensity C C over #C * #C ordered pairs.

Main declarations

• SimpleGraph.steppedCount G P A B: the number of edges from A to B predicted by P.
• SimpleGraph.steppedCount_eq_card_interedges: the prediction is exact on rectangles whose sides are unions of parts.
• SimpleGraph.steppedCount_eq_sum_edgeDensity_part: the prediction as a sum, over pairs of vertices, of the edge densities between their parts.
• SimpleGraph.steppedCount_eq_sum_refinementParent: the prediction of a coarse partition, written over the parts of a refinement.
• SimpleGraph.cutDiscrepancy G P: the maximum deviation of the prediction from the true count.
• SimpleGraph.cutDiscrepancy_le_iff and SimpleGraph.lt_cutDiscrepancy_iff: bounds on the cut discrepancy are rectangle bounds, and exceeding a bound is witnessed by a rectangle.
• SimpleGraph.cutDiscrepancy_bot: the partition into singletons has cut discrepancy 0.

References

• A. Frieze, R. Kannan, Quick approximation to matrices and applications, Combinatorica 19 (1999).
• The names steppedCount and cutDiscrepancy follow RegularityLemmata/Graph/CutNorm.lean in cameronfreer/regularity-lemmata at commit 315ef979f55f31cc43cd791302519d9a34cc2dc0, where they are stated for directed relations.

The stepped count

noncomputable def SimpleGraph.steppedCount {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (A B : Finset V) : ℝ

The number of edges from A to B predicted by the partition P: the number of edges of the P-stepped graph between A and B. Each pair of parts (C, D) contributes its edge density times the trace masses #(A ∩ C) * #(B ∩ D).

theorem SimpleGraph.steppedCount_def {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (A B : Finset V) : G.steppedCount P A B = ∑ C ∈ P.parts, ∑ D ∈ P.parts, ↑(G.edgeDensity C D) * ↑(A ∩ C).card * ↑(B ∩ D).card

Unfolding lemma for SimpleGraph.steppedCount.

@[simp]

theorem SimpleGraph.steppedCount_empty_left {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (B : Finset V) : G.steppedCount P ∅ B = 0

The prediction on a rectangle with an empty side is 0.

@[simp]

theorem SimpleGraph.steppedCount_empty_right {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (A : Finset V) : G.steppedCount P A ∅ = 0

The prediction on a rectangle with an empty side is 0.

theorem SimpleGraph.steppedCount_comm {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (A B : Finset V) : G.steppedCount P A B = G.steppedCount P B A

The stepped prediction is symmetric, like the edge count it predicts.

theorem SimpleGraph.steppedCount_nonneg {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (A B : Finset V) : 0 ≤ G.steppedCount P A B

The stepped prediction is nonnegative.

theorem SimpleGraph.steppedCount_le_card_mul_card {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (A B : Finset V) : G.steppedCount P A B ≤ ↑A.card * ↑B.card

The stepped prediction never exceeds the number #A * #B of ordered pairs.

theorem SimpleGraph.steppedCount_eq_card_interedges {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) {A B : Finset V} (hA : ∀ C ∈ P.parts, C ⊆ A ∨ Disjoint C A) (hB : ∀ D ∈ P.parts, D ⊆ B ∨ Disjoint D B) : G.steppedCount P A B = ↑(G.interedges A B).card

If A and B are unions of parts of P, the stepped prediction on (A, B) is the true number of edges from A to B.

@[simp]

theorem SimpleGraph.steppedCount_bot {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (A B : Finset V) : G.steppedCount ⊥ A B = ↑(G.interedges A B).card

The partition into singletons predicts every edge count exactly.

theorem SimpleGraph.steppedCount_top {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (A B : Finset V) : G.steppedCount ⊤ A B = ↑(G.edgeDensity Finset.univ Finset.univ) * ↑A.card * ↑B.card

The one-part partition predicts the global edge density on every rectangle.

theorem SimpleGraph.steppedCount_eq_sum_subtype {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (A B : Finset V) : G.steppedCount P A B = ∑ C : ↥P.parts, ∑ D : ↥P.parts, ↑(G.edgeDensity ↑C ↑D) * ↑(A ∩ ↑C).card * ↑(B ∩ ↑D).card

The stepped prediction of P, written over the subtype of parts.

theorem SimpleGraph.steppedCount_eq_sum_edgeDensity_part {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (A B : Finset V) : G.steppedCount P A B = ∑ x ∈ A, ∑ y ∈ B, ↑(G.edgeDensity (P.part x) (P.part y))

The stepped prediction of P as a sum over pairs of vertices: each pair (x, y) ∈ A × B contributes the edge density between the parts of x and y.

theorem SimpleGraph.steppedCount_eq_sum_refinementParent {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) {Q : Finpartition Finset.univ} (h : Q ≤ P) (A B : Finset V) : G.steppedCount P A B = ∑ C : ↥Q.parts, ∑ D : ↥Q.parts, ↑(G.edgeDensity ↑(Finpartition.refinementParent h C) ↑(Finpartition.refinementParent h D)) * ↑(A ∩ ↑C).card * ↑(B ∩ ↑D).card

Under a refinement Q ≤ P, the prediction of P sums, over the pairs of parts of Q, the edge density between their coarse parents times their trace masses.

The cut discrepancy

noncomputable def SimpleGraph.cutDiscrepancy {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) : ℝ

The cut discrepancy of G with respect to P: the largest deviation, over all rectangles (A, B), between the number of edges from A to B and its stepped prediction. It is count-scaled, so it lies between 0 and (card V) ^ 2.

theorem SimpleGraph.abs_card_interedges_sub_steppedCount_le_cutDiscrepancy {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (A B : Finset V) : |↑(G.interedges A B).card - G.steppedCount P A B| ≤ G.cutDiscrepancy P

Every rectangle deviation is bounded by the cut discrepancy.

theorem SimpleGraph.cutDiscrepancy_le_iff {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {P : Finpartition Finset.univ} {c : ℝ} : G.cutDiscrepancy P ≤ c ↔ ∀ (A B : Finset V), |↑(G.interedges A B).card - G.steppedCount P A B| ≤ c

A bound on the cut discrepancy is exactly a bound on every rectangle deviation.

theorem SimpleGraph.lt_cutDiscrepancy_iff {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {P : Finpartition Finset.univ} {c : ℝ} : c < G.cutDiscrepancy P ↔ ∃ (A : Finset V) (B : Finset V), c < |↑(G.interedges A B).card - G.steppedCount P A B|

The cut discrepancy exceeds c exactly when some rectangle deviation does.

theorem SimpleGraph.cutDiscrepancy_nonneg {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) : 0 ≤ G.cutDiscrepancy P

The cut discrepancy is nonnegative.

theorem SimpleGraph.cutDiscrepancy_le_card_sq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) : G.cutDiscrepancy P ≤ ↑(Fintype.card V) ^ 2

The cut discrepancy is at most the number (card V) ^ 2 of ordered pairs of vertices.

@[simp]

theorem SimpleGraph.cutDiscrepancy_bot {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : G.cutDiscrepancy ⊥ = 0

The partition into singletons has cut discrepancy 0.