Gate-count corollaries of the capacity theorem

A run with r input-reading gates changes at most 2 ^ r - 1 times, so it costs at most 4 ^ r, and at most 4 · 2 ^ r. Splitting the gates into single-gate runs bounds the product of the run costs by 4 ^ s_in; a split into B runs bounds it by 4 ^ B · 2 ^ s_in. A multilevel threshold function F(⟨w, x⟩) is a decomposition with one block.

theorem Algebraic.Threshold.cost_oneDim_le_four_pow (r : ℕ) : (BlockKind.oneDim (2 ^ r - 1)).cost ≤ 4 ^ r

theorem Algebraic.Threshold.cost_oneDim_le_four_mul (r : ℕ) : (BlockKind.oneDim (2 ^ r - 1)).cost ≤ 4 * 2 ^ r

theorem Algebraic.Threshold.cost_oneDim_eq_max (T : ℕ) : (BlockKind.oneDim T).cost = max 1 (4 * T)

theorem Algebraic.Threshold.Program.DirectionRuns.sum_size {n s : ℕ} {C : Program n s} {B : ℕ} (R : C.DirectionRuns B) : ∑ i ∈ Finset.range B, R.size i = C.inputGates.card

noncomputable def Algebraic.Threshold.Program.gateRuns {n s : ℕ} (C : Program n s) : C.DirectionRuns s

The split of the gates into single-gate runs, each along its own input weight vector.

Equations

• C.gateRuns = { run := fun (j : Fin s) => ↑j, monotone := ⋯, run_lt := ⋯, dir := fun (i : ℕ) => if h : i < s then C.inputWeight ⟨i, h⟩ else 0, along := ⋯ }

def Algebraic.Threshold.Program.singleRun {n s : ℕ} (C : Program n s) (w : Fin n → ℝ) (along : ∀ (j : Fin s), ∃ (c : ℝ), C.inputWeight j = c • w) : C.DirectionRuns 1

The single run of a program whose input weight vectors are all multiples of w.

Equations

• C.singleRun w along = { run := fun (x : Fin s) => 0, monotone := ⋯, run_lt := ⋯, dir := fun (x : ℕ) => w, along := along }

theorem Algebraic.Threshold.Program.DirectionRuns.prod_cost_le_four_pow {n s : ℕ} {C : Program n s} {B : ℕ} (R : C.DirectionRuns B) : ∏ i ∈ Finset.range B, (BlockKind.oneDim (2 ^ R.size i - 1)).cost ≤ 4 ^ C.inputGates.card

theorem Algebraic.Threshold.Program.DirectionRuns.prod_cost_le_four_pow_mul {n s : ℕ} {C : Program n s} {B : ℕ} (R : C.DirectionRuns B) : ∏ i ∈ Finset.range B, (BlockKind.oneDim (2 ^ R.size i - 1)).cost ≤ 4 ^ B * 2 ^ C.inputGates.card

theorem Algebraic.Threshold.two_pow_lt_of_directionRuns_internal {n s : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hf : TwoSidedRectangleFree f K) {C : Program n s} (hC : C.Computes f) {B : ℕ} (R : C.DirectionRuns B) : 2 ^ n < 4 * K ^ 2 * ∏ i ∈ Finset.range B, (BlockKind.oneDim (2 ^ R.size i - 1)).cost

noncomputable def Algebraic.Threshold.multilevelDecomposition {n : ℕ} {f : Cslib.BooleanFunction n} (w : Fin n → ℝ) (F : ℝ → Bool) {T : ℕ} (hF : ChangesAtMost F T) (hfF : ∀ (x : Cslib.BitString n), f x = F (weightedSum w x)) : BlockDecomposition f Bool

The one-block decomposition of a multilevel threshold function F(⟨w, x⟩).

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Threshold.two_pow_lt_of_multilevel_internal {n : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hf : TwoSidedRectangleFree f K) (w : Fin n → ℝ) (F : ℝ → Bool) {T : ℕ} (hF : ChangesAtMost F T) (hfF : ∀ (x : Cslib.BitString n), f x = F (weightedSum w x)) : 2 ^ n < 4 * K ^ 2 * max 1 (4 * T)

theorem Algebraic.Threshold.lt_of_two_pow_lt_mul {n k K X e : ℕ} (hK : K ≤ 2 ^ k) (hX : X ≤ 2 ^ e) (h : 2 ^ n < 4 * K ^ 2 * X) : n < 2 * k + 2 + e

Binary logarithms of a capacity bound with K ≤ 2 ^ k and X ≤ 2 ^ e.

theorem Algebraic.Threshold.two_pow_sub_lt_of_multilevel_internal {n : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hf : TwoSidedRectangleFree f K) {k : ℕ} (hK : K ≤ 2 ^ k) (w : Fin n → ℝ) (F : ℝ → Bool) {T : ℕ} (hF : ChangesAtMost F T) (hfF : ∀ (x : Cslib.BitString n), f x = F (weightedSum w x)) (hn : 2 * k + 4 ≤ n) : 2 ^ (n - (2 * k + 4)) < T