OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactHeightBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Uniform direct and inverse moduli for the nine-link height solve. The four sloping links keep this one-dimensional solve quantitatively regular.

  1. theorem OAI.ContinuumCoulomb.contactHeight_interval_bounds line 11
  2. theorem OAI.ContinuumCoulomb.adjustedContactForward_slope line 22
  3. theorem OAI.ContinuumCoulomb.adjustedContactSpan_broad_slope line 58
  4. theorem OAI.ContinuumCoulomb.adjustedContactSpan_slope line 76
  5. theorem OAI.ContinuumCoulomb.adjustedContactSpan_broad_inverse_error line 88
  6. theorem OAI.ContinuumCoulomb.adjustedContactSpan_inverse_error line 108
  7. theorem OAI.ContinuumCoulomb.adjustedContactSpan_broad_lipschitz line 120