# 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]

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

- Finpartition.equitabilise h = ⋯.choose

## Instances For

We can find equipartitions of arbitrary size.