OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/RationalSquareRoot.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Certified evaluation of square roots of nonnegative rational samples. The same finite dyadic procedure serves the fixed Gaussian constants and softened Coulomb distances.

  1. def OAI.ContinuumCoulomb.RationalSquareRoot.value line 13
  2. def OAI.ContinuumCoulomb.RationalSquareRoot.inputCode line 16
  3. opaque OAI.ContinuumCoulomb.RationalSquareRoot.argumentProgram line 18
  4. opaque OAI.ContinuumCoulomb.RationalSquareRoot.program line 26
  5. def OAI.ContinuumCoulomb.RationalSquareRoot.certificate line 29
  6. theorem OAI.ContinuumCoulomb.RationalSquareRoot.value_error line 32
  7. theorem OAI.ContinuumCoulomb.RationalSquareRoot.sqrt_perturbation line 45