Symmetric functions and majority

Symmetry means that the output depends only on Hamming weight. Majority uses the convention in Lecomte and Ramakrishnan's paper: ties are accepted. This differs from the strict-majority function used for error amplification.

def Complexity.Shallow.Symmetric {n : ℕ} (f : BitString n → Bool) : Prop

A symmetric Boolean function is constant on each Hamming-weight level.

Equations

• Complexity.Shallow.Symmetric f = ∀ (x y : Fin n → Bool), Complexity.Shallow.weight x = Complexity.Shallow.weight y → f x = f y

def Complexity.Shallow.majority {n : ℕ} (x : BitString n) : Bool

Majority with ties accepted, as in the source paper.

Equations

• Complexity.Shallow.majority x = decide (n ≤ 2 * Complexity.Shallow.weight x)

theorem Complexity.Shallow.majority_symmetric (n : ℕ) : Symmetric majority

Majority depends only on Hamming weight.

theorem Complexity.Shallow.Symmetric.exists_weight_function {n : ℕ} {f : BitString n → Bool} (hf : Symmetric f) : ∃ (a : ℕ → Bool), ∀ (x : Fin n → Bool), a (weight x) = f x

Every symmetric function factors through Hamming weight.