Coarse induced-count predictions and labelled three-vertex counts

For a graph J on Fin 3 and a finite graph G, J.inducedGraphCount3 G counts the labelled induced copies of J in G: the injective maps g : Fin 3 → V with J.Adj i j ↔ G.Adj (g i) (g j) for all i, j. Nonedges of J must go to nonedges of G, and there is no division by automorphisms of J. This is the number of graph embeddings J ↪g G.

The coarse prediction is defined for every finite linearly ordered vertex type of J. The counting estimates below specialize to three vertices.

Given a partition P of the vertices, J.coarseInducedGraphEstimate G P predicts this count from the edge densities between parts. Each assignment φ of the three vertices of J to three distinct parts contributes the volume ∏ i, #(φ i) times, for each pair i < j, the edge density d(φ i, φ j) if J.Adj i j and the nonedge density 1 - d(φ i, φ j) otherwise. Assignments with a repeated part are not predicted.

The counting lemma for a regular partition compares the two part by part. The actual count splits the same way: the induced copies with vertices in three distinct parts are counted separately for each assignment, and at most 3 * m * (card V) ^ 2 induced copies meet some part twice when all parts have size at most m.

For a τ-uniform equipartition, the coarse prediction counts the induced copies with vertices in three distinct parts up to an error of 15 τ (card V) ^ 3. An assignment whose three pairs of parts are τ-uniform contributes an error of at most 3 τ times its volume, by the counting lemma for three cells. Each other assignment contributes an error of at most its volume, and Mathlib's Finpartition.IsEquipartition.sum_nonUniforms_lt bounds the total volume of these by 3 * 4 τ (card V) ^ 3, one term for each of the three pairs that may fail to be uniform.

Main definitions

• SimpleGraph.inducedGraphCount3 J G: the number of labelled induced copies of J in G.
• SimpleGraph.coarseInducedGraphEstimate J G P: its prediction from the densities of P.

Main results

• SimpleGraph.inducedGraphCount3_eq_card_embedding: the count is the number of embeddings J ↪g G.
• SimpleGraph.inducedGraphCount3_eq_sum: the count splits along the parts containing the three vertices.
• SimpleGraph.sum_card_induced_le_inducedGraphCount3 and SimpleGraph.inducedGraphCount3_le_sum_card_induced_add: the induced copies with vertices in three distinct parts account for all but at most 3 * m * (card V) ^ 2 induced copies.
• SimpleGraph.abs_sum_card_induced_sub_coarseInducedGraphEstimate_le: for a τ-uniform equipartition, the coarse prediction counts the induced copies with vertices in three distinct parts up to an error of 15 τ (card V) ^ 3.
• SimpleGraph.inducedGraphCount3_le_coarseInducedGraphEstimate_add and SimpleGraph.coarseInducedGraphEstimate_sub_le_inducedGraphCount3: the induced counting lemma for a τ-uniform equipartition whose parts have at most m vertices.

References

• Y. Zhao, Graph Theory and Additive Combinatorics, Cambridge University Press (2023), Chapter 2 (the graph regularity method: the graph counting lemma and strong regularity).
• A comparable repeated-cell bound, for real weights dominated by the volume of cell triples, is sum_nontransversal_weight_le in RegularityLemmata/Relational/DiagonalGate.lean of cameronfreer/regularity-lemmata at commit 315ef979f55f31cc43cd791302519d9a34cc2dc0.

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

The coarse prediction of the labelled induced count of J in G from a partition P of the vertices. Each assignment φ of the vertices of J to distinct parts of P contributes the volume ∏ i, #(φ i) times, for each pair i < j, the edge density d(φ i, φ j) if J.Adj i j and the nonedge density 1 - d(φ i, φ j) otherwise (SimpleGraph.patternDensity).

