OAI/Combinatorics/EditApproximation/Geometry/PreparedLocalGroupPolynomial.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A fixed-degree cap on all whole-cell loops at a query. Distance scales enter through their bit length; their numeric size is never charged.

  1. abbrev OAI.EditApproximation.LP line 11
  2. def OAI.EditApproximation.lpGuard line 12
  3. def OAI.EditApproximation.lpCellSetup line 15
  4. def OAI.EditApproximation.lpTargetCells line 17
  5. def OAI.EditApproximation.lpScales line 18
  6. def OAI.EditApproximation.localGroupPolynomial line 20
  7. def OAI.EditApproximation.preparedLocalGroupBitDegree line 32
  8. def OAI.EditApproximation.localGroupEnvironment line 34
  9. def OAI.EditApproximation.localGroupMajorant line 43
  10. theorem OAI.EditApproximation.localGroupPolynomial_eval line 51
  11. theorem OAI.EditApproximation.preparedLocalGroupsBitBudget_fixedPower line 55