OAI/Combinatorics/EditApproximation/Geometry/PreparedBandPolynomial.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

A fixed-degree bound for the complete band constructor. The sole non-polynomial quantity is the actual Cartesian-product list bound, an explicit input subsequently bounded by the computed grid parameters.

  1. abbrev OAI.EditApproximation.BP line 12
  2. def OAI.EditApproximation.bpSumStorage line 13
  3. def OAI.EditApproximation.bpSumWord line 14
  4. def OAI.EditApproximation.bpSumWork line 16
  5. def OAI.EditApproximation.bpConnectionWord line 17
  6. def OAI.EditApproximation.bpConnectionWork line 18
  7. def OAI.EditApproximation.bpEndpointWord line 21
  8. def OAI.EditApproximation.bpEndpointWork line 23
  9. def OAI.EditApproximation.bpMinimum line 26
  10. def OAI.EditApproximation.bpGapWord line 29
  11. def OAI.EditApproximation.bpGapWork line 30
  12. def OAI.EditApproximation.bpNaturalDistance line 32
  13. def OAI.EditApproximation.bpAnchor line 34
  14. def OAI.EditApproximation.bpTolerance line 36
  15. def OAI.EditApproximation.bpPredicate line 38
  16. def OAI.EditApproximation.bpBand line 40
  17. def OAI.EditApproximation.bpRepresentative line 42
  18. def OAI.EditApproximation.bpGridPoints line 47
  19. def OAI.EditApproximation.bpGridBox line 49
  20. def OAI.EditApproximation.bpWide line 52
  21. def OAI.EditApproximation.bpEnvelopeWord line 55
  22. def OAI.EditApproximation.bpEnvelopeWork line 56
  23. def OAI.EditApproximation.bpRound line 61
  24. def OAI.EditApproximation.bpGuard line 66
  25. def OAI.EditApproximation.preparedBandPolynomial line 75
  26. def OAI.EditApproximation.preparedBandBitDegree line 86
  27. def OAI.EditApproximation.preparedBandEnvironment line 88
  28. theorem OAI.EditApproximation.preparedBandPolynomial_eval line 98
  29. theorem OAI.EditApproximation.preparedUnskippedBitBudget_fixedPower line 102
  30. def OAI.EditApproximation.representativeCompleteBitDegree line 114

    Source documentation

    The representative tail used to construct the actual online draw range.

    def representativeCompleteBitDegree : ℕ :=
…
  31. theorem OAI.EditApproximation.representativeCompleteBitBudget_fixedPower line 117