4.4 More subtractive methods

4.4.1 Sums with varying signs

Definition 4.72

✓

Let \(n\in \mathbb {N}\) and \(d\in \mathbb {N}\). An \(n\)-tuple \(\left( x_{1},x_{2},\ldots ,x_{n}\right) \in \left[ d\right] ^{n}\) is said to be all-even if each element of \(\left[ d\right] \) occurs an even number of times in this \(n\)-tuple (i.e., if for each \(k\in \left[ d\right] \), the number of all \(i\in \left[ n\right] \) satisfying \(x_{i}=k\) is even).

docs source

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

Prop

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

In the Lean formalization, sign tuples \(\left(e_1, e_2, \ldots , e_d\right) \in \{ 1, -1\} ^d\) are represented as functions \(e : \operatorname {Fin} d \to \mathbb {Z}/2\mathbb {Z}\), where \(0\) represents \(+1\) and \(1\) represents \(-1\). The conversion is performed by a sign conversion function. The product \(e_{x_1} e_{x_2} \cdots e_{x_n}\) is represented by a sign product function, and the sum \(e_1 + e_2 + \cdots + e_d\) (in \(\mathbb {Z}\)) by a sign sum function.

Definition 4.73

✓

For an \(n\)-tuple \(x : \operatorname {Fin} n \to \operatorname {Fin} d\) and \(k \in \operatorname {Fin} d\), the multiplicity of \(k\) in \(x\) is the number of all \(i \in \operatorname {Fin} n\) satisfying \(x(i) = k\).

docs source

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

ℕ

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

Definition 4.74 Sign conversion

✓

The function \(\operatorname {toSign} : \mathbb {Z}/2\mathbb {Z} \to \mathbb {Z}\) converts elements of \(\mathbb {Z}/2\mathbb {Z}\) to signs: \(\operatorname {toSign}(0) = 1\) and \(\operatorname {toSign}(1) = -1\).

docs source

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

ℤ

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

Definition 4.75 Sign product

✓

For a sign tuple \(e : \operatorname {Fin} d \to \mathbb {Z}/2\mathbb {Z}\) and an index tuple \(x : \operatorname {Fin} n \to \operatorname {Fin} d\), the sign product is

\[ \operatorname {signProduct}(e, x) := \prod _{i=1}^{n} \operatorname {toSign}(e_{x_i}). \]

docs source

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

ℤ

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

Definition 4.76 Sign sum

✓

For a sign tuple \(e : \operatorname {Fin} d \to \mathbb {Z}/2\mathbb {Z}\), the sign sum is the integer

\[ \operatorname {signSum}(e) := \sum _{k=1}^{d} \operatorname {toSign}(e_k). \]

docs source

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

ℤ

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

Definition 4.77 Set of all-even tuples

✓

The set of all-even \(n\)-tuples in \([d]^n\) is

\[ \operatorname {allEvenTuples}(n, d) := \{ x \in (\operatorname {Fin} n \to \operatorname {Fin} d) \mid x \text{ is all-even}\} . \]

docs source

def AlgebraicCombinatorics.SubtractiveMethods.allEvenTuples (n d : ℕ) :

Finset (Fin n → Fin d)

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

Theorem 4.78

✓

Let \(n\in \mathbb {N}\) and \(d\in \mathbb {N}\). Then, the number of all all-even \(n\)-tuples \(\left( x_{1},x_{2},\ldots ,x_{n}\right) \in \left[ d\right] ^{n}\) is

\[ \frac{1}{2^{d}}\sum _{k=0}^{d}\binom {d}{k}\left( d-2k\right) ^{n}. \]

More precisely (avoiding division), the number of all-even \(n\)-tuples multiplied by \(2^d\) equals \(\sum _{k=0}^{d}\binom {d}{k}(d-2k)^n\).

docs source

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

Proof ▶

Lemma 4.80 yields

