OAI/Combinatorics/EditApproximation/Geometry/PreparedCachedKernelWork.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The complete refinement return includes literal power-denominator construction, multiplication, division and trimming before cache insertion.

  1. abbrev OAI.EditApproximation.CachePoly line 10
  2. def OAI.EditApproximation.cacheSum line 11
  3. def OAI.EditApproximation.cacheConnection line 13
  4. def OAI.EditApproximation.cacheAction line 14
  5. def OAI.EditApproximation.cacheRawWidth line 15
  6. def OAI.EditApproximation.cacheReturnPolynomial line 18
  7. def OAI.EditApproximation.cacheEnvironment line 26
  8. def OAI.EditApproximation.preparedCacheReturnBitDegree line 32
  9. def OAI.EditApproximation.preparedCachedKernelBitDegree line 34
  10. theorem OAI.EditApproximation.preparedCacheReturnBitBudget_fixedPower line 38
  11. theorem OAI.EditApproximation.preparedCachedKernelBitBudget_fixedPower line 50
  12. theorem OAI.EditApproximation.BinaryFraction.cachedPreparedLocalKernelWithWork_bounds line 85