OAI/Combinatorics/EditApproximation/Geometry/PreparedGroupPolynomial.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A fixed-degree cap for the complete cell selector, including all band construction and exact finite-count sampled scores.

  1. abbrev OAI.EditApproximation.CP line 12
  2. def OAI.EditApproximation.cpEligibility line 13
  3. def OAI.EditApproximation.cpGridPoints line 16
  4. def OAI.EditApproximation.cpCellStates line 18
  5. def OAI.EditApproximation.cpCellCenters line 20
  6. def OAI.EditApproximation.cellGroupPolynomial line 23
  7. def OAI.EditApproximation.preparedCellGroupBitDegree line 32
  8. def OAI.EditApproximation.cellGroupEnvironment line 34
  9. theorem OAI.EditApproximation.cellGroupPolynomial_eval line 40
  10. theorem OAI.EditApproximation.preparedCellGroupBitBudget_fixedPower line 46