More Subtractive Methods

This file formalizes Section sec.cancel.moresub on more subtractive methods in combinatorics, focusing on the technique of summing with varying signs to achieve cancellation.

Main definitions

• IsAllEven: An n-tuple x : Fin n → Fin d is "all-even" if each element of Fin d occurs an even number of times in the tuple.
• signProduct: The product e_{x_1} * e_{x_2} * ... * e_{x_n} for a sign tuple e and index tuple x.
• signSum: The sum of entries of a sign tuple, as an integer.
• allEvenTuples: The set of all-even tuples in (Fin n → Fin d).
• signTupleEquivSubset: Equivalence between sign tuples and subsets of [d].

Main results

• sum_signSum_pow_eq_sum_signProduct: Sum interchange identity (Lemma lem.cancel.all-even.l1).
• sum_signProduct_not_allEven: If an n-tuple is not all-even, then the sum ∑_{e ∈ {1,-1}^d} ∏_i e_{x_i} equals 0 (Lemma lem.cancel.all-even.l2(a)).
• sum_signProduct_allEven: If an n-tuple is all-even, then the sum ∑_{e ∈ {1,-1}^d} ∏_i e_{x_i} equals 2^d (Lemma lem.cancel.all-even.l2(b)).
• allEven_count_formula: The number of all-even n-tuples in [d]^n equals (1/2^d) ∑_{k=0}^d C(d,k) (d-2k)^n (Theorem thm.cancel.all-even).
• sum_choose_pow_dvd_pow_two: The sum ∑_{k=0}^d C(d,k) (d-2k)^n is divisible by 2^d.
• sum_choose_pow_nonneg: The sum ∑_{k=0}^d C(d,k) (d-2k)^n is nonnegative.

References

• Source: AlgebraicCombinatorics/tex/SignedCounting/SubtractiveMethods.tex

The all-even property

An n-tuple (x₁, x₂, ..., xₙ) ∈ [d]ⁿ is called "all-even" if each element of [d] occurs an even number of times in the tuple.

def AlgebraicCombinatorics.SubtractiveMethods.IsAllEven {n d : ℕ} (x : Fin n → Fin d) : Prop

An n-tuple x : Fin n → Fin d is "all-even" if each element of Fin d occurs an even number of times. For example, the 4-tuple (1,4,4,1) is all-even since 1 appears twice and 4 appears twice.

Label: Definition from Theorem thm.cancel.all-even

Equations

• AlgebraicCombinatorics.SubtractiveMethods.IsAllEven x = ∀ (k : Fin d), Even {i : Fin n | x i = k}.card

def AlgebraicCombinatorics.SubtractiveMethods.multiplicity {n d : ℕ} (x : Fin n → Fin d) (k : Fin d) : ℕ

The multiplicity of element k in tuple x

Equations

• AlgebraicCombinatorics.SubtractiveMethods.multiplicity x k = {i : Fin n | x i = k}.card

theorem AlgebraicCombinatorics.SubtractiveMethods.isAllEven_iff_multiplicity {n d : ℕ} (x : Fin n → Fin d) : IsAllEven x ↔ ∀ (k : Fin d), Even (multiplicity x k)

A tuple is all-even iff all multiplicities are even

instance AlgebraicCombinatorics.SubtractiveMethods.instDecidableIsAllEven {n d : ℕ} (x : Fin n → Fin d) : Decidable (IsAllEven x)

Equations

• AlgebraicCombinatorics.SubtractiveMethods.instDecidableIsAllEven x = inferInstanceAs (Decidable (∀ (k : Fin d), Even {i : Fin n | x i = k}.card))

Sign tuples

We represent sign tuples as functions e : Fin d → ZMod 2, where 0 represents +1 and 1 represents -1. This gives us a natural finite type structure. We then convert to ℤ when needed.

def AlgebraicCombinatorics.SubtractiveMethods.toSign (b : ZMod 2) : ℤ

Convert a ZMod 2 value to a sign: 0 ↦ 1, 1 ↦ -1

Equations

