OAI/Combinatorics/EditApproximation/Queries/QueryOrderBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Quadratic work bounds for actual duplicate removal and encoded sorting. The bound counts comparisons and list allocation, including duplicates.

  1. theorem OAI.EditApproximation.queryEraseLoopWithWork_length line 10
  2. theorem OAI.EditApproximation.queryEraseWithWork_length line 22
  3. theorem OAI.EditApproximation.queryOrderedInputsWithWork_cost line 27
  4. theorem OAI.EditApproximation.queryEncodedLEWithWork_cost line 44