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.
References #
[Yaël Dillies, Bhavik Mehta, Formalising Szemerédi’s Regularity Lemma in Lean][srl_itp]
def
Finpartition.energy
{α : Type u_1}
[DecidableEq α]
{s : Finset α}
(P : Finpartition s)
(G : SimpleGraph α)
[DecidableRel G.Adj]
:
The energy of a partition, also known as index. Auxiliary quantity for Szemerédi's regularity lemma.
Instances For
theorem
Finpartition.energy_nonneg
{α : Type u_1}
[DecidableEq α]
{s : Finset α}
(P : Finpartition s)
(G : SimpleGraph α)
[DecidableRel G.Adj]
:
0 ≤ Finpartition.energy P G
theorem
Finpartition.energy_le_one
{α : Type u_1}
[DecidableEq α]
{s : Finset α}
(P : Finpartition s)
(G : SimpleGraph α)
[DecidableRel G.Adj]
:
Finpartition.energy P G ≤ 1
@[simp]
theorem
Finpartition.coe_energy
{α : Type u_1}
[DecidableEq α]
{s : Finset α}
(P : Finpartition s)
(G : SimpleGraph α)
[DecidableRel G.Adj]
{𝕜 : Type u_2}
[LinearOrderedField 𝕜]
:
↑(Finpartition.energy P G) = (Finset.sum (Finset.offDiag P.parts) fun uv => ↑(SimpleGraph.edgeDensity G uv.fst uv.snd) ^ 2) / ↑(Finset.card P.parts) ^ 2