OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/ExpandingWorkBudget.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A computable choice of schedule pays for the product of the number of gates and the largest address. This is the arithmetic part of the global derivative bound.

  1. def OAI.ForcedComputation.ExpandingDetector.workGrowth line 14
  2. def OAI.ForcedComputation.ExpandingDetector.workFactor line 18
  3. theorem OAI.ForcedComputation.ExpandingDetector.workGrowth_ge_one line 22
  4. theorem OAI.ForcedComputation.ExpandingDetector.workFactor_nonneg line 28
  5. theorem OAI.ForcedComputation.ExpandingDetector.geometric_work_bound line 32