OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactMediatorGeometry.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Independent prescribed lengths for the exact nineteen local edges identified with the actual iterated mediator graph.

  1. abbrev OAI.ContinuumCoulomb.ContactMediator.ContactEdge line 11
  2. def OAI.ContinuumCoulomb.ContactMediator.leftEdge line 13
  3. def OAI.ContinuumCoulomb.ContactMediator.rightEdge line 24
  4. def OAI.ContinuumCoulomb.ContactMediator.edgeAt line 35
  5. def OAI.ContinuumCoulomb.ContactMediator.edgeIndex line 38
  6. def OAI.ContinuumCoulomb.ContactMediator.contactEdgeEquiv line 54
  7. theorem OAI.ContinuumCoulomb.ContactMediator.leftEdge_distance line 76
  8. theorem OAI.ContinuumCoulomb.ContactMediator.rightEdge_distance line 84
  9. def OAI.ContinuumCoulomb.ContactMediator.pathLengths line 94
  10. theorem OAI.ContinuumCoulomb.ContactMediator.exists_local_geometry line 97