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.

Equations

• Finpartition.energy P G = (Finset.sum (Finset.offDiag P.parts) fun (uv : Finset α × Finset α) => SimpleGraph.edgeDensity G uv.1 uv.2 ^ 2) / ↑P.parts.card ^ 2

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 : Finset α × Finset α) => ↑(SimpleGraph.edgeDensity G uv.1 uv.2) ^ 2) / ↑P.parts.card ^ 2