Parity Function and Imbalance Lemma

The parity function and its interaction with Boolean functions and sensitivity.

Main results

• parity_flipBit — flipping a bit negates the parity
• moebius_parity_sum — the Möbius coefficient relates to parity-weighted sum
• fullDegree_imbalance — if f has full degree n, one "parity-sign class" has more than half the vertices

def Sensitivity.parity {n : ℕ} (x : Fin n → Bool) : ℤ

Parity: (-1)^(number of true bits).

Equations

• Sensitivity.parity x = (-1) ^ {i : Fin n | x i = true}.card

def Sensitivity.BoolFun.pmOne {n : ℕ} (f : BoolFun n) (x : Fin n → Bool) : ℤ

±1 encoding of a Boolean function: true ↦ 1, false ↦ -1.

Equations

• f.pmOne x = if f x = true then 1 else -1

def Sensitivity.BoolFun.paritySigned {n : ℕ} (f : BoolFun n) (x : Fin n → Bool) : ℤ

The parity-signed function: g(x) = f_pm(x) · parity(x).

Equations

• f.paritySigned x = f.pmOne x * Sensitivity.parity x

theorem Sensitivity.BoolFun.pmOne_ne_zero {n : ℕ} (f : BoolFun n) (x : Fin n → Bool) : f.pmOne x ≠ 0

theorem Sensitivity.parity_ne_zero {n : ℕ} (x : Fin n → Bool) : parity x ≠ 0

theorem Sensitivity.parity_flipBit {n : ℕ} (x : Fin n → Bool) (i : Fin n) : parity (flipBit x i) = -parity x

Flipping a bit negates the parity.

theorem Sensitivity.BoolFun.sensitiveAt_of_paritySigned_eq {n : ℕ} (f : BoolFun n) (x : Fin n → Bool) (i : Fin n) (h : f.paritySigned (flipBit x i) = f.paritySigned x) : f.sensitiveAt x i

If paritySigned is the same at x and flipBit x i, then f is sensitive there.

Proof: parity flips sign under flipBit. If f_pm · parity stays the same, f_pm must also flip, so f changes value.

theorem Sensitivity.moebius_parity_sum {n : ℕ} (f : BoolFun n) (hn : 0 < n) : ∑ x : Fin n → Bool, f.paritySigned x = 2 * (-1) ^ n * f.moebius Finset.univ

Key identity: the parity-weighted sum relates to the top Möbius coefficient. ∑x f_pm(x) · parity(x) = 2 · (-1)^n · c{univ}(f).

This follows from expanding the Möbius coefficients and using the bijection between Boolean vectors and subsets.

theorem Sensitivity.fullDegree_paritySigned_sum_ne_zero {n : ℕ} (f : BoolFun n) (hn : 0 < n) (h : f.moebius Finset.univ ≠ 0) : ∑ x : Fin n → Bool, f.paritySigned x ≠ 0

If f has full degree (moebius at univ ≠ 0), the parity-weighted sum is nonzero.

theorem Sensitivity.fullDegree_imbalance {n : ℕ} (f : BoolFun n) (hn : 0 < n) (h : f.moebius Finset.univ ≠ 0) : ∃ (c : ℤ), (c = 1 ∨ c = -1) ∧ 2 ^ (n - 1) < {x : Fin n → Bool | f.paritySigned x = c}.card

Imbalance: if the parity-weighted sum is nonzero, then one of the two "parity-sign classes" has more than 2^{n-1} elements.