OAI/MathematicalPhysics/ContinuumCoulomb/Programs/CappedKernelProgram.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

A literal rational approximation of the bounded three-dimensional Coulomb kernel. Only a dyadic square root and rational arithmetic occur.

  1. abbrev OAI.ContinuumCoulomb.CappedKernelProgram.Triple line 14
  2. abbrev OAI.ContinuumCoulomb.CappedKernelProgram.Input line 15
  3. def OAI.ContinuumCoulomb.CappedKernelProgram.position line 17
  4. def OAI.ContinuumCoulomb.CappedKernelProgram.normSquare line 18
  5. def OAI.ContinuumCoulomb.CappedKernelProgram.approximate line 20
  6. theorem OAI.ContinuumCoulomb.CappedKernelProgram.normSquare_nonnegative line 23
  7. theorem OAI.ContinuumCoulomb.CappedKernelProgram.position_norm_sq line 27
  8. theorem OAI.ContinuumCoulomb.CappedKernelProgram.position_norm line 32
  9. theorem OAI.ContinuumCoulomb.CappedKernelProgram.approximation_error line 35
  10. def OAI.ContinuumCoulomb.CappedKernelProgram.tripleCode line 65
  11. def OAI.ContinuumCoulomb.CappedKernelProgram.inputCode line 66
  12. opaque OAI.ContinuumCoulomb.CappedKernelProgram.maximumProgram line 68
  13. opaque OAI.ContinuumCoulomb.CappedKernelProgram.normSquareProgram line 78
  14. opaque OAI.ContinuumCoulomb.CappedKernelProgram.program line 89
  15. def OAI.ContinuumCoulomb.CappedKernelProgram.certificate line 100