• AlgebraicCombinatorics.SubtractiveMethods.toSign b = if b = 0 then 1 else -1

@[simp]

theorem AlgebraicCombinatorics.SubtractiveMethods.toSign_zero : toSign 0 = 1

@[simp]

theorem AlgebraicCombinatorics.SubtractiveMethods.toSign_one : toSign 1 = -1

def AlgebraicCombinatorics.SubtractiveMethods.signProduct {n d : ℕ} (e : Fin d → ZMod 2) (x : Fin n → Fin d) : ℤ

The product e_{x_1} * e_{x_2} * ... * e_{x_n} for a sign tuple e and index tuple x

Equations

• AlgebraicCombinatorics.SubtractiveMethods.signProduct e x = ∏ i : Fin n, AlgebraicCombinatorics.SubtractiveMethods.toSign (e (x i))

Helper lemmas about toSign and powers

theorem AlgebraicCombinatorics.SubtractiveMethods.toSign_sq (b : ZMod 2) : toSign b ^ 2 = 1

The square of any sign is 1

theorem AlgebraicCombinatorics.SubtractiveMethods.toSign_pow_even (b : ZMod 2) (m : ℕ) (hm : Even m) : toSign b ^ m = 1

Even powers of a sign equal 1

theorem AlgebraicCombinatorics.SubtractiveMethods.toSign_pow_odd (b : ZMod 2) (m : ℕ) (hm : Odd m) : toSign b ^ m = toSign b

Odd powers of a sign equal the sign itself

theorem AlgebraicCombinatorics.SubtractiveMethods.toSign_add_one (b : ZMod 2) : toSign (b + 1) = -toSign b

Adding 1 in ZMod 2 flips the sign

theorem AlgebraicCombinatorics.SubtractiveMethods.signProduct_eq_prod_pow {n d : ℕ} (e : Fin d → ZMod 2) (x : Fin n → Fin d) : signProduct e x = ∏ k : Fin d, toSign (e k) ^ multiplicity x k

The product can be rewritten in terms of multiplicities: ∏_i e_{x_i} = ∏_k e_k^{m_k} where m_k is the multiplicity of k in x.

Label: Equation pf.lem.cancel.all-even.l2.e=e

Lemma lem.cancel.all-even.l1: Sum interchange

This lemma establishes that:

∑_{e ∈ {1,-1}^d} (e_1 + e_2 + ... + e_d)^n =
  ∑_{x ∈ [d]^n} ∑_{e ∈ {1,-1}^d} e_{x_1} * e_{x_2} * ... * e_{x_n}

def AlgebraicCombinatorics.SubtractiveMethods.signSum {d : ℕ} (e : Fin d → ZMod 2) : ℤ

The sum of entries of a sign tuple, as an integer

Equations

• AlgebraicCombinatorics.SubtractiveMethods.signSum e = ∑ k : Fin d, AlgebraicCombinatorics.SubtractiveMethods.toSign (e k)

theorem AlgebraicCombinatorics.SubtractiveMethods.sum_signSum_pow_eq_sum_signProduct (n d : ℕ) : ∑ e : Fin d → ZMod 2, signSum e ^ n = ∑ x : Fin n → Fin d, ∑ e : Fin d → ZMod 2, signProduct e x

Sum interchange identity (Lemma lem.cancel.all-even.l1): The sum over sign tuples of (∑_k e_k)^n equals the double sum over index tuples and sign tuples of the sign product.

This follows from expanding (∑_k e_k)^n using the distributive law.

Label: Lemma lem.cancel.all-even.l1

Lemma lem.cancel.all-even.l2: Computing the inner sums

Part (a): If the tuple is not all-even, the sum of sign products is 0. Part (b): If the tuple is all-even, the sum of sign products is 2^d.

The involution for cancellation

We define an involution on sign tuples that flips the sign at position k. This is used to show cancellation when the tuple has odd multiplicity at k.

def AlgebraicCombinatorics.SubtractiveMethods.flipSign {d : ℕ} (k : Fin d) (e : Fin d → ZMod 2) : Fin d → ZMod 2

