OAI/Combinatorics/EditApproximation/Probability/FiniteQueryWork.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact read costs for the finite query combinators used in warmup and refinement. In particular, a collected value is computed once and is reused by the continuation's local arithmetic.

  1. theorem OAI.EditApproximation.FiniteQuery.keys_bind line 12
  2. theorem OAI.EditApproximation.FiniteQuery.keys_collect line 22
  3. theorem OAI.EditApproximation.FiniteQuery.keys_all_collect line 32
  4. theorem OAI.EditApproximation.FiniteQuery.cost_bind line 44
  5. theorem OAI.EditApproximation.FiniteQuery.cost_collect line 53
  6. theorem OAI.EditApproximation.FiniteQuery.keys_length_eq_cost_one line 63
  7. theorem OAI.EditApproximation.FiniteQuery.collect_cost_le line 68