OAI/Combinatorics/EditApproximation/Binary/BinaryOptimizerSpace.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Fresh list cells and primitive call frames of the materialized Boolean optimizer. Intermediate vectors may all remain live; the counters include every optimizer iteration and every candidate score.

  1. def OAI.EditApproximation.vectorMapInvocations line 16
  2. theorem OAI.EditApproximation.vectorMapAllocation_le_work line 19
  3. theorem OAI.EditApproximation.vectorMapInvocations_le_work_add_one line 31
  4. def OAI.EditApproximation.BinaryFraction.gradientInvocations line 47
  5. theorem OAI.EditApproximation.BinaryFraction.gradientAllocation_le_work line 50
  6. theorem OAI.EditApproximation.BinaryFraction.gradientInvocations_le_work_add_one line 54
  7. def OAI.EditApproximation.BinaryFraction.scoredArgmaxInvocations line 60
  8. theorem OAI.EditApproximation.BinaryFraction.scoredArgmaxAllocation_le_work line 69
  9. theorem OAI.EditApproximation.BinaryFraction.scoredArgmaxInvocations_le_work_add_one line 88
  10. def OAI.EditApproximation.BinaryFraction.maximizerInvocations line 109
  11. theorem OAI.EditApproximation.BinaryFraction.maximizerAllocation_le_work line 114
  12. theorem OAI.EditApproximation.BinaryFraction.maximizerInvocations_le_work_add_one line 124
  13. def OAI.EditApproximation.BinaryFraction.optimizerUpdateCellInvocations line 136
  14. def OAI.EditApproximation.BinaryFraction.optimizerUpdateInvocations line 144
  15. theorem OAI.EditApproximation.BinaryFraction.optimizerUpdateAllocation_le_work line 150
  16. theorem OAI.EditApproximation.BinaryFraction.optimizerUpdateInvocations_le_work line 175
  17. def OAI.EditApproximation.BinaryFraction.optimizerInvocations line 202
  18. theorem OAI.EditApproximation.BinaryFraction.optimizerAllocation_le_work line 212
  19. theorem OAI.EditApproximation.BinaryFraction.optimizerInvocations_le_work line 226