OAI/Algebra/DepthFive/GateCardinality.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem335.circuitSize_le_block_bound line 8

   Source documentation

   The numerical size estimate used after instantiating the block circuit.

   theorem circuitSize_le_block_bound {K : Type*} [CommSemiring K] {n r t : ℕ}
       (c : Depth5Circuit K n)
       (hleaf : c.leafCount ≤ n ^ 3)
       (hbottom : c.bottomCount ≤ n ^ 3)
       (hlower : c.lowerCount ≤ r * n ^ (t + 1))
       (hmiddle : c.middleCount ≤ r * n ^ 2)
       (hupper : c.upperCount ≤ n ^ (r - 1)) :
       circuitSize c ≤ 2 * n ^ 3 + r * n ^ 2 + r * n ^ (t + 1) +
         n ^ (r - 1) + 1 := by
   …

   Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.circuitSize

2. theorem OAI.Problem335.circuitSize_le_upperGateBound line 21

   Source documentation

   Specialization of the block count to the precise upper gate bound.

   theorem circuitSize_le_upperGateBound {K : Type*} [CommSemiring K] {n : ℕ}
       (c : Depth5Circuit K n)
       (hleaf : c.leafCount ≤ n ^ 3)
       (hbottom : c.bottomCount ≤ n ^ 3)
       (hlower : c.lowerCount ≤ ceilDiv n (ceilSqrt n) * n ^ (ceilSqrt n + 1))
       (hmiddle : c.middleCount ≤ ceilDiv n (ceilSqrt n) * n ^ 2)
       (hupper : c.upperCount ≤ n ^ (ceilDiv n (ceilSqrt n) - 1)) :
       circuitSize c ≤ upperGateBound n := by
   …

   Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.ceilDiv, OAI.Problem335.ceilSqrt, OAI.Problem335.circuitSize, OAI.Problem335.upperGateBound