Maps into the parts of a finite partition

Let P be a finite partition of a finset s and let ι be a finite index type. A map g : ι → α with values in s has a cell assignment i ↦ P.part (g i), and the maps whose cell assignment is a given φ : ι → P.parts form the box Fintype.piFinset fun i ↦ φ i. These boxes partition the maps ι → s, so sums over such maps split along cell assignments.

Counting lemmas for regular partitions treat the maps whose coordinates lie in distinct parts separately from the rest: a map with an injective cell assignment is itself injective, while the maps putting two coordinates in a common part are few when all parts are small. This file supplies both facts.

Main results

• Finpartition.sum_sum_piFinset_parts: a sum over maps ι → s splits along cell assignments.
• Finpartition.sum_piFinset_apply_part: a sum over maps ι → s of a function of their cell assignments weights each cell assignment by the size of its box.
• Finpartition.mem_piFinset_part_iff: a map lies in the box of parts through x exactly when it has the same cell assignment as x.
• Finpartition.injective_of_mem_piFinset_parts: a map in the box of an injective cell assignment is injective.
• Finpartition.card_filter_not_injective_part_le: at most (card ι).choose 2 * #s ^ (card ι - 2) * ∑ A ∈ P.parts, #A ^ 2 maps ι → s have a non-injective cell assignment.
• Finpartition.sum_prod_card_of_not_injective_le: the same bound for the total size of the boxes of non-injective cell assignments.
• Finpartition.card_filter_not_injective_part_le_of_card_le, Finpartition.sum_prod_card_of_not_injective_le_of_card_le: when all parts have size at most m, both counts are at most (card ι).choose 2 * m * #s ^ (card ι - 1).
• Finpartition.card_embedding_exists_mem_part_le_of_card_le: the same bound for the embeddings ι ↪ α sending two distinct points to a common part of a partition of a finite type α.

theorem Finpartition.pairwiseDisjoint_piFinset_parts {α : Type u_1} {ι : Type u_2} [DecidableEq α] [Fintype ι] [DecidableEq ι] {s : Finset α} (P : Finpartition s) : (↑Finset.univ).PairwiseDisjoint fun (φ : ι → ↥P.parts) => Fintype.piFinset fun (i : ι) => ↑(φ i)

The boxes of distinct cell assignments are disjoint.

theorem Finpartition.biUnion_piFinset_parts {α : Type u_1} {ι : Type u_2} [DecidableEq α] [Fintype ι] [DecidableEq ι] {s : Finset α} (P : Finpartition s) : (Finset.univ.biUnion fun (φ : ι → ↥P.parts) => Fintype.piFinset fun (i : ι) => ↑(φ i)) = Fintype.piFinset fun (x : ι) => s

The boxes of all cell assignments cover the maps ι → s.

theorem Finpartition.sum_sum_piFinset_parts {α : Type u_1} {ι : Type u_2} [DecidableEq α] [Fintype ι] [DecidableEq ι] {s : Finset α} (P : Finpartition s) {M : Type u_3} [AddCommMonoid M] (f : (ι → α) → M) : ∑ φ : ι → ↥P.parts, ∑ g ∈ Fintype.piFinset fun (i : ι) => ↑(φ i), f g = ∑ g ∈ Fintype.piFinset fun (x : ι) => s, f g

A sum over the maps ι → s splits along cell assignments.

theorem Finpartition.sum_card_filter_piFinset_parts {α : Type u_1} {ι : Type u_2} [DecidableEq α] [Fintype ι] [DecidableEq ι] {s : Finset α} (P : Finpartition s) (p : (ι → α) → Prop) [DecidablePred p] : ∑ φ : ι → ↥P.parts, {g ∈ Fintype.piFinset fun (i : ι) => ↑(φ i) | p g}.card = {g ∈ Fintype.piFinset fun (x : ι) => s | p g}.card

The maps ι → s with a given property are counted along cell assignments.

theorem Finpartition.injective_of_mem_piFinset_parts {α : Type u_1} {ι : Type u_2} [DecidableEq α] [Fintype ι] [DecidableEq ι] {s : Finset α} (P : Finpartition s) {φ : ι → ↥P.parts} (hφ : Function.Injective φ) {g : ι → α} (hg : g ∈ Fintype.piFinset fun (i : ι) => ↑(φ i)) : Function.Injective g

A map in the box of an injective cell assignment is injective.

theorem Finpartition.part_eq_of_mem_piFinset_parts {α : Type u_1} {ι : Type u_2} [DecidableEq α] [Fintype ι] [DecidableEq ι] {s : Finset α} (P : Finpartition s) {φ : ι → ↥P.parts} {g : ι → α} (hg : g ∈ Fintype.piFinset fun (i : ι) => ↑(φ i)) (i : ι) : P.part (g i) = ↑(φ i)

On the box of a cell assignment φ, the cell assignment of each map is φ.

theorem Finpartition.mem_piFinset_part_iff {α : Type u_1} {ι : Type u_2} [DecidableEq α] [Fintype ι] [DecidableEq ι] {s : Finset α} (P : Finpartition s) {x y : ι → α} (hx : ∀ (i : ι), x i ∈ s) : (y ∈ Fintype.piFinset fun (i : ι) => P.part (x i)) ↔ (fun (i : ι) => P.part (y i)) = fun (i : ι) => P.part (x i)