The involution that flips the k-th sign: if e_k = +1, make it -1, and vice versa

Equations

• AlgebraicCombinatorics.SubtractiveMethods.flipSign k e = Function.update e k (e k + 1)

theorem AlgebraicCombinatorics.SubtractiveMethods.flipSign_involutive {d : ℕ} (k : Fin d) : Function.Involutive (flipSign k)

flipSign is an involution

theorem AlgebraicCombinatorics.SubtractiveMethods.flipSign_ne {d : ℕ} (k : Fin d) (e : Fin d → ZMod 2) : flipSign k e ≠ e

flipSign produces a different tuple

theorem AlgebraicCombinatorics.SubtractiveMethods.flipSign_self {d : ℕ} (k : Fin d) (e : Fin d → ZMod 2) : flipSign k e k = e k + 1

flipSign at position k gives e_k + 1 at position k

theorem AlgebraicCombinatorics.SubtractiveMethods.flipSign_ne_self {d : ℕ} (k j : Fin d) (e : Fin d → ZMod 2) (h : j ≠ k) : flipSign k e j = e j

flipSign at position k leaves other positions unchanged

theorem AlgebraicCombinatorics.SubtractiveMethods.signProduct_flipSign {n d : ℕ} (e : Fin d → ZMod 2) (x : Fin n → Fin d) (k : Fin d) (hk : Odd (multiplicity x k)) : signProduct (flipSign k e) x = -signProduct e x

Key lemma: flipping sign k negates the sign product when k has odd multiplicity

theorem AlgebraicCombinatorics.SubtractiveMethods.sum_signProduct_not_allEven {n d : ℕ} (x : Fin n → Fin d) (hx : ¬IsAllEven x) : ∑ e : Fin d → ZMod 2, signProduct e x = 0

If an n-tuple is not all-even, then the sum over all sign tuples of the sign product is zero (Lemma lem.cancel.all-even.l2(a)).

The proof uses an involution argument: if some element k has odd multiplicity, flipping the sign of e_k negates the product, so terms cancel in pairs.

Label: Lemma lem.cancel.all-even.l2(a)

theorem AlgebraicCombinatorics.SubtractiveMethods.sum_signProduct_allEven {n d : ℕ} (x : Fin n → Fin d) (hx : IsAllEven x) : ∑ e : Fin d → ZMod 2, signProduct e x = 2 ^ d

If an n-tuple is all-even, then the sum over all sign tuples of the sign product equals 2^d (Lemma lem.cancel.all-even.l2(b)).

The proof: when all multiplicities are even, each e_k^{m_k} = 1 (since (±1)^{even} = 1), so every sign product equals 1, and there are 2^d sign tuples.

Label: Lemma lem.cancel.all-even.l2(b)

Theorem thm.cancel.all-even: The counting formula

The number of all-even n-tuples in [d]^n equals (1/2^d) ∑_{k=0}^d C(d,k) (d-2k)^n.

def AlgebraicCombinatorics.SubtractiveMethods.allEvenTuples (n d : ℕ) : Finset (Fin n → Fin d)

The set of all-even tuples in (Fin n → Fin d)

Equations

• AlgebraicCombinatorics.SubtractiveMethods.allEvenTuples n d = Finset.filter AlgebraicCombinatorics.SubtractiveMethods.IsAllEven Finset.univ

def AlgebraicCombinatorics.SubtractiveMethods.signTupleToSubset {d : ℕ} (e : Fin d → ZMod 2) : Finset (Fin d)

Bijection between sign tuples and subsets of [d]: A sign tuple (e_1, ..., e_d) ∈ {1,-1}^d corresponds to the set {i ∈ [d] | e_i = -1} of positions with -1.

Equations

• AlgebraicCombinatorics.SubtractiveMethods.signTupleToSubset e = {k : Fin d | e k = 1}

theorem AlgebraicCombinatorics.SubtractiveMethods.signSum_eq_card {d : ℕ} (e : Fin d → ZMod 2) : signSum e = ↑d - 2 * ↑(signTupleToSubset e).card

