OAI/Combinatorics/EditApproximation/Queries/QueryEarlierInputs.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

All wide-coordinate requests needed for one local query can be gathered from bounded representative lists, including complete requested cells and the rounded online center at every applicable scale.

  1. theorem OAI.EditApproximation.queryEarlierRepresentatives_length line 17
  2. theorem OAI.EditApproximation.queryEarlierRepresentatives_local line 43
  3. theorem OAI.EditApproximation.queryEarlierRepresentatives_cell line 49
  4. theorem OAI.EditApproximation.queryEarlierRepresentatives_online line 58
  5. theorem OAI.EditApproximation.queryEarlierInputCover_card line 67