OAI/MathematicalPhysics/ContinuumCoulomb/Programs/CoulombNormalizationProgram.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A certified rational evaluator for the fixed Coulomb normalization factor. The natural guard depends only on the fixed one-well model.

  1. def OAI.ContinuumCoulomb.CoulombNormalization.guard line 12
  2. def OAI.ContinuumCoulomb.CoulombNormalization.coefficient line 15
  3. def OAI.ContinuumCoulomb.CoulombNormalization.factorBound line 16
  4. def OAI.ContinuumCoulomb.CoulombNormalization.precision line 17
  5. def OAI.ContinuumCoulomb.CoulombNormalization.approximate line 20
  6. theorem OAI.ContinuumCoulomb.CoulombNormalization.guard_bounds line 25
  7. theorem OAI.ContinuumCoulomb.CoulombNormalization.precision_bounds line 44
  8. theorem OAI.ContinuumCoulomb.CoulombNormalization.approximation_error line 73
  9. opaque OAI.ContinuumCoulomb.CoulombNormalization.precisionProgram line 96
  10. opaque OAI.ContinuumCoulomb.CoulombNormalization.piCountProgram line 101
  11. opaque OAI.ContinuumCoulomb.CoulombNormalization.program line 106
  12. def OAI.ContinuumCoulomb.CoulombNormalization.certificate line 115