\begin{align*} & \sum _{\left( e_{1},e_{2},\ldots ,e_{d}\right) \in \left\{ 1,-1\right\} ^{d}}\left( e_{1}+e_{2}+\cdots +e_{d}\right) ^{n}\\ & =\sum _{\left( x_{1},x_{2},\ldots ,x_{n}\right) \in \left[ d\right] ^{n}}\ \ \sum _{\left( e_{1},e_{2},\ldots ,e_{d}\right) \in \left\{ 1,-1\right\} ^{d}}e_{x_{1}}e_{x_{2}}\cdots e_{x_{n}}. \end{align*}

By Lemma 4.90 (which splits according to whether each tuple is all-even or not, using Lemma 4.88 and Lemma 4.89), the right-hand side equals \((\text{\# of all-even tuples}) \cdot 2^d\).

On the other hand, a \(d\)-tuple \(\left( e_{1},e_{2},\ldots ,e_{d}\right) \in \left\{ 1,-1\right\} ^{d}\) is uniquely determined by the set \(S = \left\{ i\in \left[ d\right] \ \mid \ e_{i}=-1\right\} \), and for this tuple we have \(e_{1}+e_{2}+\cdots +e_{d}=d-2\left\vert S\right\vert \). By Lemma 4.96, we can rewrite the sum over sign tuples as a sum over subsets. By Lemma 4.97, grouping by cardinality \(|S| = k\) yields

\[ \sum _{\left( e_{1},e_{2},\ldots ,e_{d}\right) \in \left\{ 1,-1\right\} ^{d}}\left( e_{1}+e_{2}+\cdots +e_{d}\right) ^{n}=\sum _{k=0}^{d}\binom {d}{k}\left( d-2k\right) ^{n}. \]

Comparing the two expressions gives

\[ \left( \text{\# of all-even tuples}\right) \cdot 2^{d}=\sum _{k=0}^{d}\binom {d}{k}\left( d-2k\right) ^{n}. \]

4.4.2 Lemmas for the proof

Lemma 4.79

✓

Let \(n,d\in \mathbb {N}\). Let \(e = (e_1, \ldots , e_d) \in \{ 1,-1\} ^d\) and \(x = (x_1, \ldots , x_n) \in [d]^n\). For each \(k \in [d]\), let \(m_k\) be the multiplicity of \(k\) in \(x\). Then

\[ e_{x_{1}}e_{x_{2}}\cdots e_{x_{n}}=e_{1}^{m_{1}}e_{2}^{m_{2}}\cdots e_{d}^{m_{d}}. \]

docs source

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

Proof ▶

Each factor of the product \(e_{x_{1}}e_{x_{2}}\cdots e_{x_{n}}\) is one of the \(d\) entries \(e_{1},e_{2},\ldots ,e_{d}\). Moreover, each given entry \(e_{k}\) appears exactly \(m_{k}\) times in the product \(e_{x_{1}}e_{x_{2}}\cdots e_{x_{n}}\), because \(k\) appears exactly \(m_{k}\) times among the subscripts \(x_{1},x_{2},\ldots ,x_{n}\). Thus the product equals \(e_{1}^{m_{1}}e_{2}^{m_{2}}\cdots e_{d}^{m_{d}}\).

Lemma 4.80

✓

Let \(n,d\in \mathbb {N}\). Then,

docs source

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

Proof ▶

For each \(\left( e_{1},e_{2},\ldots ,e_{d}\right) \in \left\{ 1,-1\right\} ^{d}\), we have

\begin{align*} \left( e_{1}+e_{2}+\cdots +e_{d}\right) ^{n} & =\left( \sum _{k=1}^{d}e_{k}\right) ^{n} =\sum _{\left( x_{1},x_{2},\ldots ,x_{n}\right) \in \left[ d\right] ^{n}}e_{x_{1}}e_{x_{2}}\cdots e_{x_{n}} \end{align*}

(by the generalized distributive law / product rule). Summing over all \(\left( e_{1},e_{2},\ldots ,e_{d}\right) \in \left\{ 1,-1\right\} ^{d}\) and interchanging the order of summation yields the result.

Lemma 4.81

✓

Let \(n,d\in \mathbb {N}\). Let \(\left( x_{1},x_{2},\ldots ,x_{n}\right) \in \left[ d\right] ^{n}\).

(a) If the \(n\)-tuple \(\left( x_{1},x_{2},\ldots ,x_{n}\right)\) is not all-even, then \(\sum _{\left( e_{1},\ldots ,e_{d}\right) \in \left\{ 1,-1\right\} ^{d}} e_{x_{1}}e_{x_{2}}\cdots e_{x_{n}}=0\).

(b) If the \(n\)-tuple \(\left( x_{1},x_{2},\ldots ,x_{n}\right)\) is all-even, then \(\sum _{\left( e_{1},\ldots ,e_{d}\right) \in \left\{ 1,-1\right\} ^{d}} e_{x_{1}}e_{x_{2}}\cdots e_{x_{n}}=2^{d}\).

docs source

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

docs source

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

Proof ▶

This combines parts (a) and (b).

4.4.3 Involution argument for part (a)

Definition 4.82

✓

For \(k \in [d]\), the map \(\operatorname {flipSign}_k : \{ 1,-1\} ^d \to \{ 1,-1\} ^d\) sends a \(d\)-tuple \((e_1, \ldots , e_d)\) to the tuple obtained by flipping the sign of the \(k\)-th entry: i.e., replacing \(e_k\) by \(-e_k\) and leaving all other entries unchanged.

docs source

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

Fin d → ZMod 2

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

Lemma 4.83

✓

For any \(k \in [d]\), the map \(\operatorname {flipSign}_k\) is an involution.

docs source

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

Function.Involutive (flipSign k)

Proof ▶

Flipping the sign of the \(k\)-th entry twice restores the original sign.

Lemma 4.84

✓

For any \(k \in [d]\) and \(e \in \{ 1,-1\} ^d\), we have \(\operatorname {flipSign}_k(e) \neq e\).

docs source

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

flipSign k e ≠ e

Proof ▶

Since \(e_k \in \{ 1, -1\} \), flipping the sign of \(e_k\) produces a different value (\(-e_k \neq e_k\)), so the resulting tuple differs from the original.

Lemma 4.85 flipSign at the flipped position

✓

For any \(k \in [d]\) and \(e \in \{ 1,-1\} ^d\), \((\operatorname {flipSign}_k(e))_k = e_k + 1\) (in \(\mathbb {Z}/2\mathbb {Z}\)).

docs source

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

flipSign k e k = e k + 1

Proof ▶

By definition of \(\operatorname {flipSign}\), which updates position \(k\).

Lemma 4.86 flipSign leaves other positions unchanged

✓

For any \(k, j \in [d]\) with \(j \neq k\) and \(e \in \{ 1,-1\} ^d\), \((\operatorname {flipSign}_k(e))_j = e_j\).

docs source

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

Proof ▶

The update only affects position \(k\), so all other positions are unchanged.

Lemma 4.87

✓

Let \(e \in \{ 1,-1\} ^d\), \(x \in [d]^n\), and \(k \in [d]\) such that the multiplicity \(m_k\) of \(k\) in \(x\) is odd. Then

\[ \operatorname {signProduct}(\operatorname {flipSign}_k(e), x) = -\operatorname {signProduct}(e, x). \]

docs source

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

Proof ▶

Using the product-of-powers representation (Lemma 4.79), flipping the \(k\)-th entry multiplies the product by \((-1)^{m_k} = -1\) (since \(m_k\) is odd), while all other factors remain unchanged.

Lemma 4.88

✓

Let \(n,d\in \mathbb {N}\). Let \(\left( x_{1},x_{2},\ldots ,x_{n}\right) \in \left[ d\right] ^{n}\). If the \(n\)-tuple \(\left( x_{1},x_{2},\ldots ,x_{n}\right) \) is not all-even, then

\[ \sum _{\left( e_{1},e_{2},\ldots ,e_{d}\right) \in \left\{ 1,-1\right\} ^{d}}e_{x_{1}}e_{x_{2}}\cdots e_{x_{n}}=0. \]

docs source

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

Proof ▶

Since the tuple is not all-even, there exists some \(k\in \left[ d\right] \) such that \(m_{k}\) is odd.

Define \(f:\left\{ 1,-1\right\} ^{d}\rightarrow \left\{ 1,-1\right\} ^{d}\) as \(\operatorname {flipSign}_k\) (flipping the sign of the \(k\)-th entry). By Lemma 4.83, \(f\) is an involution. By Lemma 4.84, \(f\) has no fixed points. By Lemma 4.87, \(\operatorname {signProduct}(f(e), x) = -\operatorname {signProduct}(e, x)\).

Hence, the terms cancel in pairs, giving

\[ \sum _{\left( e_{1},e_{2},\ldots ,e_{d}\right) \in \left\{ 1,-1\right\} ^{d}}e_{x_{1}}e_{x_{2}}\cdots e_{x_{n}}=0. \]

The Lean proof uses the involution summation lemma from Mathlib.

Lemma 4.89

✓

Let \(n,d\in \mathbb {N}\). Let \(\left( x_{1},x_{2},\ldots ,x_{n}\right) \in \left[ d\right] ^{n}\). If the \(n\)-tuple \(\left( x_{1},x_{2},\ldots ,x_{n}\right) \) is all-even, then

\[ \sum _{\left( e_{1},e_{2},\ldots ,e_{d}\right) \in \left\{ 1,-1\right\} ^{d}}e_{x_{1}}e_{x_{2}}\cdots e_{x_{n}}=2^{d}. \]

docs source

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

Proof ▶

Since the tuple is all-even, all the multiplicities \(m_{1},m_{2},\ldots ,m_{d}\) are even.

Let \(\left( e_{1},e_{2},\ldots ,e_{d}\right) \in \left\{ 1,-1\right\} ^{d}\). For each \(k\in \left[ d\right] \), we have \(e_{k}\in \left\{ 1,-1\right\} \) and \(m_{k}\) is even, so \(e_{k}^{m_{k}}=1\). By Lemma 4.79, \(e_{x_{1}}e_{x_{2}}\cdots e_{x_{n}} = e_{1}^{m_{1}}e_{2}^{m_{2}}\cdots e_{d}^{m_{d}} = 1\).

Since every sign product equals \(1\) and there are \(2^d\) sign tuples,

\[ \sum _{\left( e_{1},e_{2},\ldots ,e_{d}\right) \in \left\{ 1,-1\right\} ^{d}}e_{x_{1}}e_{x_{2}}\cdots e_{x_{n}}=2^{d}. \]

Lemma 4.90

✓

Let \(n,d\in \mathbb {N}\). Then

\[ \sum _{\left( x_{1},x_{2},\ldots ,x_{n}\right) \in \left[ d\right] ^{n}}\ \ \sum _{\left( e_{1},e_{2},\ldots ,e_{d}\right) \in \left\{ 1,-1\right\} ^{d}}e_{x_{1}}e_{x_{2}}\cdots e_{x_{n}} = \left(\text{\# of all-even tuples in } [d]^n\right) \cdot 2^d. \]

docs source

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

Proof ▶

Split the outer sum according to whether each tuple is all-even or not. By Lemma 4.88, the non-all-even tuples contribute \(0\). By Lemma 4.89, each all-even tuple contributes \(2^d\). Hence the total is \((\text{\# of all-even tuples}) \cdot 2^d\).

4.4.4 Computing the left-hand side

Lemma 4.91

✓

For a sign tuple \(e \in \{ 1,-1\} ^d\), let \(S = \{ i \in [d] \mid e_i = -1\} \). Then

\[ e_1 + e_2 + \cdots + e_d = d - 2|S|. \]

docs source

theorem AlgebraicCombinatorics.SubtractiveMethods.signSum_eq_card {d : ℕ} (e : Fin d → ZMod 2) :

signSum e = ↑d - 2 * ↑(signTupleToSubset e).card

Proof ▶

Each entry \(e_i\) equals \(-1\) if \(i \in S\) and \(1\) if \(i \notin S\). The sum has \(|S|\) addends equal to \(-1\) and \(d - |S|\) addends equal to \(1\), giving \(|S| \cdot (-1) + (d - |S|) \cdot 1 = d - 2|S|\).

Definition 4.92 Sign tuple to subset

✓

The map \(\operatorname {signTupleToSubset} : (\operatorname {Fin} d \to \mathbb {Z}/2\mathbb {Z}) \to \mathcal{P}(\operatorname {Fin} d)\) sends a sign tuple \(e\) to the set \(S = \{ k \in \operatorname {Fin} d \mid e_k = 1\} \) (i.e., the positions where \(\operatorname {toSign}(e_k) = -1\)).

docs source

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

Finset (Fin d)

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

Definition 4.93 Subset to sign tuple

✓

The inverse map \(\operatorname {subsetToSignTuple} : \mathcal{P}(\operatorname {Fin} d) \to (\operatorname {Fin} d \to \mathbb {Z}/2\mathbb {Z})\) sends a subset \(S \subseteq \operatorname {Fin} d\) to the sign tuple where position \(k\) has value \(1\) (representing \(-1\)) if \(k \in S\), and \(0\) (representing \(+1\)) otherwise.

docs source

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

Fin d → ZMod 2

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

Lemma 4.94

✓

There is a bijection between sign tuples \(\{ 1,-1\} ^d\) and subsets of \([d]\), sending each tuple \(e\) to the set \(S = \{ i \in [d] \mid e_i = -1\} \).

docs source

def AlgebraicCombinatorics.SubtractiveMethods.signTupleEquivSubset (d : ℕ) :

(Fin d → ZMod 2) ≃ Finset (Fin d)

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

Proof ▶

The inverse sends a subset \(S \subseteq [d]\) to the sign tuple where position \(k\) has \(e_k = -1\) if \(k \in S\) and \(e_k = 1\) otherwise.

Lemma 4.95 Sign sum under the subset correspondence

✓

For a subset \(S \subseteq [d]\), the sign sum of the corresponding sign tuple is

\[ \operatorname {signSum}(\operatorname {subsetToSignTuple}(S)) = d - 2|S|. \]

docs source

theorem AlgebraicCombinatorics.SubtractiveMethods.signSum_subsetToSignTuple {d : ℕ} (S : Finset (Fin d)) :

signSum (subsetToSignTuple S) = ↑d - 2 * ↑S.card

Proof ▶

By Lemma 4.91, the sign sum equals \(d - 2|T|\) where \(T = \operatorname {signTupleToSubset}(\operatorname {subsetToSignTuple}(S)) = S\).

Lemma 4.96

✓

Let \(n,d\in \mathbb {N}\). Then

\[ \sum _{\left( e_{1},e_{2},\ldots ,e_{d}\right) \in \left\{ 1,-1\right\} ^{d}}\left( e_{1}+e_{2}+\cdots +e_{d}\right) ^{n}=\sum _{S\subseteq \left[ d\right] }\left( d-2\left\vert S\right\vert \right) ^{n}. \]

docs source

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

Proof ▶

Substitute via the bijection of Lemma 4.94 and use Lemma 4.91.

Lemma 4.97

✓

Let \(n,d\in \mathbb {N}\). Then

\[ \sum _{S\subseteq \left[ d\right] }\left( d-2\left\vert S\right\vert \right) ^{n} = \sum _{k=0}^{d}\binom {d}{k}\left( d-2k\right) ^{n}. \]

docs source

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

Proof ▶

Split the sum over subsets \(S\) according to the value of \(|S| = k\). For each \(k\), all subsets of size \(k\) contribute the same summand \((d-2k)^n\), and the number of \(k\)-element subsets of \([d]\) is \(\binom {d}{k}\).

4.4.5 Helper lemmas for toSign

Lemma 4.98

✓

For any \(b \in \mathbb {Z}/2\mathbb {Z}\), we have \((\operatorname {toSign} b)^2 = 1\).

docs source

theorem AlgebraicCombinatorics.SubtractiveMethods.toSign_sq (b : ZMod 2) :

toSign b ^ 2 = 1

Proof ▶

By case analysis: both \(1^2 = 1\) and \((-1)^2 = 1\).

Lemma 4.99

✓

For any \(b \in \mathbb {Z}/2\mathbb {Z}\) and even \(m \in \mathbb {N}\), we have \((\operatorname {toSign} b)^m = 1\).

docs source

theorem AlgebraicCombinatorics.SubtractiveMethods.toSign_pow_even (b : ZMod 2) (m : ℕ) (hm : Even m) :

toSign b ^ m = 1

Proof ▶

Write \(m = 2k\). Then \((\operatorname {toSign} b)^m = ((\operatorname {toSign} b)^2)^k = 1^k = 1\).

Lemma 4.100 Odd powers of a sign

✓

For any \(b \in \mathbb {Z}/2\mathbb {Z}\) and odd \(m \in \mathbb {N}\), we have \((\operatorname {toSign} b)^m = \operatorname {toSign} b\).

docs source

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

toSign b ^ m = toSign b

Proof ▶

Write \(m = 2k + 1\). Then \((\operatorname {toSign} b)^m = ((\operatorname {toSign} b)^2)^k \cdot \operatorname {toSign} b = 1^k \cdot \operatorname {toSign} b = \operatorname {toSign} b\).

Lemma 4.101

✓

For any \(b \in \mathbb {Z}/2\mathbb {Z}\), we have \(\operatorname {toSign}(b+1) = -\operatorname {toSign}(b)\).

docs source

theorem AlgebraicCombinatorics.SubtractiveMethods.toSign_add_one (b : ZMod 2) :

toSign (b + 1) = -toSign b

Proof ▶

By case analysis on \(b \in \{ 0, 1\} \): adding \(1\) in \(\mathbb {Z}/2\mathbb {Z}\) toggles between \(0\) and \(1\), and \(\operatorname {toSign}(0) = 1 = -(-1) = -\operatorname {toSign}(1)\) while \(\operatorname {toSign}(1) = -1 = -(1) = -\operatorname {toSign}(0)\).

4.4.6 Corollaries of the counting formula

Corollary 4.102 Divisibility by \(2^d\)

✓

For any \(n, d \in \mathbb {N}\), we have

\[ 2^d \mid \sum _{k=0}^{d} \binom {d}{k} (d - 2k)^n. \]

docs source

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

Proof ▶

By Theorem 4.78, the sum equals \((\text{\# of all-even tuples}) \cdot 2^d\), which is divisible by \(2^d\).

Corollary 4.103 Nonnegativity

✓

For any \(n, d \in \mathbb {N}\), we have

\[ \sum _{k=0}^{d} \binom {d}{k} (d - 2k)^n \geq 0. \]

This is not obvious from the formula when \(n\) is odd, since the summands can be negative.

docs source

theorem AlgebraicCombinatorics.SubtractiveMethods.sum_choose_pow_nonneg (n d : ℕ) :

0 ≤ ∑ k ∈ Finset.range (d + 1), ↑(d.choose k) * (↑d - 2 * ↑k) ^ n

Proof ▶

By Theorem 4.78, the sum equals \((\text{\# of all-even tuples}) \cdot 2^d\), which is a product of two nonnegative integers.