OAI/Combinatorics/EditApproximation/Geometry/LocalOnlineProgram.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Direct online queries use one rounded center per allowed scale. The integer argument denotes the accepted output of the exact rejection sampler; reduction modulo the requested range merely makes the finite rule total.

  1. theorem OAI.EditApproximation.rationalRefinementUpdate_online_mem_ext line 16
  2. theorem OAI.EditApproximation.keyedOnlineBandG_positive line 28
  3. theorem OAI.EditApproximation.boundedOnlineInteger_val line 37
  4. theorem OAI.EditApproximation.localOnlineCandidates_length line 45
  5. theorem OAI.EditApproximation.localOnlineCandidates_mem line 56
  6. theorem OAI.EditApproximation.keyedOnlineCandidate_eq_physical line 93
  7. def OAI.EditApproximation.physicalLocalOnline line 130