OAI/Combinatorics/EditApproximation/Queries/QueryActionInputCost.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Bounds for the final adaptive child gather. The temporary list and its sorting work depend on emitted actions, rather than the full table.

  1. theorem OAI.EditApproximation.queryActionInputsWithWork_bounds line 12
  2. theorem OAI.EditApproximation.queryOrderedChildInputsWithWork_length line 35
  3. def OAI.EditApproximation.queryNeededInputsBitBudget line 40
  4. theorem OAI.EditApproximation.queryNeededInputsWithWork_bounds line 44