Equitabilising a partition #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source

theorem finpartition.equitabilise_aux {α : Type u_1} [decidable_eq α] {s : finset α} {m a b : ℕ} (P : finpartition s) (hs : a * m + b * (m + 1) = s.card) :

∃ (Q : finpartition s), (∀ (x : finset α), x ∈ Q.parts → x.card = m ∨ x.card = m + 1) ∧ (∀ (x : finset α), x ∈ P.parts → (x \ (finset.filter (λ (y : finset α), y ⊆ x) Q.parts).bUnion id).card ≤ m) ∧ (finset.filter (λ (i : finset α), i.card = m + 1) Q.parts).card = 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.

source

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

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.

Equations

P.equitabilise h = _.some

source

theorem finpartition.card_eq_of_mem_parts_equitabilise {α : Type u_1} [decidable_eq α] {s t : finset α} {m a b : ℕ} {P : finpartition s} {h : a * m + b * (m + 1) = s.card} :

t ∈ (P.equitabilise h).parts → t.card = m ∨ t.card = m + 1

source

theorem finpartition.equitabilise_is_equipartition {α : Type u_1} [decidable_eq α] {s : finset α} {m a b : ℕ} {P : finpartition s} {h : a * m + b * (m + 1) = s.card} :

(P.equitabilise h).is_equipartition

source

theorem finpartition.card_filter_equitabilise_big {α : Type u_1} [decidable_eq α] {s : finset α} {m a b : ℕ} (P : finpartition s) (h : a * m + b * (m + 1) = s.card) :

(finset.filter (λ (u : finset α), u.card = m + 1) (P.equitabilise h).parts).card = b

source

theorem finpartition.card_filter_equitabilise_small {α : Type u_1} [decidable_eq α] {s : finset α} {m a b : ℕ} (P : finpartition s) (h : a * m + b * (m + 1) = s.card) (hm : m ≠ 0) :

(finset.filter (λ (u : finset α), u.card = m) (P.equitabilise h).parts).card = a

source

theorem finpartition.card_parts_equitabilise {α : Type u_1} [decidable_eq α] {s : finset α} {m a b : ℕ} (P : finpartition s) (h : a * m + b * (m + 1) = s.card) (hm : m ≠ 0) :

(P.equitabilise h).parts.card = a + b

source

theorem finpartition.card_parts_equitabilise_subset_le {α : Type u_1} [decidable_eq α] {s t : finset α} {m a b : ℕ} (P : finpartition s) (h : a * m + b * (m + 1) = s.card) :

t ∈ P.parts → (t \ (finset.filter (λ (u : finset α), u ⊆ t) (P.equitabilise h).parts).bUnion id).card ≤ m

source

theorem finpartition.exists_equipartition_card_eq {α : Type u_1} [decidable_eq α] (s : finset α) {n : ℕ} (hn : n ≠ 0) (hs : n ≤ s.card) :

∃ (P : finpartition s), P.is_equipartition ∧ P.parts.card = n

We can find equipartitions of arbitrary size.