Gates with arbitrary activations

Every gate of an ActivationProgram is its own block. Given the earlier gates, an input-reading gate j is activation j (t + c) in its weighted input sum t, for a constant c, so it changes at most T j times when its activation does; a gate reading no input is a function of the earlier gates. The capacity theorem then charges max 1 (4 T j) to every input-reading gate and nothing to the other gates.

theorem Algebraic.Threshold.ChangesAtMost.map {β : Type u_1} {γ : Type u_2} {Ψ : ℝ → β} {T : ℕ} (h : ChangesAtMost Ψ T) (G : β → γ) : ChangesAtMost (fun (t : ℝ) => G (Ψ t)) T

theorem Algebraic.Threshold.changesAtMost_const {β : Type u_1} (c : β) : ChangesAtMost (fun (x : ℝ) => c) 0

theorem Algebraic.Threshold.ActivationProgram.eval_eq_internal {n s : ℕ} (C : ActivationProgram n s) (x : Fin n → Bool) (j : Fin s) : C.eval x j = C.activation j (weightedSum (C.inputWeight j) x + ∑ k : Fin s, if k < j then C.gateWeight j k * ↑(C.eval x k).toNat else 0)

noncomputable def Algebraic.Threshold.ActivationProgram.budget {n s : ℕ} (C : ActivationProgram n s) (T : Fin s → ℕ) (i : ℕ) : ℕ

The change budget of the i-th gate: T for an input-reading gate, 0 otherwise.

Equations

• C.budget T i = if h : i < s then if ⟨i, h⟩ ∈ C.inputGates then T ⟨i, h⟩ else 0 else 0

noncomputable def Algebraic.Threshold.ActivationProgram.toBlockDecomposition {n s : ℕ} (C : ActivationProgram n s) {f : Cslib.BooleanFunction n} (hC : C.Computes f) (T : Fin s → ℕ) (hT : ∀ j ∈ C.inputGates, ChangesAtMost (C.activation j) (T j)) : BlockDecomposition f (Fin s → Bool)

The gate-by-gate block decomposition of an activation program.

Equations

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

theorem Algebraic.Threshold.ActivationProgram.toBlockDecomposition_cost {n s : ℕ} (C : ActivationProgram n s) {f : Cslib.BooleanFunction n} (hC : C.Computes f) (T : Fin s → ℕ) (hT : ∀ j ∈ C.inputGates, ChangesAtMost (C.activation j) (T j)) : (C.toBlockDecomposition hC T hT).cost = ∏ j ∈ C.inputGates, max 1 (4 * T j)

theorem Algebraic.Threshold.two_pow_lt_of_activations_internal {n s : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hf : TwoSidedRectangleFree f K) {C : ActivationProgram n s} (hC : C.Computes f) (T : Fin s → ℕ) (hT : ∀ j ∈ C.inputGates, ChangesAtMost (C.activation j) (T j)) : 2 ^ n < 4 * K ^ 2 * ∏ j ∈ C.inputGates, max 1 (4 * T j)