OAI/Combinatorics/EditApproximation/Geometry/PreparedInitialPolynomial.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Fixed degrees for the literal initial grid/minimum, trimmed seed median, and child warmup average. Grid side length is an explicit input.

  1. abbrev OAI.EditApproximation.IP line 15
  2. def OAI.EditApproximation.ipCenter line 16
  3. def OAI.EditApproximation.ipScale line 19
  4. def OAI.EditApproximation.ipGrid line 22
  5. def OAI.EditApproximation.ipBox line 23
  6. def OAI.EditApproximation.ipGridScale line 25
  7. def OAI.EditApproximation.ipDistance line 27
  8. def OAI.EditApproximation.ipGap line 29
  9. def OAI.EditApproximation.ipConeInput line 31
  10. def OAI.EditApproximation.ipSeed line 32
  11. def OAI.EditApproximation.ipCone line 34
  12. def OAI.EditApproximation.ipMinimumWord line 37
  13. def OAI.EditApproximation.ipMinimum line 38
  14. def OAI.EditApproximation.initialShellPolynomial line 42
  15. def OAI.EditApproximation.preparedInitialBitDegree line 49
  16. def OAI.EditApproximation.cachedInitialShellPolynomial line 51
  17. def OAI.EditApproximation.preparedCachedInitialBitDegree line 55
  18. theorem OAI.EditApproximation.initialProgramBitBudget_fixedPower line 57
  19. theorem OAI.EditApproximation.cachedInitialProgramBitBudget_fixedPower line 70
  20. def OAI.EditApproximation.medianShellPolynomial line 84
  21. def OAI.EditApproximation.preparedMedianBitDegree line 91
  22. theorem OAI.EditApproximation.seedMedianBitBudget_fixedPower line 93
  23. def OAI.EditApproximation.ipStoredSumWord line 104
  24. def OAI.EditApproximation.ipMassStorage line 106
  25. def OAI.EditApproximation.averageShellPolynomial line 107
  26. def OAI.EditApproximation.preparedAverageBitDegree line 113
  27. theorem OAI.EditApproximation.warmupAverageBitBudget_fixedPower line 115