OAI/Combinatorics/EditApproximation/Geometry/LocalRefinementQueryWork.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The literal three-stage query plan has the earlier-cover cost plus at most twice the current-cover cost. This counts its executed readers, including overlap between its two current gathers.

  1. theorem OAI.EditApproximation.localRefinementStepQuery_cost line 32
  2. theorem OAI.EditApproximation.localRefinementStepQuery_cost_le line 85