OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactHeightEvaluation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A concrete rational evaluator for the one-dimensional height residual. There are exactly four dyadic square-root calls; all other terms are exact.

  1. abbrev OAI.ContinuumCoulomb.ContactHeightEvaluation.Environment line 12
  2. def OAI.ContinuumCoulomb.ContactHeightEvaluation.lengthAt line 14
  3. def OAI.ContinuumCoulomb.ContactHeightEvaluation.rootSample line 16
  4. def OAI.ContinuumCoulomb.ContactHeightEvaluation.value line 19
  5. def OAI.ContinuumCoulomb.ContactHeightEvaluation.residual line 23
  6. theorem OAI.ContinuumCoulomb.ContactHeightEvaluation.rootSample_error line 26
  7. theorem OAI.ContinuumCoulomb.ContactHeightEvaluation.four_errors line 41
  8. theorem OAI.ContinuumCoulomb.ContactHeightEvaluation.approximation_error line 50