OAI/Combinatorics/EditApproximation/Queries/QueryRefinementWorkBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Composition of the seven executed refinement stages. Recursive reads, list construction, sorting, both selectors and the final continuation are all included in this counter.

  1. theorem OAI.EditApproximation.query_sum_map_bound line 12
  2. def OAI.EditApproximation.BinaryFraction.queryRefinementStagesBudget line 24
  3. theorem OAI.EditApproximation.queryRefinementGather_work_bound line 51