OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CoulombPairSum.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The actual scalar direct-interaction offset is one half of the ordered off-diagonal Coulomb sum. The finite list evaluator excludes only identical coordinates; injectivity identifies that test with the diagonal.

  1. abbrev OAI.ContinuumCoulomb.CoulombPairSum.Point line 13
  2. abbrev OAI.ContinuumCoulomb.CoulombPairSum.Input line 14
  3. def OAI.ContinuumCoulomb.CoulombPairSum.offsite line 16
  4. def OAI.ContinuumCoulomb.CoulombPairSum.row line 20
  5. def OAI.ContinuumCoulomb.CoulombPairSum.total line 23
  6. def OAI.ContinuumCoulomb.CoulombPairSum.exactTotal line 26
  7. theorem OAI.ContinuumCoulomb.CoulombPairSum.row_error line 31
  8. theorem OAI.ContinuumCoulomb.CoulombPairSum.total_error line 57
  9. def OAI.ContinuumCoulomb.CoulombPairSum.precision line 76
  10. def OAI.ContinuumCoulomb.CoulombPairSum.value line 77
  11. theorem OAI.ContinuumCoulomb.CoulombPairSum.precision_budget line 79
  12. theorem OAI.ContinuumCoulomb.CoulombPairSum.error line 89