OAI/Combinatorics/EditApproximation/Binary/BinaryMedianSpace.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Every insertion-sort copy, median traversal, ceiling and final trimming scan is retained in these seed-branch allocation and call-frame counters.

  1. theorem OAI.EditApproximation.wordLEAllocation_le_work line 15
  2. theorem OAI.EditApproximation.wordInsertAllocation_le_work line 21
  3. theorem OAI.EditApproximation.wordSortAllocation_le_work line 37
  4. def OAI.EditApproximation.wordLEInvocations line 46
  5. theorem OAI.EditApproximation.wordLEInvocations_le_work line 48
  6. def OAI.EditApproximation.wordInsertInvocations line 52
  7. theorem OAI.EditApproximation.wordInsertInvocations_le_work line 57
  8. def OAI.EditApproximation.wordSortInvocations line 67
  9. theorem OAI.EditApproximation.wordSortInvocations_le_work line 72
  10. theorem OAI.EditApproximation.BinaryFraction.scaledCeilingAllocation_le_work line 85
  11. theorem OAI.EditApproximation.BinaryFraction.medianSeedAllocation_le_work line 95
  12. theorem OAI.EditApproximation.BinaryFraction.seedMedianAllocation_le_work line 109
  13. def OAI.EditApproximation.BinaryFraction.scaledCeilingInvocations line 117
  14. theorem OAI.EditApproximation.BinaryFraction.scaledCeilingInvocations_le_work line 121
  15. def OAI.EditApproximation.BinaryFraction.medianSeedInvocations line 129
  16. theorem OAI.EditApproximation.BinaryFraction.medianSeedInvocations_le_work line 136
  17. def OAI.EditApproximation.BinaryFraction.seedMedianInvocations line 148
  18. theorem OAI.EditApproximation.BinaryFraction.seedMedianInvocations_le_work line 152