OAI/Algebra/DepthFive/UpperConstruction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem335.immUpperCircuit line 12

   Source documentation

   The canonical block circuit at block width ceilSqrt n.

   def immUpperCircuit (K : Type*) [CommSemiring K] (n : ℕ) (hn : 0 < n) :
       Depth5Circuit K n :=
   …

   Mentions: OAI.Problem335.Depth5Circuit

2. theorem OAI.Problem335.immUpperCircuit_outputDegree line 16
3. theorem OAI.Problem335.immUpperCircuit_size line 20
4. theorem OAI.Problem335.immUpperCircuit_value line 47
5. theorem OAI.Problem335.exists_imm_circuit_le_upperGateBound line 53

   Source documentation

   A homogeneous depth-five circuit attaining the explicit block-expansion gate budget.

   theorem exists_imm_circuit_le_upperGateBound (K : Type*) [CommSemiring K]
       (n : ℕ) (hn : 2 ≤ n) :
       ∃ c : Depth5Circuit K n, circuitValue c = imm K n ∧ circuitSize c ≤ upperGateBound n := by
   …

   Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.circuitValue, OAI.Problem335.imm, OAI.Problem335.circuitSize, OAI.Problem335.upperGateBound