OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactClosedCoordinates.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The rational path keeps both original endpoints exact. Replacing its last approximate prefix sum by the prescribed span improves its distance to the exact reference path and does not change the polynomial program.

  1. def OAI.ContinuumCoulomb.ContactHeightEvaluation.closedVertex line 13
  2. def OAI.ContinuumCoulomb.ContactHeightEvaluation.closedVertexPoint line 16
  3. theorem OAI.ContinuumCoulomb.ContactHeightEvaluation.closedVertex_start line 19
  4. theorem OAI.ContinuumCoulomb.ContactHeightEvaluation.closedVertex_end line 22
  5. theorem OAI.ContinuumCoulomb.ContactHeightEvaluation.closedVertex_error line 25
  6. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.closedVertexProgram line 41
  7. def OAI.ContinuumCoulomb.ContactHeightEvaluation.closedVertexListProgram line 53
  8. def OAI.ContinuumCoulomb.ContactHeightEvaluation.closedVertexListCertificate line 67