The stepped prediction of labelled induced three-vertex counts

For a graph J on Fin 3, a finite graph G and a partition R of its vertices, J.steppedInducedGraphCount3 G R is the number of labelled induced copies of J predicted by the R-stepped graph, the weighted graph whose weight on a pair of vertices is the edge density of G between their parts. Each assignment φ of the three vertices of J to parts of R, repeated parts included, 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. Equivalently, it sums over all maps g : Fin 3 → V the product of these densities between the parts containing the images (SimpleGraph.steppedInducedGraphCount3_eq_sum_part).

Unlike the coarse prediction SimpleGraph.coarseInducedGraphEstimate, which only sums over assignments to three distinct parts, the stepped prediction behaves well under refinement: for a refinement Q ≤ P whose size-weighted energy exceeds that of P by at most ε, the stepped predictions of Q and P differ by at most 3 √ε (card V) ^ 3. Each of the three density factors changes by the deviation of a fine density from its coarse parent density, and the weighted mean of these deviations is at most √ε (SimpleGraph.weightedDensityDeviation_abs_le). For a single partition R, the stepped prediction and the coarse prediction differ only by the assignments with a repeated part, which contribute at most 3 * m * (card V) ^ 2 when every part of R has at most m vertices.

These are the energy-transfer and repeated-cell steps of the induced counting lemma for strong graph regularity, which compares the actual count with the coarse prediction of the coarse partition through the stepped predictions of the fine and coarse partitions.

Main definitions

• SimpleGraph.steppedInducedGraphCount3 J G R: the stepped prediction of the induced count.

Main results

• SimpleGraph.steppedInducedGraphCount3_eq_sum_part: the stepped prediction as a sum over all maps Fin 3 → V.
• SimpleGraph.abs_steppedInducedGraphCount3_sub_le: the energy-transfer bound |T_Q - T_P| ≤ 3 √ε (card V) ^ 3 for a refinement with energy gap at most ε.
• SimpleGraph.coarseInducedGraphEstimate_le_steppedInducedGraphCount3 and SimpleGraph.steppedInducedGraphCount3_le_coarseInducedGraphEstimate_add: the stepped prediction exceeds the coarse prediction by at most 3 * m * (card V) ^ 2.

References

• T. Tao, Szemerédi's regularity lemma revisited, Contrib. Discrete Math. 1 (2006).
• Y. Zhao, Graph Theory and Additive Combinatorics, Cambridge University Press (2023), Chapter 2 (the graph regularity method: the graph counting lemma and strong regularity).

noncomputable def SimpleGraph.steppedInducedGraphCount3 {V : Type u_1} [Fintype V] [DecidableEq V] (J : SimpleGraph (Fin 3)) [DecidableRel J.Adj] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Finpartition Finset.univ) : ℝ

The stepped prediction of J.inducedGraphCount3 G from a partition R of the vertices: the number of labelled induced copies of J in the R-stepped graph. Each assignment φ of the vertices of J to parts of R, repeated parts included, 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.

theorem SimpleGraph.steppedInducedGraphCount3_def {V : Type u_1} [Fintype V] [DecidableEq V] (J : SimpleGraph (Fin 3)) [DecidableRel J.Adj] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Finpartition Finset.univ) : J.steppedInducedGraphCount3 G R = ∑ φ : Fin 3 → ↥R.parts, (∏ i : Fin 3, ↑(↑(φ i)).card) * ∏ p : { p : Fin 3 × Fin 3 // p.1 < p.2 }, G.patternDensity (J.Adj (↑p).1 (↑p).2) ↑(φ (↑p).1) ↑(φ (↑p).2)

theorem SimpleGraph.steppedInducedGraphCount3_eq_sum_part {V : Type u_1} [Fintype V] [DecidableEq V] (J : SimpleGraph (Fin 3)) [DecidableRel J.Adj] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Finpartition Finset.univ) : J.steppedInducedGraphCount3 G R = ∑ g : Fin 3 → V, ∏ p : { p : Fin 3 × Fin 3 // p.1 < p.2 }, G.patternDensity (J.Adj (↑p).1 (↑p).2) (R.part (g (↑p).1)) (R.part (g (↑p).2))

The stepped prediction sums, over all maps g : Fin 3 → V, the product of the edge or nonedge densities between the parts of R containing the images.

theorem SimpleGraph.steppedInducedGraphCount3_nonneg {V : Type u_1} [Fintype V] [DecidableEq V] (J : SimpleGraph (Fin 3)) [DecidableRel J.Adj] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Finpartition Finset.univ) : 0 ≤ J.steppedInducedGraphCount3 G R

The stepped prediction is nonnegative.

theorem SimpleGraph.coarseInducedGraphEstimate_le_steppedInducedGraphCount3 {V : Type u_1} [Fintype V] [DecidableEq V] (J : SimpleGraph (Fin 3)) [DecidableRel J.Adj] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Finpartition Finset.univ) : J.coarseInducedGraphEstimate G R ≤ J.steppedInducedGraphCount3 G R

The coarse prediction, which omits the assignments with a repeated part, is at most the stepped prediction.

theorem SimpleGraph.steppedInducedGraphCount3_le_coarseInducedGraphEstimate_add {V : Type u_1} [Fintype V] [DecidableEq V] (J : SimpleGraph (Fin 3)) [DecidableRel J.Adj] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Finpartition Finset.univ) {m : ℕ} (hm : ∀ A ∈ R.parts, A.card ≤ m) : J.steppedInducedGraphCount3 G R ≤ J.coarseInducedGraphEstimate G R + 3 * ↑m * ↑(Fintype.card V) ^ 2

If every part of R has at most m vertices, the assignments with a repeated part add at most 3 * m * (card V) ^ 2 to the coarse prediction.

theorem SimpleGraph.abs_steppedInducedGraphCount3_sub_le {V : Type u_1} [Fintype V] [DecidableEq V] (J : SimpleGraph (Fin 3)) [DecidableRel J.Adj] (G : SimpleGraph V) [DecidableRel G.Adj] {P Q : Finpartition Finset.univ} (h : Q ≤ P) {ε : ℝ} (hgap : G.weightedEnergy Q - G.weightedEnergy P ≤ ε) : |J.steppedInducedGraphCount3 G Q - J.steppedInducedGraphCount3 G P| ≤ 3 * √ε * ↑(Fintype.card V) ^ 3

Energy transfer. For a refinement Q ≤ P whose size-weighted energy exceeds that of P by at most ε, the stepped predictions of Q and P differ by at most 3 √ε (card V) ^ 3. No equitability or regularity is assumed.