Equitabilising a partition

This file allows to blow partitions up into parts of controlled size. Given a partition P and a b m : ℕ, we want to find a partition Q with a parts of size m and b parts of size m + 1 such that all parts of P are "as close as possible" to unions of parts of Q. By "as close as possible", we mean that each part of P can be written as the union of some parts of Q along with at most m other elements.

Main declarations

• Finpartition.equitabilise: P.equitabilise h where h : a * m + b * (m + 1) is a partition with a parts of size m and b parts of size m + 1 which almost refines P.
• Finpartition.exists_equipartition_card_eq: We can find equipartitions of arbitrary size.

References

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

theorem Finpartition.equitabilise_aux {α : Type u_1} [DecidableEq α] {s : Finset α} {m : ℕ} {a : ℕ} {b : ℕ} {P : Finpartition s} (hs : a * m + b * (m + 1) = Finset.card s) : ∃ Q, (∀ (x : Finset α), x ∈ Q.parts → Finset.card x = m ∨ Finset.card x = m + 1) ∧ (∀ (x : Finset α), x ∈ P.parts → Finset.card (x \ Finset.biUnion (Finset.filter (fun y => y ⊆ x) Q.parts) id) ≤ m) ∧ Finset.card (Finset.filter (fun i => Finset.card i = m + 1) Q.parts) = b

Given a partition P of s, as well as a proof that a * m + b * (m + 1) = s.card, we can find a new partition Q of s where each part has size m or m + 1, every part of P is the union of parts of Q plus at most m extra elements, there are b parts of size m + 1 and (provided m > 0, because a partition does not have parts of size 0) there are a parts of size m and hence a + b parts in total.

noncomputable def Finpartition.equitabilise {α : Type u_1} [DecidableEq α] {s : Finset α} {m : ℕ} {a : ℕ} {b : ℕ} {P : Finpartition s} (h : a * m + b * (m + 1) = Finset.card s) : Finpartition s

Given a partition P of s, as well as a proof that a * m + b * (m + 1) = s.card, build a new partition Q of s where each part has size m or m + 1, every part of P is the union of parts of Q plus at most m extra elements, there are b parts of size m + 1 and (provided m > 0, because a partition does not have parts of size 0) there are a parts of size m and hence a + b parts in total.

theorem Finpartition.card_eq_of_mem_parts_equitabilise {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {m : ℕ} {a : ℕ} {b : ℕ} {P : Finpartition s} {h : a * m + b * (m + 1) = Finset.card s} : t ∈ (Finpartition.equitabilise h).parts → Finset.card t = m ∨ Finset.card t = m + 1

theorem Finpartition.equitabilise_isEquipartition {α : Type u_1} [DecidableEq α] {s : Finset α} {m : ℕ} {a : ℕ} {b : ℕ} {P : Finpartition s} {h : a * m + b * (m + 1) = Finset.card s} : Finpartition.IsEquipartition (Finpartition.equitabilise h)

theorem Finpartition.card_filter_equitabilise_big {α : Type u_1} [DecidableEq α] {s : Finset α} {m : ℕ} {a : ℕ} {b : ℕ} (P : Finpartition s) (h : a * m + b * (m + 1) = Finset.card s) : Finset.card (Finset.filter (fun u => Finset.card u = m + 1) (Finpartition.equitabilise h).parts) = b

theorem Finpartition.card_filter_equitabilise_small {α : Type u_1} [DecidableEq α] {s : Finset α} {m : ℕ} {a : ℕ} {b : ℕ} (P : Finpartition s) (h : a * m + b * (m + 1) = Finset.card s) (hm : m ≠ 0) : Finset.card (Finset.filter (fun u => Finset.card u = m) (Finpartition.equitabilise h).parts) = a

theorem Finpartition.card_parts_equitabilise {α : Type u_1} [DecidableEq α] {s : Finset α} {m : ℕ} {a : ℕ} {b : ℕ} (P : Finpartition s) (h : a * m + b * (m + 1) = Finset.card s) (hm : m ≠ 0) : Finset.card (Finpartition.equitabilise h).parts = a + b

theorem Finpartition.card_parts_equitabilise_subset_le {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {m : ℕ} {a : ℕ} {b : ℕ} (P : Finpartition s) (h : a * m + b * (m + 1) = Finset.card s) : t ∈ P.parts → Finset.card (t \ Finset.biUnion (Finset.filter (fun u => u ⊆ t) (Finpartition.equitabilise h).parts) id) ≤ m

theorem Finpartition.exists_equipartition_card_eq {α : Type u_1} [DecidableEq α] (s : Finset α) {n : ℕ} (hn : n ≠ 0) (hs : n ≤ Finset.card s) : ∃ P, Finpartition.IsEquipartition P ∧ Finset.card P.parts = n

We can find equipartitions of arbitrary size.