OAI/Combinatorics/EditApproximation/Queries/QueryScopedSourceCost.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The source ports are bounded only at keys visited by the adaptive local loops. Unused natural-number coordinates require no uniform size assumption.

  1. theorem OAI.EditApproximation.BinaryFraction.queryGroupKeysWithWork_mem_of_guard line 11
  2. def OAI.EditApproximation.BinaryFraction.queryGroupBufferReadBudget line 30
  3. theorem OAI.EditApproximation.BinaryFraction.queryGroupDrawReadWithWork_scoped_cost line 34
  4. theorem OAI.EditApproximation.BinaryFraction.queryOnlineKeysWithWork_scale line 61
  5. def OAI.EditApproximation.BinaryFraction.queryOnlineBufferReadBudget line 69
  6. theorem OAI.EditApproximation.BinaryFraction.queryOnlineIntegerReadWithWork_scoped_cost line 72