OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactRationalGadget.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

A concrete rational twenty-site gadget. The two paths share the same rational prescribed span; their outer endpoints are exact and their internal vertices approximate the original independent-length gadget.

  1. abbrev OAI.ContinuumCoulomb.ContactRationalGadget.Input line 14
  2. def OAI.ContinuumCoulomb.ContactRationalGadget.span line 16
  3. def OAI.ContinuumCoulomb.ContactRationalGadget.origin line 19
  4. def OAI.ContinuumCoulomb.ContactRationalGadget.leftEnvironment line 22
  5. def OAI.ContinuumCoulomb.ContactRationalGadget.rightEnvironment line 25
  6. def OAI.ContinuumCoulomb.ContactRationalGadget.position line 28
  7. def OAI.ContinuumCoulomb.ContactRationalGadget.point line 35
  8. def OAI.ContinuumCoulomb.ContactRationalGadget.leftLengths line 38
  9. def OAI.ContinuumCoulomb.ContactRationalGadget.rightLengths line 39
  10. theorem OAI.ContinuumCoulomb.ContactRationalGadget.span_cast line 41
  11. theorem OAI.ContinuumCoulomb.ContactRationalGadget.origin_cast line 45
  12. theorem OAI.ContinuumCoulomb.ContactRationalGadget.point_left line 49
  13. theorem OAI.ContinuumCoulomb.ContactRationalGadget.point_right line 52
  14. theorem OAI.ContinuumCoulomb.ContactRationalGadget.point_side line 61
  15. theorem OAI.ContinuumCoulomb.ContactRationalGadget.point_start line 68
  16. theorem OAI.ContinuumCoulomb.ContactRationalGadget.point_end line 72
  17. theorem OAI.ContinuumCoulomb.ContactRationalGadget.point_near_reference line 84
  18. theorem OAI.ContinuumCoulomb.ContactRationalGadget.exists_reference line 122
  19. theorem OAI.ContinuumCoulomb.ContactRationalGadget.reference_near_base line 148