OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CalibratedEvaluationError.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Certified evaluation of the actual calibrated hopping residual, uniformly on rational points in a bounded interval.

  1. theorem OAI.ContinuumCoulomb.CalibratedEvaluation.approximation_error line 11