Finpartition.equitabilise_aux
theorem Finpartition.equitabilise_aux :
∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {m a b : ℕ} {P : Finpartition s},
a * m + b * (m + 1) = s.card →
∃ Q,
(∀ x ∈ Q.parts, x.card = m ∨ x.card = m + 1) ∧
(∀ x ∈ P.parts, (x \ (Finset.filter (fun y => y ⊆ x) Q.parts).biUnion id).card ≤ m) ∧
(Finset.filter (fun i => i.card = m + 1) Q.parts).card = b
This theorem states that given a partition `P` of a finite set `s`, and the preconditions that `a * m + b * (m + 1) = s.card`, there exists a new partition `Q` of `s` with the following properties:
1. Each part in `Q` has a size of either `m` or `m + 1`.
2. Every part of `P` is the union of parts of `Q` plus at most `m` extra elements.
3. The number of parts of size `m + 1` in `Q` is `b`.
4. Provided `m > 0` (as a partition does not have parts of size `0`), there are `a` parts of size `m` in `Q`, and hence `a + b` parts in total.
This theorem is essentially proving the existence of a way to "repartition" a given partition `P` into a more "equitable" partition `Q`, under certain conditions.
More concisely: Given a finite set `s` with partition `P` and integers `a` and `b` such that `a * m + b * (m + 1) = s.card` for some positive integer `m`, there exists a partition `Q` of `s` with each part having size `m` or `m + 1`, `a` parts of size `m`, `b` parts of size `m + 1`, and every part of `P` being a union of parts of `Q` plus at most `m` extra elements.
|
Finpartition.exists_equipartition_card_eq
theorem Finpartition.exists_equipartition_card_eq :
∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α) {n : ℕ},
n ≠ 0 → n ≤ s.card → ∃ P, P.IsEquipartition ∧ P.parts.card = n
This theorem states that for any given type `α` with decidable equality, any finite set `s` of this type, and any natural number `n` that is not zero and is less than or equal to the cardinality of `s`, there exists a partition `P` of the set `s` such that this partition is an equipartition (every partition has the same size) and the number of parts in this partition is equal to `n`. In simpler terms, it is always possible to divide a finite set into a specified number of equal parts, given that the number of parts is not greater than the size of the original set and is not zero.
More concisely: Given a finite type `α` with decidable equality, for any natural number `n` less than or equal to the cardinality of a finite set `s` of `α`, there exists an equipartition of `s` into `n` parts.
|
Finpartition.card_eq_of_mem_parts_equitabilise
theorem Finpartition.card_eq_of_mem_parts_equitabilise :
∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {m a b : ℕ} {P : Finpartition s}
{h : a * m + b * (m + 1) = s.card}, t ∈ (Finpartition.equitabilise h).parts → t.card = m ∨ t.card = m + 1
The theorem `Finpartition.card_eq_of_mem_parts_equitabilise` states that for any type `α` with decidable equality, any finsets `s` and `t` of `α`, any natural numbers `m`, `a`, `b`, and any finpartition `P` of `s` such that `a * m + b * (m + 1) = s.card`, if `t` is a member of the parts of the equitabilised finpartition `P` through `h`, then the cardinality of `t` is either `m` or `m + 1`.
In simpler terms, it says that when we balance the partition `P` of a finset `s`, any set `t` in this balanced partition has a size that's either `m` or `m+1`, where `m` is a factor of the size of `s`.
More concisely: For any finset `s` with decidable equality, given a finpartition `P` of `s` with a cardinality `m` factor that balances `s`, any set `t` in the equitabilised partition `P` has cardinality either `m` or `m+1`.
|