OAI/Combinatorics/EditApproximation/Geometry/RefinementDataQueryWork.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Read counts for the full adaptive data query. Weighting reads permits the same theorem to count current-index and earlier-index dependencies separately. The bounds count executed readers, including repeated reads across successive gathering stages.

  1. theorem OAI.EditApproximation.list_map_sum_le_constant line 13
  2. theorem OAI.EditApproximation.localRefinementBandDataQuery_cost_le line 42
  3. theorem OAI.EditApproximation.localRefinementDataQuery_cost_le line 121
  4. theorem OAI.EditApproximation.localRefinementStepQuery_keys_all line 197
  5. theorem OAI.EditApproximation.localRefinementBandDataQuery_keys_all line 217
  6. theorem OAI.EditApproximation.localRefinementDataQuery_keys_all line 237