Finite-set infrastructure

• Finset.exists_nat_prod_lt bounds both coordinates of a finite set of pairs of natural numbers.
• Finset.exists_perm_eqOn_le_apply gives a permutation of ℕ fixing one finite set pointwise and carrying a disjoint one past any bound.
• TauCeti.product_union_eq_union_product rearranges a union of products of finsets.
• TauCeti.card_nonempty_finset counts the nonempty finsets of a finite type.
• TauCeti.card_even_card_finset and TauCeti.card_odd_card_finset count the finsets of a nonempty finite type by the parity of their cardinality: each parity accounts for exactly half of them.
• Finset.sum_powerset_neg_one_pow_card_of_ring evaluates the alternating sum over the subsets of a finset in an arbitrary ring.
• Finset.sum_powerset_neg_one_pow_mul_eq_zero pairs subsets that differ by one element to cancel a signed sum.
• Finset.sum_Icc_neg_one_pow_card_sub_card_left and Finset.sum_Icc_neg_one_pow_card_sub_card_right compute the Möbius function of the Boolean lattice of finsets: the signed sum over an interval [s, t] is 1 if s = t and 0 otherwise.
• Finset.card_symmDiff_add_two_mul_card_inter and Finset.even_card_symmDiff_iff compare the cardinality of a symmetric difference with the cardinalities of its two arguments: exactly, and modulo two.
• Finset.map_swap_pair, Finset.map_swap_pair_right and Finset.map_swap_eq_self_iff describe how a transposition moves a finset around, and Finset.mem_map_swap_symmDiff_pair_iff, Finset.involutive_map_swap_symmDiff_pair and Finset.map_swap_symmDiff_pair_eq_self_iff do the same for a transposition composed with the toggle of the two transposed points.
• Finset.sum_filter_le_sum_filter_le reindexes a double sum over chains in a finite type with a ≤ relation.
• Finset.sum_eq_two and Finset.sum_eq_four reduce a sum over a finite type, and a double sum over a pair of finite types, to the values of its summand at the two points where it is supported, and at the four cells of a rectangle.
• TauCeti.sum_piecewise_eq_sum_update_of_card_eq_succ reindexes a sum of Finset.piecewise terms over the subsets of size one less than card ι as a sum of Function.update terms over ι. It is what turns a formula indexed by "all but one point" into one indexed by the omitted point, as in the change-origin and derivative computations for multilinear series.