For a sign tuple corresponding to subset S, the sum of entries equals d - 2|S|.

Bijection between sign tuples and subsets

def AlgebraicCombinatorics.SubtractiveMethods.subsetToSignTuple {d : ℕ} (S : Finset (Fin d)) : Fin d → ZMod 2

Inverse of signTupleToSubset: given a subset S, produce the sign tuple where position k has value 1 (representing -1) iff k ∈ S

Equations

• AlgebraicCombinatorics.SubtractiveMethods.subsetToSignTuple S k = if k ∈ S then 1 else 0

theorem AlgebraicCombinatorics.SubtractiveMethods.signTupleToSubset_subsetToSignTuple {d : ℕ} (S : Finset (Fin d)) : signTupleToSubset (subsetToSignTuple S) = S

theorem AlgebraicCombinatorics.SubtractiveMethods.subsetToSignTuple_signTupleToSubset {d : ℕ} (e : Fin d → ZMod 2) : subsetToSignTuple (signTupleToSubset e) = e

def AlgebraicCombinatorics.SubtractiveMethods.signTupleEquivSubset (d : ℕ) : (Fin d → ZMod 2) ≃ Finset (Fin d)

Equivalence between sign tuples and subsets of [d]

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicCombinatorics.SubtractiveMethods.signSum_subsetToSignTuple {d : ℕ} (S : Finset (Fin d)) : signSum (subsetToSignTuple S) = ↑d - 2 * ↑S.card

For a subset S, the sign sum of the corresponding tuple equals d - 2|S|

theorem AlgebraicCombinatorics.SubtractiveMethods.sum_signProduct_eq_allEven_count (n d : ℕ) : ∑ x : Fin n → Fin d, ∑ e : Fin d → ZMod 2, signProduct e x = ↑(allEvenTuples n d).card * 2 ^ d

Compute the double sum using lemma l2

theorem AlgebraicCombinatorics.SubtractiveMethods.sum_signSum_pow_eq_sum_subset (n d : ℕ) : ∑ e : Fin d → ZMod 2, signSum e ^ n = ∑ S : Finset (Fin d), (↑d - 2 * ↑S.card) ^ n

Rewrite sum over sign tuples as sum over subsets

theorem AlgebraicCombinatorics.SubtractiveMethods.sum_subset_eq_sum_choose (n d : ℕ) : ∑ S : Finset (Fin d), (↑d - 2 * ↑S.card) ^ n = ∑ k ∈ Finset.range (d + 1), ↑(d.choose k) * (↑d - 2 * ↑k) ^ n

Group sum over subsets by cardinality

theorem AlgebraicCombinatorics.SubtractiveMethods.allEven_count_formula (n d : ℕ) : ↑(allEvenTuples n d).card * 2 ^ d = ∑ k ∈ Finset.range (d + 1), ↑(d.choose k) * (↑d - 2 * ↑k) ^ n

The main counting formula (Theorem thm.cancel.all-even): The number of all-even n-tuples in (Fin n → Fin d) equals (1/2^d) ∑_{k=0}^d C(d,k) (d-2k)^n.

This formula implies that ∑_{k=0}^d C(d,k) (d-2k)^n is nonnegative and divisible by 2^d, which is not obvious from the formula itself due to the alternating signs when n is odd.

Label: Theorem thm.cancel.all-even

theorem AlgebraicCombinatorics.SubtractiveMethods.sum_choose_pow_dvd_pow_two (n d : ℕ) : 2 ^ d ∣ ∑ k ∈ Finset.range (d + 1), ↑(d.choose k) * (↑d - 2 * ↑k) ^ n

Corollary: The sum ∑_{k=0}^d C(d,k) (d-2k)^n is divisible by 2^d.

theorem AlgebraicCombinatorics.SubtractiveMethods.sum_choose_pow_nonneg (n d : ℕ) : 0 ≤ ∑ k ∈ Finset.range (d + 1), ↑(d.choose k) * (↑d - 2 * ↑k) ^ n

Corollary: The sum ∑_{k=0}^d C(d,k) (d-2k)^n is nonnegative.