OAI/Combinatorics/EditApproximation/Refinement/PhysicalLocalGroupKeys.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Every whole-cell stream used by the complete program has a bounded physical key. Its two cell coordinates are at most n*2^exponent.

  1. theorem OAI.EditApproximation.list_eraseDups_nodup line 14
  2. theorem OAI.EditApproximation.targetCell_coordinate_bound line 29
  3. theorem OAI.EditApproximation.physicalProgramCells_bounds line 57
  4. theorem OAI.EditApproximation.physicalGroupScale_positive line 64
  5. def OAI.EditApproximation.physicalGroupRawKey line 71
  6. theorem OAI.EditApproximation.physicalGroupRawKey_injective line 80
  7. abbrev OAI.EditApproximation.PhysicalLocalGroupArray line 100
  8. def OAI.EditApproximation.physicalLocalGroupArrayLaw line 106
  9. instance OAI.EditApproximation.physicalLocalGroupArrayLaw_probability line 114
  10. theorem OAI.EditApproximation.physicalLocalGroupDrawLaw_restrict line 121