OAI/Combinatorics/EditApproximation/Geometry/DyadicQueryWindow.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The query scale window has length controlled by the refinement factor, independently of the number of dyadic scales below N.

  1. theorem OAI.EditApproximation.dyadicQueryWindow_length_le line 16