OAI/MathematicalPhysics/ContinuumCoulomb/Programs/CoulombEvaluationProgram.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

A single polynomial-time TM2 program for the actual localized Coulomb coefficient at every rational separation and unary precision.

  1. abbrev OAI.ContinuumCoulomb.CoulombEvaluation.Input line 11
  2. def OAI.ContinuumCoulomb.CoulombEvaluation.inputCode line 12
  3. opaque OAI.ContinuumCoulomb.CoulombEvaluation.scaleProgram line 14
  4. opaque OAI.ContinuumCoulomb.CoulombEvaluation.sixthProgram line 18
  5. opaque OAI.ContinuumCoulomb.CoulombEvaluation.truncationPrecisionProgram line 22
  6. opaque OAI.ContinuumCoulomb.CoulombEvaluation.capScaleProgram line 25
  7. opaque OAI.ContinuumCoulomb.CoulombEvaluation.denominatorProgram line 30
  8. opaque OAI.ContinuumCoulomb.CoulombEvaluation.radiusProgram line 33
  9. opaque OAI.ContinuumCoulomb.CoulombEvaluation.rawPrecisionProgram line 37
  10. opaque OAI.ContinuumCoulomb.CoulombEvaluation.volumeProgram line 41
  11. opaque OAI.ContinuumCoulomb.CoulombEvaluation.lipschitzProgram line 45
  12. opaque OAI.ContinuumCoulomb.CoulombEvaluation.meshProgram line 55
  13. opaque OAI.ContinuumCoulomb.CoulombEvaluation.samplePrecisionProgram line 62
  14. opaque OAI.ContinuumCoulomb.CoulombEvaluation.kernelPrecisionProgram line 69
  15. opaque OAI.ContinuumCoulomb.CoulombEvaluation.normalizationPrecisionProgram line 76
  16. opaque OAI.ContinuumCoulomb.CoulombEvaluation.radiusRationalProgram line 82
  17. opaque OAI.ContinuumCoulomb.CoulombEvaluation.meshRationalProgram line 87
  18. opaque OAI.ContinuumCoulomb.CoulombEvaluation.epsilonProgram line 92
  19. opaque OAI.ContinuumCoulomb.CoulombEvaluation.inputProgram line 98
  20. opaque OAI.ContinuumCoulomb.CoulombEvaluation.rawProgram line 117
  21. opaque OAI.ContinuumCoulomb.CoulombEvaluation.program line 121
  22. def OAI.ContinuumCoulomb.CoulombEvaluation.certificate line 128