Energy of a partition #
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.
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.
theorem
finpartition.energy_nonneg
{α : Type u_1}
[decidable_eq α]
{s : finset α}
(P : finpartition s)
(G : simple_graph α)
[decidable_rel G.adj] :
theorem
finpartition.energy_le_one
{α : Type u_1}
[decidable_eq α]
{s : finset α}
(P : finpartition s)
(G : simple_graph α)
[decidable_rel G.adj] :