OAI/MathematicalPhysics/ContinuumCoulomb/Programs/PlanarWellProgram.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The fixed well profile has an actual rational polynomial-time evaluator. The positive denominator guard is independent of all inputs.

  1. abbrev OAI.ContinuumCoulomb.PlanarWellNumerics.Input line 11
  2. def OAI.ContinuumCoulomb.PlanarWellNumerics.inputCode line 12
  3. opaque OAI.ContinuumCoulomb.PlanarWellNumerics.precisionProgram line 14
  4. opaque OAI.ContinuumCoulomb.PlanarWellNumerics.normSquareProgram line 18
  5. opaque OAI.ContinuumCoulomb.PlanarWellNumerics.program line 26
  6. def OAI.ContinuumCoulomb.PlanarWellNumerics.certificate line 51