OAI/Combinatorics/EditApproximation/Queries/QueryGridCost.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A scale guard bounds the number of grid points even when the center radius is as large as the input. These bounds include construction of all points, before subsequent eligibility filtering.

  1. theorem OAI.EditApproximation.queryGridSpacing_count line 12
  2. def OAI.EditApproximation.queryGridPointsWithWork line 23
  3. def OAI.EditApproximation.queryGridPointsBitBudget line 29
  4. theorem OAI.EditApproximation.queryGridPointsWithWork_bounds line 32