Equitable exact refinements of equipartitions

An equipartition P of s can be refined exactly by an equipartition with a times as many parts, as soon as a * #P.parts ≤ #s: equitabilise every part of P into a pieces. Since the parts of P have size #s / #P.parts or one more, all the pieces have size q or q + 1, where q = #s / #P.parts / a.

Exact refinement by equipartitions is what iterated regularity arguments need when they nest regular partitions: Mathlib's Finpartition.exists_equipartition_card_eq produces an equipartition with a prescribed number of parts but relates it to no given partition.

Equitabilising an arbitrary partition P does not refine it, but it moves few points: at most m points of each part of P lie in a part of P.equitabilise h that is not contained in it. This controls how much a quantity defined part by part, such as an energy, can change.

Main declarations

• Finpartition.IsEquipartition.exists_refining_equipartition_card_eq_mul: an equipartition with k parts is refined by an equipartition with exactly a * k parts, provided a ≠ 0 and a * k ≤ #s.
• Finpartition.card_filter_not_part_equitabilise_subset_part_le: at most #P.parts * m points of s have a part in P.equitabilise h not contained in their part in P.
• Finpartition.exists_card_parts_equitabilise_eq: P.equitabilise can produce any number n ≤ #s of parts.
• Finpartition.exists_equipartition_card_eq_card_filter_not_part_subset_le: every partition is close, in this sense, to an equipartition with any number n ≤ #s of parts.

theorem Finpartition.IsEquipartition.exists_refining_equipartition_card_eq_mul {α : Type u_1} [DecidableEq α] {s : Finset α} {P : Finpartition s} (hP : P.IsEquipartition) {a : ℕ} (ha : a ≠ 0) (hs : a * P.parts.card ≤ s.card) : ∃ (Q : Finpartition s), Q.IsEquipartition ∧ Q.parts.card = a * P.parts.card ∧ Q ≤ P

An equipartition P of s is refined by an equipartition of s with exactly a * #P.parts parts, for any a ≠ 0 with a * #P.parts ≤ #s. Each part of P is equitabilised into a pieces.

theorem Finpartition.card_filter_not_part_equitabilise_subset_part_le {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {a b m : ℕ} (h : a * m + b * (m + 1) = s.card) : {x ∈ s | ¬(equitabilise h).part x ⊆ P.part x}.card ≤ P.parts.card * m

Equitabilising moves few points. At most #P.parts * m points of s lie in a part of P.equitabilise h that is not contained in their part of P, where the parts of P.equitabilise h have size m or m + 1.

theorem Finpartition.exists_card_parts_equitabilise_eq {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {n : ℕ} (hn : n ≠ 0) (hns : n ≤ s.card) : ∃ (a : ℕ) (b : ℕ) (h : a * (s.card / n) + b * (s.card / n + 1) = s.card), (equitabilise h).parts.card = n

For 0 < n ≤ #s, some instance of P.equitabilise has exactly n parts, of sizes #s / n and #s / n + 1.

theorem Finpartition.exists_equipartition_card_eq_card_filter_not_part_subset_le {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {n : ℕ} (hn : n ≠ 0) (hns : n ≤ s.card) : ∃ (Q : Finpartition s), Q.IsEquipartition ∧ Q.parts.card = n ∧ {x ∈ s | ¬Q.part x ⊆ P.part x}.card ≤ P.parts.card * (s.card / n)

Every partition P of s is close to an equipartition of s into any number n of parts with 0 < n ≤ #s: at most #P.parts * (#s / n) points of s lie in a part of the equipartition not contained in their part of P.