OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactRationalCoordinates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Rational contact vertices approximate the same exact height witness as the deterministic height solve. This estimate preserves separation margins when the requested precision is increased.

  1. def OAI.ContinuumCoulomb.ContactHeightEvaluation.stepX line 13
  2. def OAI.ContinuumCoulomb.ContactHeightEvaluation.stepY line 16
  3. def OAI.ContinuumCoulomb.ContactHeightEvaluation.vertex line 19
  4. def OAI.ContinuumCoulomb.ContactHeightEvaluation.vertexPoint line 23
  5. theorem OAI.ContinuumCoulomb.ContactHeightEvaluation.forward_lipschitz line 26
  6. theorem OAI.ContinuumCoulomb.ContactHeightEvaluation.stepX_error line 40
  7. theorem OAI.ContinuumCoulomb.ContactHeightEvaluation.stepY_error line 78
  8. theorem OAI.ContinuumCoulomb.ContactHeightEvaluation.contactPoint_dist_le_abs line 91
  9. theorem OAI.ContinuumCoulomb.ContactHeightEvaluation.vertex_error line 99