A map y lies in the box of parts through a map x : ι → s exactly when y has the same cell assignment as x.

theorem Finpartition.sum_piFinset_apply_part {α : Type u_1} {ι : Type u_2} [DecidableEq α] [Fintype ι] [DecidableEq ι] {s : Finset α} (P : Finpartition s) {M : Type u_3} [AddCommMonoid M] (f : (ι → Finset α) → M) : (∑ g ∈ Fintype.piFinset fun (x : ι) => s, f fun (i : ι) => P.part (g i)) = ∑ φ : ι → ↥P.parts, (∏ i : ι, (↑(φ i)).card) • f fun (i : ι) => ↑(φ i)

A sum over the maps ι → s of a function of their cell assignments counts each cell assignment φ with the size ∏ i, #(φ i) of its box.

theorem Finpartition.card_filter_part_eq_part_le {α : Type u_1} {ι : Type u_2} [DecidableEq α] [Fintype ι] [DecidableEq ι] {s : Finset α} (P : Finpartition s) {i j : ι} (hij : i ≠ j) : {g ∈ Fintype.piFinset fun (x : ι) => s | P.part (g i) = P.part (g j)}.card ≤ s.card ^ (Fintype.card ι - 2) * ∑ A ∈ P.parts, A.card ^ 2

At most #s ^ (card ι - 2) * ∑ A ∈ P.parts, #A ^ 2 maps ι → s send two given distinct coordinates to a common part.

theorem Finpartition.card_filter_not_injective_part_le {α : Type u_1} {ι : Type u_2} [DecidableEq α] [Fintype ι] [DecidableEq ι] {s : Finset α} (P : Finpartition s) : {g ∈ Fintype.piFinset fun (x : ι) => s | ¬Function.Injective fun (i : ι) => P.part (g i)}.card ≤ (Fintype.card ι).choose 2 * s.card ^ (Fintype.card ι - 2) * ∑ A ∈ P.parts, A.card ^ 2

At most (card ι).choose 2 * #s ^ (card ι - 2) * ∑ A ∈ P.parts, #A ^ 2 maps ι → s send two distinct coordinates to a common part.

theorem Finpartition.sum_prod_card_of_not_injective_le {α : Type u_1} {ι : Type u_2} [DecidableEq α] [Fintype ι] [DecidableEq ι] {s : Finset α} (P : Finpartition s) : ∑ φ : ι → ↥P.parts with ¬Function.Injective φ, ∏ i : ι, (↑(φ i)).card ≤ (Fintype.card ι).choose 2 * s.card ^ (Fintype.card ι - 2) * ∑ A ∈ P.parts, A.card ^ 2

The boxes of the non-injective cell assignments have total size at most (card ι).choose 2 * #s ^ (card ι - 2) * ∑ A ∈ P.parts, #A ^ 2.

theorem Finpartition.card_filter_not_injective_part_le_of_card_le {α : Type u_1} {ι : Type u_2} [DecidableEq α] [Fintype ι] [DecidableEq ι] {s : Finset α} (P : Finpartition s) {m : ℕ} (hm : ∀ A ∈ P.parts, A.card ≤ m) : {g ∈ Fintype.piFinset fun (x : ι) => s | ¬Function.Injective fun (i : ι) => P.part (g i)}.card ≤ (Fintype.card ι).choose 2 * m * s.card ^ (Fintype.card ι - 1)

If every part of P has at most m elements, at most (card ι).choose 2 * m * #s ^ (card ι - 1) maps ι → s send two distinct coordinates to a common part.

theorem Finpartition.sum_prod_card_of_not_injective_le_of_card_le {α : Type u_1} {ι : Type u_2} [DecidableEq α] [Fintype ι] [DecidableEq ι] {s : Finset α} (P : Finpartition s) {m : ℕ} (hm : ∀ A ∈ P.parts, A.card ≤ m) : ∑ φ : ι → ↥P.parts with ¬Function.Injective φ, ∏ i : ι, (↑(φ i)).card ≤ (Fintype.card ι).choose 2 * m * s.card ^ (Fintype.card ι - 1)

If every part of P has at most m elements, the boxes of the non-injective cell assignments have total size at most (card ι).choose 2 * m * #s ^ (card ι - 1).

theorem Finpartition.card_embedding_exists_mem_part_le_of_card_le {α : Type u_1} {ι : Type u_2} [DecidableEq α] [Fintype ι] [DecidableEq ι] [Fintype α] (P : Finpartition Finset.univ) {m : ℕ} (hm : ∀ A ∈ P.parts, A.card ≤ m) : {f : ι ↪ α | ∃ (i : ι) (j : ι), i ≠ j ∧ ∃ A ∈ P.parts, f i ∈ A ∧ f j ∈ A}.card ≤ (Fintype.card ι).choose 2 * m * Fintype.card α ^ (Fintype.card ι - 1)

If every part of a finite partition P of a finite type α has at most m elements, at most (card ι).choose 2 * m * card α ^ (card ι - 1) embeddings ι ↪ α send two distinct points to a common part.