OAI/MathematicalPhysics/ContinuumCoulomb/Programs/GaussNodeProgram.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Literal polynomial-time generation of an initial rational tensor-Gauss node. Integer lattice coordinates and the reciprocal mesh denominator are binary; the approximation precision is unary.

  1. def OAI.ContinuumCoulomb.RationalGaussNodes.signsCode line 15
  2. abbrev OAI.ContinuumCoulomb.RationalGaussNodes.Input line 17
  3. def OAI.ContinuumCoulomb.RationalGaussNodes.inputCode line 18
  4. opaque OAI.ContinuumCoulomb.RationalGaussNodes.precisionProgram line 20
  5. opaque OAI.ContinuumCoulomb.RationalGaussNodes.abscissaProgram line 22
  6. opaque OAI.ContinuumCoulomb.RationalGaussNodes.signedProgram line 26
  7. abbrev OAI.ContinuumCoulomb.RationalGaussNodes.CoordinateInput line 34
  8. def OAI.ContinuumCoulomb.RationalGaussNodes.coordinateCode line 35
  9. opaque OAI.ContinuumCoulomb.RationalGaussNodes.coordinateParametersProgram line 37
  10. opaque OAI.ContinuumCoulomb.RationalGaussNodes.coordinateDataProgram line 39
  11. opaque OAI.ContinuumCoulomb.RationalGaussNodes.coordinatePrecisionProgram line 41
  12. opaque OAI.ContinuumCoulomb.RationalGaussNodes.coordinateDenominatorProgram line 43
  13. opaque OAI.ContinuumCoulomb.RationalGaussNodes.coordinateIntegerProgram line 45
  14. opaque OAI.ContinuumCoulomb.RationalGaussNodes.coordinateSignProgram line 47
  15. opaque OAI.ContinuumCoulomb.RationalGaussNodes.coordinateHalfProgram line 49
  16. opaque OAI.ContinuumCoulomb.RationalGaussNodes.coordinateProgram line 53
  17. opaque OAI.ContinuumCoulomb.RationalGaussNodes.dataProgram line 58
  18. opaque OAI.ContinuumCoulomb.RationalGaussNodes.parametersProgram line 60
  19. opaque OAI.ContinuumCoulomb.RationalGaussNodes.nodeDataProgram line 63
  20. opaque OAI.ContinuumCoulomb.RationalGaussNodes.registersProgram line 65
  21. opaque OAI.ContinuumCoulomb.RationalGaussNodes.signsProgram line 67
  22. opaque OAI.ContinuumCoulomb.RationalGaussNodes.signFirstProgram line 69
  23. opaque OAI.ContinuumCoulomb.RationalGaussNodes.signTailProgram line 70
  24. opaque OAI.ContinuumCoulomb.RationalGaussNodes.signSecondProgram line 72
  25. opaque OAI.ContinuumCoulomb.RationalGaussNodes.signThirdProgram line 74
  26. opaque OAI.ContinuumCoulomb.RationalGaussNodes.program line 77
  27. def OAI.ContinuumCoulomb.RationalGaussNodes.certificate line 87