OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactRationalLocal.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Rational contact coordinates indexed by the actual nineteen local mediator edges. Every link has a quantitative error and the nonedge margin survives with a fixed minimum requested precision.

  1. def OAI.ContinuumCoulomb.ContactRationalLocal.input line 14
  2. def OAI.ContinuumCoulomb.ContactRationalLocal.position line 19
  3. def OAI.ContinuumCoulomb.ContactRationalLocal.point line 22
  4. theorem OAI.ContinuumCoulomb.ContactRationalLocal.length_ofFn line 25
  5. theorem OAI.ContinuumCoulomb.ContactRationalLocal.left_length line 30
  6. theorem OAI.ContinuumCoulomb.ContactRationalLocal.right_length line 36
  7. theorem OAI.ContinuumCoulomb.ContactRationalLocal.distance_error line 42
  8. theorem OAI.ContinuumCoulomb.ContactRationalLocal.exists_link_approximation line 49
  9. theorem OAI.ContinuumCoulomb.ContactRationalLocal.nonedge_separation line 110
  10. theorem OAI.ContinuumCoulomb.ContactRationalLocal.near_base line 132