OAI/Combinatorics/EditApproximation/Binary/BinaryOnlineSpace.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

The online objective includes every repeated history-buffer read. Its allocation and frame counters follow the same Boolean arithmetic and materialized vector passes as the executed continuation.

  1. theorem OAI.EditApproximation.BinaryFraction.coefficientAllocation_le_work line 16
  2. theorem OAI.EditApproximation.BinaryFraction.gainReadAllocation_le_work line 26
  3. theorem OAI.EditApproximation.BinaryFraction.decrementReadAllocation_le_work line 37
  4. theorem OAI.EditApproximation.BinaryFraction.optimisticTermReadAllocation_le_work line 50
  5. theorem OAI.EditApproximation.BinaryFraction.onlineLinearReadAllocation_le_work line 67
  6. def OAI.EditApproximation.BinaryFraction.coefficientInvocations line 91
  7. theorem OAI.EditApproximation.BinaryFraction.coefficientInvocations_le_work line 94
  8. def OAI.EditApproximation.BinaryFraction.gainReadInvocations line 102
  9. theorem OAI.EditApproximation.BinaryFraction.gainReadInvocations_le_work line 107
  10. def OAI.EditApproximation.BinaryFraction.decrementReadInvocations line 116
  11. theorem OAI.EditApproximation.BinaryFraction.decrementReadInvocations_le_work line 122
  12. def OAI.EditApproximation.BinaryFraction.optimisticTermReadInvocations line 133
  13. theorem OAI.EditApproximation.BinaryFraction.optimisticTermReadInvocations_le_work line 142
  14. def OAI.EditApproximation.BinaryFraction.onlineLinearReadInvocations line 157
  15. theorem OAI.EditApproximation.BinaryFraction.onlineLinearReadInvocations_le_work line 169
  16. def OAI.EditApproximation.BinaryFraction.preparedOptimizerReadAllocation line 193
  17. def OAI.EditApproximation.BinaryFraction.preparedOptimizerReadInvocations line 206
  18. theorem OAI.EditApproximation.BinaryFraction.preparedOptimizerReadAllocation_le_work line 219
  19. theorem OAI.EditApproximation.BinaryFraction.preparedOptimizerReadInvocations_le_work_add_one line 239