OAI/Combinatorics/EditApproximation/Binary/BinaryCachedShellWork.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Initial and warmup returns are integers on every seed. Their cache representation is produced by the counted fixed-denominator routine, rather than by an uncharged conversion of a rational value.

  1. theorem OAI.EditApproximation.localInitialConeTable_den_one line 14
  2. def OAI.EditApproximation.BinaryFraction.cachedInitialProgramWithWork line 48
  3. def OAI.EditApproximation.BinaryFraction.cachedInitialProgramBitBudget line 53
  4. theorem OAI.EditApproximation.BinaryFraction.cachedInitialProgramWithWork_cost line 56
  5. theorem OAI.EditApproximation.BinaryFraction.cachedInitialProgramWithWork_value_width line 71
  6. def OAI.EditApproximation.BinaryFraction.cachedLocalWarmupKernelWithWork line 97
  7. theorem OAI.EditApproximation.BinaryFraction.localWarmupKernelWithWork_integer_bounds line 104
  8. theorem OAI.EditApproximation.BinaryFraction.cachedLocalWarmupKernelWithWork_value_width line 143
  9. theorem OAI.EditApproximation.BinaryFraction.cachedLocalWarmupKernelWithWork_cost line 161