OAI/MathematicalPhysics/ContinuumCoulomb/Programs/CoulombPairSumProgram.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The direct-interaction scalar uses two literal finite list traversals; its precision increases only polynomially with the number of sites.

  1. def OAI.ContinuumCoulomb.CoulombPairSum.pointCode line 12
  2. def OAI.ContinuumCoulomb.CoulombPairSum.inputCode line 13
  3. def OAI.ContinuumCoulomb.CoulombPairSum.rowCode line 14
  4. opaque OAI.ContinuumCoulomb.CoulombPairSum.offsiteProgram line 17
  5. opaque OAI.ContinuumCoulomb.CoulombPairSum.offsiteEnvironmentProgram line 28
  6. opaque OAI.ContinuumCoulomb.CoulombPairSum.rowProgram line 37
  7. opaque OAI.ContinuumCoulomb.CoulombPairSum.rowEnvironmentProgram line 49
  8. opaque OAI.ContinuumCoulomb.CoulombPairSum.totalProgram line 57
  9. opaque OAI.ContinuumCoulomb.CoulombPairSum.lengthProgram line 67
  10. opaque OAI.ContinuumCoulomb.CoulombPairSum.precisionProgram line 71
  11. opaque OAI.ContinuumCoulomb.CoulombPairSum.argumentProgram line 77
  12. opaque OAI.ContinuumCoulomb.CoulombPairSum.program line 81
  13. def OAI.ContinuumCoulomb.CoulombPairSum.certificate line 85