Finite equipartitions

This file defines finite equipartitions, the partitions whose parts all are the same size up to a difference of 1.

Main declarations

• Finpartition.IsEquipartition: Predicate for a Finpartition to be an equipartition.
• Finpartition.IsEquipartition.exists_partPreservingEquiv: part-preserving enumeration of a finset equipped with an equipartition. Indices of elements in the same part are congruent modulo the number of parts.

def Finpartition.IsEquipartition {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) : Prop

An equipartition is a partition whose parts are all the same size, up to a difference of 1.

Equations

• P.IsEquipartition = (↑P.parts).EquitableOn Finset.card

theorem Finpartition.isEquipartition_iff_card_parts_eq_average {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) : P.IsEquipartition ↔ ∀ a ∈ P.parts, a.card = s.card / P.parts.card ∨ a.card = s.card / P.parts.card + 1

theorem Finpartition.not_isEquipartition {α : Type u_1} [DecidableEq α] {s : Finset α} {P : Finpartition s} : ¬P.IsEquipartition ↔ ∃ a ∈ P.parts, ∃ b ∈ P.parts, b.card + 1 < a.card

theorem Set.Subsingleton.isEquipartition {α : Type u_1} [DecidableEq α] {s : Finset α} {P : Finpartition s} (h : (↑P.parts).Subsingleton) : P.IsEquipartition

theorem Finpartition.IsEquipartition.card_parts_eq_average {α : Type u_1} [DecidableEq α] {s t : Finset α} {P : Finpartition s} (hP : P.IsEquipartition) (ht : t ∈ P.parts) : t.card = s.card / P.parts.card ∨ t.card = s.card / P.parts.card + 1

theorem Finpartition.IsEquipartition.card_part_eq_average_iff {α : Type u_1} [DecidableEq α] {s t : Finset α} {P : Finpartition s} (hP : P.IsEquipartition) (ht : t ∈ P.parts) : t.card = s.card / P.parts.card ↔ t.card ≠ s.card / P.parts.card + 1

theorem Finpartition.IsEquipartition.average_le_card_part {α : Type u_1} [DecidableEq α] {s t : Finset α} {P : Finpartition s} (hP : P.IsEquipartition) (ht : t ∈ P.parts) : s.card / P.parts.card ≤ t.card

theorem Finpartition.IsEquipartition.card_part_le_average_add_one {α : Type u_1} [DecidableEq α] {s t : Finset α} {P : Finpartition s} (hP : P.IsEquipartition) (ht : t ∈ P.parts) : t.card ≤ s.card / P.parts.card + 1

theorem Finpartition.IsEquipartition.filter_ne_average_add_one_eq_average {α : Type u_1} [DecidableEq α] {s : Finset α} {P : Finpartition s} (hP : P.IsEquipartition) : Finset.filter (fun (p : Finset α) => ¬p.card = s.card / P.parts.card + 1) P.parts = Finset.filter (fun (p : Finset α) => p.card = s.card / P.parts.card) P.parts

theorem Finpartition.IsEquipartition.card_large_parts_eq_mod {α : Type u_1} [DecidableEq α] {s : Finset α} {P : Finpartition s} (hP : P.IsEquipartition) : (Finset.filter (fun (p : Finset α) => p.card = s.card / P.parts.card + 1) P.parts).card = s.card % P.parts.card

An equipartition of a finset with n elements into k parts has n % k parts of size n / k + 1.

theorem Finpartition.IsEquipartition.card_small_parts_eq_mod {α : Type u_1} [DecidableEq α] {s : Finset α} {P : Finpartition s} (hP : P.IsEquipartition) : (Finset.filter (fun (p : Finset α) => p.card = s.card / P.parts.card) P.parts).card = P.parts.card - s.card % P.parts.card

An equipartition of a finset with n elements into k parts has n - n % k parts of size n / k.

theorem Finpartition.IsEquipartition.exists_partsEquiv {α : Type u_1} [DecidableEq α] {s : Finset α} {P : Finpartition s} (hP : P.IsEquipartition) : ∃ (f : { x : Finset α // x ∈ P.parts } ≃ Fin P.parts.card), ∀ (t : { x : Finset α // x ∈ P.parts }), (↑t).card = s.card / P.parts.card + 1 ↔ ↑(f t) < s.card % P.parts.card

There exists an enumeration of an equipartition's parts where larger parts map to smaller numbers and vice versa.

theorem Finpartition.IsEquipartition.exists_partPreservingEquiv {α : Type u_1} [DecidableEq α] {s : Finset α} {P : Finpartition s} (hP : P.IsEquipartition) : ∃ (f : { x : α // x ∈ s } ≃ Fin s.card), ∀ (a b : { x : α // x ∈ s }), P.part ↑a = P.part ↑b ↔ ↑(f a) % P.parts.card = ↑(f b) % P.parts.card

Given a finset equipartitioned into k parts, its elements can be enumerated such that elements in the same part have congruent indices modulo k.

Discrete and indiscrete finpartitions

theorem Finpartition.bot_isEquipartition {α : Type u_1} [DecidableEq α] (s : Finset α) : ⊥.IsEquipartition

theorem Finpartition.top_isEquipartition {α : Type u_1} [DecidableEq α] (s : Finset α) [Decidable (s = ⊥)] : ⊤.IsEquipartition

theorem Finpartition.indiscrete_isEquipartition {α : Type u_1} [DecidableEq α] (s : Finset α) {hs : s ≠ ∅} : (indiscrete hs).IsEquipartition