Logarithmic size-activity bounds for inner product

A weighted threshold program computing inner product on m coordinates per side satisfies m / 2 ≤ e * log₂ (exp 1 * q / e) and e / exp 1 * 2 ^ (m / (2 * e)) ≤ q, where q counts the gates and e is their maximum activity. The same bounds hold when both quantities count only input-reading gates. These consequences of the exact binomial-sum bound hold throughout e ≤ q, including activity above half the gate count.

Positive-dimensional inner product requires positive input-reading activity. The numerical bounds also include zero-dimensional inputs, using the usual total real operations at e = 0. The circuit statements require a gate output. The input-reading bounds exclude gates reading only earlier gates; the total-gate bounds include them. No restriction on depth or real coefficient magnitude is imposed.

Main results

• Cslib.Circuits.Boolean.WeightedThreshold.inputActivity_pos_of_hadamardCode: positive activity when the input on each side has at least one coordinate.
• Cslib.Circuits.Boolean.WeightedThreshold.le_inputActivity_mul_logb_of_hadamardCode: the logarithmic size-activity bound.
• Cslib.Circuits.Boolean.WeightedThreshold.inputActivity_mul_rpow_le_card_of_hadamardCode: the rearranged lower bound on the number of input-reading gates.
• Cslib.Circuits.Boolean.WeightedThreshold.le_gateActivity_mul_logb_of_hadamardCode and Cslib.Circuits.Boolean.WeightedThreshold.gateActivity_mul_rpow_le_of_hadamardCode: the corresponding bounds using all gates and their maximum activity.

References

• [Threshold Circuits as Decision Trees and Finite-State Programs, Theorem 3.2] [26]

theorem Cslib.Circuits.Boolean.WeightedThreshold.inputActivity_pos_of_hadamardCode {n g : ℕ} {ι : Type u_1} [Fintype ι] (p : Program signature n g) (split : Fin n ≃ ι ⊕ ι) (readout : (Fin g → Bool) → Bool) (hm : 0 < Fintype.card ι) (h : ∀ (x y : ι → Bool), readout (p.eval interpretation (inputOfSplit split x y)) = BitString.hadamardCode x y) : 0 < inputActivity p

Computing positive-dimensional inner product requires positive input-reading activity.

theorem Cslib.Circuits.Boolean.WeightedThreshold.le_inputActivity_mul_logb_of_hadamardCode {n g : ℕ} {ι : Type u_1} [Fintype ι] (p : Program signature n g) (split : Fin n ≃ ι ⊕ ι) (readout : (Fin g → Bool) → Bool) (h : ∀ (x y : ι → Bool), readout (p.eval interpretation (inputOfSplit split x y)) = BitString.hadamardCode x y) : ↑(Fintype.card ι) / 2 ≤ ↑(inputActivity p) * Real.logb 2 (Real.exp 1 * ↑(inputGates p).card / ↑(inputActivity p))

The input-reading activity and gate count obey the logarithmic size-activity bound.

theorem Cslib.Circuits.Boolean.WeightedThreshold.inputActivity_mul_rpow_le_card_of_hadamardCode {n g : ℕ} {ι : Type u_1} [Fintype ι] (p : Program signature n g) (split : Fin n ≃ ι ⊕ ι) (readout : (Fin g → Bool) → Bool) (h : ∀ (x y : ι → Bool), readout (p.eval interpretation (inputOfSplit split x y)) = BitString.hadamardCode x y) : ↑(inputActivity p) / Real.exp 1 * 2 ^ (↑(Fintype.card ι) / (2 * ↑(inputActivity p))) ≤ ↑(inputGates p).card

Inner product requires at least e / exp 1 * 2 ^ (m / (2 * e)) input-reading gates.

theorem Cslib.Circuits.Boolean.WeightedThreshold.le_inputActivity_mul_logb_of_circuit_hadamardCode {n : ℕ} {ι : Type u_1} [Fintype ι] (c : Circuit signature n 1) (split : Fin n ≃ ι ⊕ ι) (houtput : ∃ (gate : Fin c.size), c.outputs 0 = Wire.gate gate) (h : ∀ (x y : ι → Bool), c.eval interpretation (inputOfSplit split x y) 0 = BitString.hadamardCode x y) : ↑(Fintype.card ι) / 2 ≤ ↑(inputActivity c.program) * Real.logb 2 (Real.exp 1 * ↑(inputGates c.program).card / ↑(inputActivity c.program))

