OAI/Combinatorics/EditApproximation/Geometry/CurrentQueryInputs.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Distinct current-index inputs of the bounded query loops. The cover includes all whole-cell shared estimates, selected cell actions, and online actions; repeated uses do not add recursive calls.

  1. theorem OAI.EditApproximation.groupDyadicScales_lower line 16
  2. theorem OAI.EditApproximation.localGroupQueryKeys_scale line 25
  3. theorem OAI.EditApproximation.localGroupQueryKeys_length line 33
  4. theorem OAI.EditApproximation.querySharedInputCover_card line 51
  5. theorem OAI.EditApproximation.actionCurrentInputCover_card line 116
  6. theorem OAI.EditApproximation.actionCurrentInputCover_mem line 128
  7. def OAI.EditApproximation.currentQueryInputCover line 137
  8. theorem OAI.EditApproximation.currentQueryInputCover_card line 147