mathlib3 documentation

combinatorics.simple_graph.regularity.energy

Energy of a partition #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the energy of a partition.

The energy is the auxiliary quantity that drives the induction process in the proof of Szemerédi's Regularity Lemma. As long as we do not have a suitable equipartition, we will find a new one that has an energy greater than the previous one plus some fixed constant.

References #

Yaël Dillies, Bhavik Mehta, Formalising Szemerédi’s Regularity Lemma in Lean

def finpartition.energy {α : Type u_1} [decidable_eq α] {s : finset α} (P : finpartition s) (G : simple_graph α) [decidable_rel G.adj] :

The energy of a partition, also known as index. Auxiliary quantity for Szemerédi's regularity lemma.

Equations
theorem finpartition.energy_nonneg {α : Type u_1} [decidable_eq α] {s : finset α} (P : finpartition s) (G : simple_graph α) [decidable_rel G.adj] :
0 P.energy G
theorem finpartition.energy_le_one {α : Type u_1} [decidable_eq α] {s : finset α} (P : finpartition s) (G : simple_graph α) [decidable_rel G.adj] :
P.energy G 1
@[simp, norm_cast]
theorem finpartition.coe_energy {α : Type u_1} [decidable_eq α] {s : finset α} (P : finpartition s) (G : simple_graph α) [decidable_rel G.adj] {𝕜 : Type u_2} [linear_ordered_field 𝕜] :
(P.energy G) = P.parts.off_diag.sum (λ (uv : finset α × finset α), (G.edge_density uv.fst uv.snd) ^ 2) / (P.parts.card) ^ 2