The logarithmic size-activity bound for a native single-output circuit with a gate output.

theorem Cslib.Circuits.Boolean.WeightedThreshold.inputActivity_mul_rpow_le_card_of_circuit_hadamardCode {n : ℕ} {ι : Type u_1} [Fintype ι] (c : Circuit signature n 1) (split : Fin n ≃ ι ⊕ ι) (houtput : ∃ (gate : Fin c.size), c.outputs 0 = Wire.gate gate) (h : ∀ (x y : ι → Bool), c.eval interpretation (inputOfSplit split x y) 0 = BitString.hadamardCode x y) : ↑(inputActivity c.program) / Real.exp 1 * 2 ^ (↑(Fintype.card ι) / (2 * ↑(inputActivity c.program))) ≤ ↑(inputGates c.program).card

The rearranged input-reading-gate lower bound for a circuit with a gate output.

theorem Cslib.Circuits.Boolean.WeightedThreshold.le_gateActivity_mul_logb_of_hadamardCode {n g : ℕ} {ι : Type u_1} [Fintype ι] (p : Program signature n g) (split : Fin n ≃ ι ⊕ ι) (readout : (Fin g → Bool) → Bool) (h : ∀ (x y : ι → Bool), readout (p.eval interpretation (inputOfSplit split x y)) = BitString.hadamardCode x y) : ↑(Fintype.card ι) / 2 ≤ ↑(gateActivity p) * Real.logb 2 (Real.exp 1 * ↑g / ↑(gateActivity p))

The maximum activity across all gates obeys the logarithmic size-activity bound.

theorem Cslib.Circuits.Boolean.WeightedThreshold.gateActivity_mul_rpow_le_of_hadamardCode {n g : ℕ} {ι : Type u_1} [Fintype ι] (p : Program signature n g) (split : Fin n ≃ ι ⊕ ι) (readout : (Fin g → Bool) → Bool) (h : ∀ (x y : ι → Bool), readout (p.eval interpretation (inputOfSplit split x y)) = BitString.hadamardCode x y) : ↑(gateActivity p) / Real.exp 1 * 2 ^ (↑(Fintype.card ι) / (2 * ↑(gateActivity p))) ≤ ↑g

Inner product requires at least e / exp 1 * 2 ^ (m / (2 * e)) gates at total activity e.

theorem Cslib.Circuits.Boolean.WeightedThreshold.le_gateActivity_mul_logb_of_circuit_hadamardCode {n : ℕ} {ι : Type u_1} [Fintype ι] (c : Circuit signature n 1) (split : Fin n ≃ ι ⊕ ι) (houtput : ∃ (gate : Fin c.size), c.outputs 0 = Wire.gate gate) (h : ∀ (x y : ι → Bool), c.eval interpretation (inputOfSplit split x y) 0 = BitString.hadamardCode x y) : ↑(Fintype.card ι) / 2 ≤ ↑(gateActivity c.program) * Real.logb 2 (Real.exp 1 * ↑c.size / ↑(gateActivity c.program))

The total-gate logarithmic bound for a native single-output circuit with a gate output.

theorem Cslib.Circuits.Boolean.WeightedThreshold.gateActivity_mul_rpow_le_of_circuit_hadamardCode {n : ℕ} {ι : Type u_1} [Fintype ι] (c : Circuit signature n 1) (split : Fin n ≃ ι ⊕ ι) (houtput : ∃ (gate : Fin c.size), c.outputs 0 = Wire.gate gate) (h : ∀ (x y : ι → Bool), c.eval interpretation (inputOfSplit split x y) 0 = BitString.hadamardCode x y) : ↑(gateActivity c.program) / Real.exp 1 * 2 ^ (↑(Fintype.card ι) / (2 * ↑(gateActivity c.program))) ≤ ↑c.size

The rearranged total-gate lower bound for a circuit with a gate output.