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.
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] :
@[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 𝕜] :