theorem SimpleGraph.coarseInducedGraphEstimate_def {ι : Type u_1} {V : Type u_2} [Fintype ι] [LinearOrder ι] [Fintype V] [DecidableEq V] (J : SimpleGraph ι) [DecidableRel J.Adj] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) : J.coarseInducedGraphEstimate G P = ∑ φ : ι → ↥P.parts with Function.Injective φ, (∏ i : ι, ↑(↑(φ i)).card) * ∏ p : { p : ι × ι // p.1 < p.2 }, G.patternDensity (J.Adj (↑p).1 (↑p).2) ↑(φ (↑p).1) ↑(φ (↑p).2)

theorem SimpleGraph.coarseInducedGraphEstimate_nonneg {ι : Type u_1} {V : Type u_2} [Fintype ι] [LinearOrder ι] [Fintype V] [DecidableEq V] (J : SimpleGraph ι) [DecidableRel J.Adj] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) : 0 ≤ J.coarseInducedGraphEstimate G P

The coarse prediction is nonnegative: edge and nonedge densities lie in [0, 1].

def SimpleGraph.inducedGraphCount3 {V : Type u_1} [Fintype V] [DecidableEq V] (J : SimpleGraph (Fin 3)) [DecidableRel J.Adj] (G : SimpleGraph V) [DecidableRel G.Adj] : ℕ

The number of labelled induced copies of a graph J on Fin 3 in G: the injective maps g : Fin 3 → V such that g i and g j are adjacent in G exactly when i and j are adjacent in J. Nonedges of J must go to nonedges of G, and there is no division by automorphisms of J.

theorem SimpleGraph.inducedGraphCount3_def {V : Type u_1} [Fintype V] [DecidableEq V] (J : SimpleGraph (Fin 3)) [DecidableRel J.Adj] (G : SimpleGraph V) [DecidableRel G.Adj] : J.inducedGraphCount3 G = {g : Fin 3 → V | Function.Injective g ∧ ∀ (i j : Fin 3), J.Adj i j ↔ G.Adj (g i) (g j)}.card

theorem SimpleGraph.inducedGraphCount3_eq_card_embedding {V : Type u_1} [Fintype V] [DecidableEq V] (J : SimpleGraph (Fin 3)) [DecidableRel J.Adj] (G : SimpleGraph V) [DecidableRel G.Adj] : J.inducedGraphCount3 G = Fintype.card (J ↪g G)

The labelled induced copies of J in G are the graph embeddings J ↪g G.

theorem SimpleGraph.inducedGraphCount3_eq_sum {V : Type u_1} [Fintype V] [DecidableEq V] (J : SimpleGraph (Fin 3)) [DecidableRel J.Adj] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) : J.inducedGraphCount3 G = ∑ φ : Fin 3 → ↥P.parts, {g ∈ Fintype.piFinset fun (i : Fin 3) => ↑(φ i) | Function.Injective g ∧ ∀ (i j : Fin 3), J.Adj i j ↔ G.Adj (g i) (g j)}.card

Splitting the labelled induced copies of J along the parts of P containing the images of the three vertices.

theorem SimpleGraph.sum_card_induced_le_inducedGraphCount3 {V : Type u_1} [Fintype V] [DecidableEq V] (J : SimpleGraph (Fin 3)) [DecidableRel J.Adj] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) : ∑ φ : Fin 3 → ↥P.parts with Function.Injective φ, {g ∈ Fintype.piFinset fun (i : Fin 3) => ↑(φ i) | ∀ (i j : Fin 3), J.Adj i j ↔ G.Adj (g i) (g j)}.card ≤ J.inducedGraphCount3 G

Summing, over the assignments φ of the vertices of J to three distinct parts of P, the induced copies of J in the box of φ gives at most J.inducedGraphCount3 G.

