OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CoulombPairEvaluation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Actual direct Coulomb coefficients at arbitrary rational planar sites. The distance is computed by the certified dyadic square-root program.

  1. def OAI.ContinuumCoulomb.CoulombPairEvaluation.lipschitzGuard line 14
  2. theorem OAI.ContinuumCoulomb.CoulombPairEvaluation.lipschitzGuard_positive line 17
  3. theorem OAI.ContinuumCoulomb.CoulombPairEvaluation.lipschitzGuard_bound line 21
  4. def OAI.ContinuumCoulomb.CoulombPairEvaluation.precision line 28
  5. def OAI.ContinuumCoulomb.CoulombPairEvaluation.rootPrecision line 29
  6. def OAI.ContinuumCoulomb.CoulombPairEvaluation.squaredDistance line 30
  7. def OAI.ContinuumCoulomb.CoulombPairEvaluation.distance line 31
  8. def OAI.ContinuumCoulomb.CoulombPairEvaluation.approximate line 33
  9. theorem OAI.ContinuumCoulomb.CoulombPairEvaluation.squaredDistance_cast line 36
  10. theorem OAI.ContinuumCoulomb.CoulombPairEvaluation.nat_pow_bound line 44
  11. theorem OAI.ContinuumCoulomb.CoulombPairEvaluation.distance_error line 49
  12. theorem OAI.ContinuumCoulomb.CoulombPairEvaluation.approximation_error line 61