theorem TauCeti.product_union_eq_union_product {α : Type u_1} {β : Type u_2} {s s' : Finset α} {t t' : Finset β} [DecidableEq α] [DecidableEq β] : s ×ˢ t ∪ (s ∪ s') ×ˢ t' = s' ×ˢ t' ∪ s ×ˢ (t ∪ t')

A union of two products of finsets can be rearranged by distributing each product over its union coordinate.

theorem TauCeti.card_nonempty_finset {ι : Type u_1} [Finite ι] : Nat.card { S : Finset ι // S.Nonempty } = 2 ^ Nat.card ι - 1

The number of nonempty subsets of a finite type is 2ⁿ - 1. The 2ⁿ subsets of an n-element type are the nonempty ones together with the empty set, so the nonempty ones number 2ⁿ - 1.

theorem TauCeti.card_even_card_finset {ι : Type u_1} [Finite ι] : Nat.card { S : Finset ι // Even S.card } = 2 ^ (Nat.card ι - 1)

The subsets of even cardinality of a finite type number 2 ^ (n - 1). On a nonempty type that is half of all 2 ^ n subsets: deleting a fixed point from the subsets that contain it, and adjoining it to those that do not, is an involution of the subsets of ι reversing the parity of the cardinality, so the two parities are equinumerous and together exhaust the 2 ^ n subsets. The empty type is the exception to that halving, and is covered separately: it has no fixed point to flip, and its lone subset ∅ is even with no odd subset to pair it with, so the two parities are not equinumerous there — but 2 ^ (0 - 1) = 1 counts that one even subset all the same, which is why the statement needs no nonemptiness hypothesis. (Its odd counterpart TauCeti.card_odd_card_finset does need one: the empty type has no subset of odd cardinality.)

theorem TauCeti.card_odd_card_finset {ι : Type u_1} [Finite ι] [Nonempty ι] : Nat.card { S : Finset ι // Odd S.card } = 2 ^ (Nat.card ι - 1)

Exactly half the subsets of a nonempty finite type have odd cardinality, the other half of TauCeti.card_even_card_finset.

theorem Finset.card_symmDiff_add_two_mul_card_inter {α : Type u_1} [DecidableEq α] (s t : Finset α) : (symmDiff s t).card + 2 * (s ∩ t).card = s.card + t.card

The symmetric difference and the intersection account for both cardinalities. The symmetric difference is the union minus the intersection, and the union and the intersection together have the two cardinalities as their total.

@[simp]

theorem Finset.even_card_symmDiff_iff {α : Type u_1} [DecidableEq α] (s t : Finset α) : Even (symmDiff s t).card ↔ (Even s.card ↔ Even t.card)

A symmetric difference has even cardinality exactly when its two arguments have the same cardinality parity.

theorem Finset.map_swap_pair {α : Type u_1} [DecidableEq α] (a b : α) : map (Equiv.toEmbedding (Equiv.swap a b)) {a, b} = {a, b}

A transposition fixes the pair it transposes.

theorem Finset.map_swap_pair_right {α : Type u_1} [DecidableEq α] {a b c : α} (hca : c ≠ a) (hcb : c ≠ b) : map (Equiv.toEmbedding (Equiv.swap a b)) {b, c} = {a, c}

A transposition moves a pair along its first index, provided the second index is fixed.

theorem Finset.map_swap_eq_self_iff {α : Type u_1} [DecidableEq α] (a b : α) (s : Finset α) : map (Equiv.toEmbedding (Equiv.swap a b)) s = s ↔ (a ∈ s ↔ b ∈ s)

A transposition fixes a finset exactly when the two transposed points have the same membership.

theorem Finset.mem_map_swap_symmDiff_pair_iff {α : Type u_1} [DecidableEq α] (a b : α) (s : Finset α) (x : α) : x ∈ symmDiff (map (Equiv.toEmbedding (Equiv.swap a b)) s) {a, b} ↔ ((Equiv.swap a b) x ∈ s ↔ x ≠ a ∧ x ≠ b)

Membership in a transposed finset with the two transposed points toggled.

theorem Finset.involutive_map_swap_symmDiff_pair {α : Type u_1} [DecidableEq α] (a b : α) : Function.Involutive fun (s : Finset α) => symmDiff (map (Equiv.toEmbedding (Equiv.swap a b)) s) {a, b}

Transposing two points of a finset and toggling both is an involution.

theorem Finset.map_swap_symmDiff_pair_eq_self_iff {α : Type u_1} [DecidableEq α] (a b : α) (s : Finset α) : symmDiff (map (Equiv.toEmbedding (Equiv.swap a b)) s) {a, b} = s ↔ (a ∈ s ↔ b ∉ s)

Transposing two points of a finset and toggling both fixes it exactly when the two points have opposite membership.

theorem Finset.exists_nat_prod_lt (I : Finset (ℕ × ℕ)) : ∃ (n : ℕ), ∀ p ∈ I, p.1 < n ∧ p.2 < n

The two coordinates of every element of a finite set of natural-number pairs lie below a common bound.

theorem Finset.exists_perm_eqOn_le_apply (I J : Finset ℕ) (hIJ : Disjoint I J) (n : ℕ) : ∃ (ρ : Equiv.Perm ℕ), (∀ i ∈ I, ρ i = i) ∧ ∀ j ∈ J, n ≤ ρ j

A permutation of ℕ that fixes a finite set I pointwise and carries a finite set J, disjoint from I, past n.

theorem Finset.sum_filter_le_sum_filter_le {α : Type u_1} {M : Type u_2} [Fintype α] [LE α] [AddCommMonoid M] (a : α) (f : α → α → M) : ∑ b : α with a ≤ b, ∑ c : α with b ≤ c, f b c = ∑ c : α, ∑ b : α with a ≤ b ∧ b ≤ c, f b c

A double sum over a chain a ≤ b ≤ c, summed first over b and then over c, can instead be summed first over c and then over the interval of possible b.

@[simp]

theorem Finset.sum_powerset_neg_one_pow_card_of_ring {α : Type u_1} {R : Type u_2} [DecidableEq α] [Ring R] (s : Finset α) : ∑ t ∈ s.powerset, (-1) ^ t.card = if s = ∅ then 1 else 0

The alternating sum over the subsets of a finset is 1 for the empty finset and 0 otherwise, in an arbitrary ring. Mathlib's Finset.sum_powerset_neg_one_pow_card is the case of the integers.

theorem Finset.sum_powerset_neg_one_pow_mul_eq_zero {ι : Type u_1} {R : Type u_2} [DecidableEq ι] [Ring R] (P : Finset ι) (g h : ι → Finset ι → R) (hstep : ∀ i ∈ P, ∀ t ∈ (P.erase i).powerset, g i t = g i (insert i t) + h i (insert i t)) : ∑ T ∈ P.powerset, (-1) ^ T.card * (∑ i ∈ P, g i T + ∑ i ∈ T, h i T) = 0

A telescoping signed sum over the subsets of P vanishes. If, for each i ∈ P, the summand g i changes by h i when i is adjoined to a set not containing it, then ∑_{T ⊆ P} (-1)^{|T|} (∑_{i ∈ P} g i T + ∑_{i ∈ T} h i T) = 0: for fixed i, the sets T ∌ i and T ∪ {i} cancel in pairs.

@[simp]

theorem Finset.sum_Icc_neg_one_pow_card_sub_card_left {α : Type u_1} {R : Type u_2} [DecidableEq α] [Ring R] (s t : Finset α) : ∑ u ∈ Icc s t, (-1) ^ (u.card - s.card) = if s = t then 1 else 0

The Möbius function of the Boolean lattice, measured from the bottom. The sets between s and t are s ∪ u for u ⊆ t \ s, so the signed sum ∑_{s ⊆ u ⊆ t} (-1)^{|u| - |s|} is the alternating sum over the subsets of t \ s: it is 1 if s = t and 0 otherwise.

@[simp]

theorem Finset.sum_Icc_neg_one_pow_card_sub_card_right {α : Type u_1} {R : Type u_2} [DecidableEq α] [Ring R] (s t : Finset α) : ∑ u ∈ Icc s t, (-1) ^ (t.card - u.card) = if s = t then 1 else 0

The Möbius function of the Boolean lattice, measured from the top. The signed sum ∑_{s ⊆ u ⊆ t} (-1)^{|t| - |u|} is 1 if s = t and 0 otherwise: its terms differ from those of Finset.sum_Icc_neg_one_pow_card_sub_card_left by the common sign (-1)^{|t| - |s|}.

theorem Finset.sum_eq_two {α : Type u_1} {M : Type u_2} [Fintype α] [AddCommMonoid M] (f : α → M) (a b : α) (hab : a ≠ b) (h : ∀ (x : α), x ≠ a → x ≠ b → f x = 0) : ∑ x : α, f x = f a + f b

The sum over a finite type of a function that vanishes away from two distinct points is the sum of its values at those two points.

theorem Finset.sum_eq_four {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [Fintype κ] [AddCommMonoid M] (g : ι → κ → M) (i i' : ι) (j j' : κ) (hi'ne : i ≠ i') (hj'ne : j ≠ j') (h0 : ∀ (x : ι) (y : κ), ¬(x = i ∧ y = j) → ¬(x = i ∧ y = j') → ¬(x = i' ∧ y = j) → ¬(x = i' ∧ y = j') → g x y = 0) : ∑ x : ι, ∑ y : κ, g x y = g i j + g i j' + g i' j + g i' j'

The double sum over a pair of finite types of a function that vanishes outside the four cells of the rectangle i, i' by j, j' is the sum of its four values there.

theorem TauCeti.sum_piecewise_eq_sum_update_of_card_eq_succ {ι : Type u_1} {α : ι → Type u_2} {M : Type u_3} [Fintype ι] [DecidableEq ι] [AddCommMonoid M] {m : ℕ} (hm : Fintype.card ι = m + 1) (F : ((i : ι) → α i) → M) (f g : (i : ι) → α i) : ∑ s : { s : Finset ι // s.card = m }, F ((↑s).piecewise f g) = ∑ i : ι, F (Function.update f i (g i))

Summing over the subsets of size one less than card ι is summing over the points. Such a subset is the complement of a singleton, and Finset.piecewise against such a complement is Function.update at the missing point, so a sum of F over those subsets is a sum over ι.

Use it to turn a formula indexed by the subsets that omit a single point into one indexed by the omitted point.