theorem SimpleGraph.inducedGraphCount3_le_sum_card_induced_add {V : Type u_1} [Fintype V] [DecidableEq V] (J : SimpleGraph (Fin 3)) [DecidableRel J.Adj] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) {m : ℕ} (hm : ∀ A ∈ P.parts, A.card ≤ m) : J.inducedGraphCount3 G ≤ ∑ φ : Fin 3 → ↥P.parts with Function.Injective φ, {g ∈ Fintype.piFinset fun (i : Fin 3) => ↑(φ i) | ∀ (i j : Fin 3), J.Adj i j ↔ G.Adj (g i) (g j)}.card + 3 * m * Fintype.card V ^ 2

Repeated-cell bound. If every part of P has at most m vertices, then all but at most 3 * m * (card V) ^ 2 labelled induced copies of J have their three vertices in three distinct parts of P.

theorem SimpleGraph.abs_sum_card_induced_sub_coarseInducedGraphEstimate_le {V : Type u_1} [Fintype V] [DecidableEq V] (J : SimpleGraph (Fin 3)) [DecidableRel J.Adj] (G : SimpleGraph V) [DecidableRel G.Adj] {Q : Finpartition Finset.univ} (hQ : Q.IsEquipartition) {τ : ℝ} (hτ : 0 < τ) (hQG : Q.IsUniform G τ) : |∑ φ : Fin 3 → ↥Q.parts with Function.Injective φ, ↑{g ∈ Fintype.piFinset fun (i : Fin 3) => ↑(φ i) | ∀ (i j : Fin 3), J.Adj i j ↔ G.Adj (g i) (g j)}.card - J.coarseInducedGraphEstimate G Q| ≤ 15 * τ * ↑(Fintype.card V) ^ 3

Induced counting lemma for a uniform equipartition, transversal part. If Q is a τ-uniform equipartition with τ > 0, then summing, over the assignments φ of the vertices of J to three distinct parts of Q, the induced copies of J in the box of φ gives the coarse prediction J.coarseInducedGraphEstimate G Q up to an error of at most 15 τ (card V) ^ 3.

theorem SimpleGraph.inducedGraphCount3_le_coarseInducedGraphEstimate_add {V : Type u_1} [Fintype V] [DecidableEq V] (J : SimpleGraph (Fin 3)) [DecidableRel J.Adj] (G : SimpleGraph V) [DecidableRel G.Adj] {Q : Finpartition Finset.univ} (hQ : Q.IsEquipartition) {τ : ℝ} (hτ : 0 < τ) (hQG : Q.IsUniform G τ) {m : ℕ} (hm : ∀ A ∈ Q.parts, A.card ≤ m) : ↑(J.inducedGraphCount3 G) ≤ J.coarseInducedGraphEstimate G Q + 15 * τ * ↑(Fintype.card V) ^ 3 + 3 * ↑m * ↑(Fintype.card V) ^ 2

Induced counting lemma for a uniform equipartition, upper bound. If Q is a τ-uniform equipartition with τ > 0 whose parts have at most m vertices, then J.inducedGraphCount3 G exceeds the coarse prediction from Q by at most 15 τ (card V) ^ 3 + 3 m (card V) ^ 2.

theorem SimpleGraph.coarseInducedGraphEstimate_sub_le_inducedGraphCount3 {V : Type u_1} [Fintype V] [DecidableEq V] (J : SimpleGraph (Fin 3)) [DecidableRel J.Adj] (G : SimpleGraph V) [DecidableRel G.Adj] {Q : Finpartition Finset.univ} (hQ : Q.IsEquipartition) {τ : ℝ} (hτ : 0 < τ) (hQG : Q.IsUniform G τ) : J.coarseInducedGraphEstimate G Q - 15 * τ * ↑(Fintype.card V) ^ 3 ≤ ↑(J.inducedGraphCount3 G)

Induced counting lemma for a uniform equipartition, lower bound. If Q is a τ-uniform equipartition with τ > 0, then J.inducedGraphCount3 G falls short of the coarse prediction from Q by at most 15 τ (card V) ^ 3.