Documentation

Complexity.Computability.QueryComplexity.ApproximateDegree

Approximate degree #

The ε-approximate degree adeg_ε(f) of a Boolean function f is the least degree of a real function on the cube that is within ε of f, read with values 0 and 1, at every input (QueryComplexity.approxDegree) [NS94], [BdW02]. The approximate degree adeg(f) of the literature is adeg_{1/3}(f); any constant ε < 1/2 changes it by at most a constant factor.

Exact representation is the case ε = 0 (QueryComplexity.approxDegree_zero), so adeg_ε(f) ≤ deg(f) ≤ D(f) (QueryComplexity.approxDegree_le_degree, DecisionTree.approxDegree_le_complexity). Approximate degree decreases as ε grows and vanishes from ε = 1/2 on, where the constant 1/2 is within ε of every Boolean function (QueryComplexity.approxDegree_eq_zero_of_le). Negating the output does not change it.

Main definitions #

Main results #

References #

source
noncomputable def Cslib.QueryComplexity.approxDegree {n : ℕ} (ε : ℝ) (f : BooleanFunction n) :
ℕ

The ε-approximate degree adeg_ε(f) of a Boolean function: the least degree of a real function on the cube that is within ε of f, read with values 0 and 1, at every input. It is 0 when no function qualifies, which happens exactly for ε < 0.

Instances For
    source
    theorem Cslib.QueryComplexity.approxDegree_le_of_mem_lowDegree {n : ℕ} {f : BooleanFunction n} {ε : ℝ} {p : BitString n → ℝ} {D : ℕ} (hp : p ∈ BitString.lowDegree ℝ (Fin n) D) (h : ∀ (x : BitString n), |p x - BitString.bitVal ℝ (f x)| ≤ ε) :
    approxDegree ε f ≤ D

    A real function of degree at most D within ε of f bounds adeg_ε(f) by D.

    source
    theorem Cslib.QueryComplexity.exists_mem_lowDegree_approxDegree {n : ℕ} {f : BooleanFunction n} {ε : ℝ} (hε : 0 ≤ ε) :
    ∃ p ∈ BitString.lowDegree ℝ (Fin n) (approxDegree ε f), ∀ (x : Fin n → Bool), |p x - BitString.bitVal ℝ (f x)| ≤ ε

    For ε ≥ 0 the approximate degree is attained: some real function of degree adeg_ε(f) is within ε of f.

    source
    theorem Cslib.QueryComplexity.approxDegree_le_degree {n : ℕ} {f : BooleanFunction n} {ε : ℝ} (hε : 0 ≤ ε) :
    approxDegree ε f ≤ degree f

    adeg_ε(f) ≤ deg(f) for ε ≥ 0.

    source
    theorem Cslib.QueryComplexity.approxDegree_le_card {n : ℕ} {f : BooleanFunction n} {ε : ℝ} (hε : 0 ≤ ε) :
    approxDegree ε f ≤ n

    adeg_ε(f) ≤ n for ε ≥ 0.

    source
    theorem Cslib.QueryComplexity.approxDegree_zero {n : ℕ} {f : BooleanFunction n} :
    approxDegree 0 f = degree f

    Exact representation: adeg_0(f) = deg(f).

    source
    theorem Cslib.QueryComplexity.approxDegree_antitone {n : ℕ} {f : BooleanFunction n} {ε δ : ℝ} (hε : 0 ≤ ε) (hεδ : ε ≤ δ) :
    approxDegree δ f ≤ approxDegree ε f

    adeg_ε(f) decreases as ε grows.

    source
    theorem Cslib.QueryComplexity.approxDegree_eq_zero_of_le {n : ℕ} {f : BooleanFunction n} {ε : ℝ} (hε : 1 / 2 ≤ ε) :
    approxDegree ε f = 0

    From ε = 1/2 on, the constant 1/2 is within ε of every Boolean function.

    source
    theorem Cslib.QueryComplexity.approxDegree_not {n : ℕ} (ε : ℝ) (f : BooleanFunction n) :
    (approxDegree ε fun (x : BitString n) => !f x) = approxDegree ε f

    Negating a Boolean function preserves its approximate degree: 1 - p approximates !f as well as p approximates f.

    source
    theorem Cslib.DecisionTree.approxDegree_le_complexity {n : ℕ} (f : BooleanFunction n) {ε : ℝ} (hε : 0 ≤ ε) :
    QueryComplexity.approxDegree ε f ≤ complexity f

    adeg_ε(f) ≤ D(f) for ε ≥ 0.