Size-weighted energy of a vertex partition

For a finite simple graph G on V with n = |V| and a partition P of the vertex set, the size-weighted energy is G.weightedEnergy P = ∑ A ∈ P, ∑ B ∈ P, (|A||B| / n²) · d_G(A, B)², where d_G = SimpleGraph.edgeDensity. It is the mean square of the block-average step function (x, y) ↦ d_G(P.part x, P.part y) (SimpleGraph.weightedEnergy_eq_sum_part).

Two conventions are deliberate. All ordered pairs of parts are summed, including the diagonal blocks A = B, and d_G(A, A) uses the denominator |A|² (ordered pairs, loops counted as non-edges), not |A|(|A| - 1). Consequently the energy is not Mathlib's Finpartition.energy, which averages over off-diagonal pairs of parts without size weights and is not monotone under arbitrary refinement.

The weighted energy is monotone under arbitrary refinement, with an exact defect: for Q ≤ P, the weighted mean square deviation between the densities of fine blocks and of their coarse parent blocks is the energy gap (SimpleGraph.weightedDensityDeviation_sq). By weighted Cauchy–Schwarz, an energy gap of at most ε bounds the weighted mean absolute deviation by √ε (SimpleGraph.weightedDensityDeviation_abs_le). Neither statement needs equitability or regularity; these are the energy-increment inputs of weak and strong regularity arguments.

Main results

• SimpleGraph.weightedEnergy: the size-weighted energy, with weightedEnergy_nonneg and weightedEnergy_le_one.
• SimpleGraph.weightedEnergy_eq_sum_part: the energy is the mean square of the block-average step function.
• SimpleGraph.weightedEnergy_comap_symm: the energy is invariant under relabelling the vertices.
• SimpleGraph.weightedDensityDeviation_sq: the refinement defect identity.
• SimpleGraph.weightedEnergy_mono_of_refines: refining a partition does not decrease energy.
• SimpleGraph.weightedDensityDeviation_abs_le: the absolute-deviation bound from an energy gap.
• SimpleGraph.sum_sum_abs_edgeDensity_part_sub_le: the same bound summed over pairs of vertices.

References

• L. Lovász, B. Szegedy, Szemerédi's Lemma for the Analyst, GAFA 17 (2007).
• Y. Zhao, Graph Theory and Additive Combinatorics (2023), ch. 2.
• The size-weighted energy and its refinement monotonicity also appear, for directed relations, as energy and energy_mono in the Lean library cameronfreer/regularity-lemmata (Partition/Energy.lean).

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

The size-weighted energy of a partition P of the vertices of G: ∑ A ∈ P, ∑ B ∈ P, (|A||B| / |V|²) · d_G(A, B)². It sums over all ordered pairs of parts, including the diagonal blocks A = B, where d_G(A, A) has denominator |A|². Unlike Mathlib's Finpartition.energy, it is monotone under arbitrary refinement (SimpleGraph.weightedEnergy_mono_of_refines).

theorem SimpleGraph.weightedEnergy_def {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) : G.weightedEnergy P = ∑ A ∈ P.parts, ∑ B ∈ P.parts, ↑A.card * ↑B.card / ↑(Fintype.card V) ^ 2 * ↑(G.edgeDensity A B) ^ 2

Unfolding lemma for SimpleGraph.weightedEnergy.

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

The weighted energy is nonnegative.

theorem SimpleGraph.weightedEnergy_le_one {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) : G.weightedEnergy P ≤ 1

The weighted energy is at most one, since edge densities lie in [0, 1] and the block weights sum to at most one.

theorem SimpleGraph.weightedEnergy_eq_sum_part {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) : G.weightedEnergy P = (∑ x : V, ∑ y : V, ↑(G.edgeDensity (P.part x) (P.part y)) ^ 2) / ↑(Fintype.card V) ^ 2

The weighted energy is the mean square of the block-average step function (x, y) ↦ d_G(P.part x, P.part y) over all ordered pairs of vertices, diagonal included.

@[simp]

theorem SimpleGraph.weightedEnergy_comap_symm {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {W : Type u_2} [Fintype W] [DecidableEq W] (e : V ≃ W) (P : Finpartition Finset.univ) : (SimpleGraph.comap (⇑e.symm) G).weightedEnergy (Finpartition.comap (⇑e.symm) (P.copy ⋯)) = G.weightedEnergy P

The weighted energy is invariant under relabelling. Relabel the vertices along e: the graph becomes G.comap e.symm and the partition becomes the pullback of P along e.symm. The size-weighted energy is unchanged.

theorem SimpleGraph.weightedDensityDeviation_sq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {P Q : Finpartition Finset.univ} (h : Q ≤ P) : ∑ B : ↥Q.parts, ∑ D : ↥Q.parts, ↑(↑B).card * ↑(↑D).card / ↑(Fintype.card V) ^ 2 * (↑(G.edgeDensity ↑B ↑D) - ↑(G.edgeDensity ↑(Finpartition.refinementParent h B) ↑(Finpartition.refinementParent h D))) ^ 2 = G.weightedEnergy Q - G.weightedEnergy P

Refinement defect identity. For a refinement Q ≤ P, the size-weighted mean square deviation of the fine block densities from the densities of their coarse parent blocks equals the energy gap. All ordered pairs of fine parts are summed, diagonal blocks included; no equitability or regularity is assumed, and on the empty host both sides vanish.

theorem SimpleGraph.weightedEnergy_mono_of_refines {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {P Q : Finpartition Finset.univ} (h : P ≤ Q) : G.weightedEnergy Q ≤ G.weightedEnergy P

Monotonicity under refinement. If P refines Q (P ≤ Q), then the energy of P is at least that of Q.

theorem SimpleGraph.weightedDensityDeviation_abs_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 ≤ ε) : ∑ B : ↥Q.parts, ∑ D : ↥Q.parts, ↑(↑B).card * ↑(↑D).card / ↑(Fintype.card V) ^ 2 * |↑(G.edgeDensity ↑B ↑D) - ↑(G.edgeDensity ↑(Finpartition.refinementParent h B) ↑(Finpartition.refinementParent h D))| ≤ √ε

Energy gap controls absolute deviation. For a refinement Q ≤ P whose energy gap is at most ε, the size-weighted mean absolute deviation of the fine block densities from their parent densities is at most √ε. This is weighted Cauchy–Schwarz applied to SimpleGraph.weightedDensityDeviation_sq, using that the block weights sum to at most one.

theorem SimpleGraph.sum_sum_abs_edgeDensity_part_sub_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 ≤ ε) : ∑ x : V, ∑ y : V, |↑(G.edgeDensity (Q.part x) (Q.part y)) - ↑(G.edgeDensity (P.part x) (P.part y))| ≤ √ε * ↑(Fintype.card V) ^ 2

Summed over all ordered pairs of vertices, the edge densities between the parts through them change by at most √ε * (card V) ^ 2 from a refinement Q ≤ P to P whose energy gap is at most ε. This is SimpleGraph.weightedDensityDeviation_abs_le with each pair of fine parts counted once for each pair of vertices in it.