OAI/Combinatorics/EditApproximation/Geometry/PreparedShellPolynomial.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Fixed-degree envelopes for the literal representative, online outer, and continuation loops. Large action counts are explicit numeric inputs.

  1. abbrev OAI.EditApproximation.SP line 14

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Binary/BinarySampledOnlinePolynomial.lean:12 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.SP@path.

  2. def OAI.EditApproximation.spGuard line 15
  3. def OAI.EditApproximation.spGrid line 18
  4. def OAI.EditApproximation.spBox line 19
  5. def OAI.EditApproximation.spQuery line 21
  6. def OAI.EditApproximation.representativeShell line 22
  7. def OAI.EditApproximation.spCoordinates line 32
  8. def OAI.EditApproximation.spPower line 34
  9. def OAI.EditApproximation.spOnline line 35
  10. def OAI.EditApproximation.onlineShell line 38
  11. def OAI.EditApproximation.spSumStorage line 47
  12. def OAI.EditApproximation.spSumWord line 48
  13. def OAI.EditApproximation.spSumWork line 50
  14. def OAI.EditApproximation.spConnectionWord line 51
  15. def OAI.EditApproximation.spConnectionWork line 52
  16. def OAI.EditApproximation.spActionWord line 55
  17. def OAI.EditApproximation.spActionWork line 56
  18. def OAI.EditApproximation.spBellman line 59
  19. def OAI.EditApproximation.spUpdate line 61
  20. def OAI.EditApproximation.spContinuation line 63
  21. def OAI.EditApproximation.physicalShell line 67
  22. def OAI.EditApproximation.representativeShellDegree line 83
  23. def OAI.EditApproximation.onlineShellDegree line 84
  24. def OAI.EditApproximation.physicalShellDegree line 85
  25. theorem OAI.EditApproximation.localRepresentativesBitBudget_fixedPower line 87
  26. theorem OAI.EditApproximation.preparedLocalOnlineBitBudget_fixedPower line 99
  27. theorem OAI.EditApproximation.physicalContinuationBitBudget_fixedPower line 111