Documentation

Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

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 #

References #

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

theorem Finpartition.equitabilise_aux {α : Type u_1} [DecidableEq α] {s : Finset α} {m : } {a : } {b : } {P : Finpartition s} (hs : a * m + b * (m + 1) = s.card) :
∃ (Q : Finpartition s), (∀ xQ.parts, x.card = m x.card = m + 1) (∀ xP.parts, (x \ (Finset.filter (fun (y : Finset α) => y x) Q.parts).biUnion id).card m) (Finset.filter (fun (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.

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

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
Instances For
    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) = s.card} :
    t (Finpartition.equitabilise h).partst.card = m t.card = m + 1
    theorem Finpartition.equitabilise_isEquipartition {α : Type u_1} [DecidableEq α] {s : Finset α} {m : } {a : } {b : } {P : Finpartition s} {h : a * m + b * (m + 1) = s.card} :
    (Finpartition.equitabilise h).IsEquipartition
    theorem Finpartition.card_filter_equitabilise_big {α : Type u_1} [DecidableEq α] {s : Finset α} {m : } {a : } {b : } (P : Finpartition s) (h : a * m + b * (m + 1) = s.card) :
    (Finset.filter (fun (u : Finset α) => u.card = m + 1) (Finpartition.equitabilise h).parts).card = 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) = s.card) (hm : m 0) :
    (Finset.filter (fun (u : Finset α) => u.card = m) (Finpartition.equitabilise h).parts).card = a
    theorem Finpartition.card_parts_equitabilise {α : Type u_1} [DecidableEq α] {s : Finset α} {m : } {a : } {b : } (P : Finpartition s) (h : a * m + b * (m + 1) = s.card) (hm : m 0) :
    (Finpartition.equitabilise h).parts.card = 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) = s.card) :
    t P.parts(t \ (Finset.filter (fun (u : Finset α) => u t) (Finpartition.equitabilise h).parts).biUnion id).card m
    theorem Finpartition.exists_equipartition_card_eq {α : Type u_1} [DecidableEq α] (s : Finset α) {n : } (hn : n 0) (hs : n s.card) :
    ∃ (P : Finpartition s), P.IsEquipartition P.parts.card = n

    We can find equipartitions of arbitrary size.