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
whereh : a * m + b * (m + 1)
is a partition witha
parts of sizem
andb
parts of sizem + 1
which almost refinesP
.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
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.
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
We can find equipartitions of arbitrary size.