Parity Function and the Imbalance Lemma

The parity function (-1)^{|x|} and its interaction with the Möbius expansion of a Boolean function. The main quantitative output is a parity imbalance lemma: a Boolean function whose top Möbius coefficient is nonzero must have a "majority" parity-sign class strictly larger than 2^{n-1}.

Main results

• LeanPoolSensitivity.parity_flipBit — flipping any bit negates the parity.
• LeanPoolSensitivity.moebius_parity_sum — the sum of f's parity-signed values equals 2 · (-1)^n · c_univ(f).
• LeanPoolSensitivity.fullDegree_imbalance — if f has full multilinear degree, one parity-sign class has more than 2^{n-1} vertices.

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

The parity sign of an input: (-1)^{number of true coordinates}.

Equations

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

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

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

Equations

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

def LeanPoolSensitivity.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 * LeanPoolSensitivity.parity x

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

The ±1 encoding is never zero.

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

The parity sign is never zero.

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

Flipping any single bit negates the parity.

theorem LeanPoolSensitivity.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 the parity-signed value of f is unchanged by a bit flip, then f is sensitive at that input in that direction.

theorem LeanPoolSensitivity.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 recovers the top Möbius coefficient, ∑_x f_pm(x) · parity(x) = 2 · (-1)^n · c_univ(f).

theorem LeanPoolSensitivity.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 multilinear degree (c_univ(f) ≠ 0), then the parity-weighted sum is nonzero.

theorem LeanPoolSensitivity.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

Parity imbalance. If f has full multilinear degree, then one of the two parity-sign classes contains more than 2^{n-1} inputs.