OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactDisplacement.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Uniform displacement bounds for the explicit independent-length paths.

  1. theorem OAI.ContinuumCoulomb.adjustedContactForward_antitone line 11
  2. theorem OAI.ContinuumCoulomb.adjustedContactForward_near line 16
  3. theorem OAI.ContinuumCoulomb.contactHeight_near line 34
  4. theorem OAI.ContinuumCoulomb.adjustedContactStepX_near line 50
  5. theorem OAI.ContinuumCoulomb.adjustedContactStepY_near line 65
  6. theorem OAI.ContinuumCoulomb.contact_sum_error line 75
  7. theorem OAI.ContinuumCoulomb.adjustedContactVertex_displacement line 85

    Source documentation

    A uniform displacement bound with room for moving the path origin.

    theorem adjustedContactVertex_displacement {c h : ℝ} (hc : 3 / 4 ≤ c) (hc' : c ≤ 7 / 8)
    (hh : h ∈ Set.Icc (contactHeightLow c) (contactHeightHigh c))
    (lengths : ℕ → ℝ)
    (hl : ∀ j < 9, 1 - contactLengthTolerance ≤ lengths j)
    (hl' : ∀ j < 9, lengths j ≤ 1 + contactLengthTolerance) {k : ℕ} (hk : k ≤ 9) :
    dist (adjustedContactVertex lengths h k) (contactPathVertex c k) < 1 / 25 := by
…

    Mentions: OAI.ContinuumCoulomb.contactHeightLow, OAI.ContinuumCoulomb.contactHeightHigh, OAI.ContinuumCoulomb.contactLengthTolerance, OAI.ContinuumCoulomb.adjustedContactVertex, OAI.ContinuumCoulomb.contactPathVertex

  8. theorem OAI.ContinuumCoulomb.adjustedContactVertex_near line 122