Documentation

Complexity.Foundations.BooleanAnalysis.Symmetrization

Minsky–Papert symmetrization #

Averaging a function on the cube over each layer of inputs of a given weight turns it into a function of the weight. For a function of degree at most D this function of the weight is a univariate polynomial of degree at most D [MP69] (BitString.exists_natDegree_le_eval_eq_layerAverage): the monomial of a set S of s coordinates is 1 on (n - s).choose (k - s) of the n.choose k inputs of weight k, an average of k.choose s / n.choose s, and k.choose s = k (k - 1) ⋯ (k - s + 1) / s! is a polynomial of degree s in k. Conversely, a univariate polynomial of degree D evaluated at the weight has degree at most D on the cube (BitString.eval_weight_mem_lowDegree).

Substituting into a function of degree at most D a map whose output bits each have degree at most 1 keeps the degree at most D (BitString.comp_mem_lowDegree), so restricting a function to the cube spanned by disjoint blocks of coordinates, as in block sensitivity, and then symmetrizing reduces questions about the degree of a Boolean function to univariate polynomials.

Main definitions #

Main results #

References #

source
theorem Cslib.BitString.comp_mem_lowDegree {R : Type u_1} [CommRing R] {ι : Type u_2} {κ : Type u_3} {φ : (κ → Bool) → ι → Bool} (hφ : ∀ (i : ι), (fun (y : κ → Bool) => bitVal R (φ y i)) ∈ lowDegree R κ 1) {D : ℕ} {f : (ι → Bool) → R} (hf : f ∈ lowDegree R ι D) :
(fun (y : κ → Bool) => f (φ y)) ∈ lowDegree R κ D

Substitution preserves degree: if every output bit of φ, read in R, is a function of degree at most 1, then f ∘ φ has degree at most that of f.

source
theorem Cslib.BitString.weight_mem_lowDegree {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] :
(fun (x : ι → Bool) => ↑(weight x)) ∈ lowDegree R ι 1

The weight, read in R, has degree at most 1.

source
theorem Cslib.BitString.eval_weight_mem_lowDegree {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] (q : Polynomial R) :
(fun (x : ι → Bool) => Polynomial.eval (↑(weight x)) q) ∈ lowDegree R ι q.natDegree

A univariate polynomial evaluated at the weight has degree at most its degree on the cube.

source
def Cslib.BitString.layerAverage {𝕜 : Type u_1} [Field 𝕜] [CharZero 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → 𝕜) (k : ℕ) :
𝕜

The average of f over the inputs of weight k.

Instances For
    source
    theorem Cslib.BitString.layerAverage_monomial {𝕜 : Type u_1} [Field 𝕜] [CharZero 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (S : Finset ι) {k : ℕ} (hk : k ≤ Fintype.card ι) :
    layerAverage (monomial 𝕜 S) k = ↑(k.choose S.card) / ↑((Fintype.card ι).choose S.card)

    The monomial of a set of s coordinates averages to k.choose s / n.choose s over the inputs of weight k ≤ n.

    source
    theorem Cslib.BitString.exists_natDegree_le_eval_eq_layerAverage {𝕜 : Type u_1} [Field 𝕜] [CharZero 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {D : ℕ} {f : (ι → Bool) → 𝕜} (hf : f ∈ lowDegree 𝕜 ι D) :
    ∃ (q : Polynomial 𝕜), q.natDegree ≤ D ∧ ∀ k ≤ Fintype.card ι, Polynomial.eval (↑k) q = layerAverage f k

    Minsky–Papert symmetrization: the layer averages of a function of degree at most D are the values at the weights of a univariate polynomial of degree at most D.