OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactHeightBisection.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The height search uses fixed rational endpoints, its concrete evaluator, and a linear unary precision schedule. The reference height is supplied by the already proved contact intermediate-value theorem.

  1. def OAI.ContinuumCoulomb.ContactHeightEvaluation.tolerance line 13
  2. def OAI.ContinuumCoulomb.ContactHeightEvaluation.argument line 15
  3. def OAI.ContinuumCoulomb.ContactHeightEvaluation.bisect line 18
  4. def OAI.ContinuumCoulomb.ContactHeightEvaluation.refinedEnvironment line 21
  5. def OAI.ContinuumCoulomb.ContactHeightEvaluation.iterations line 23
  6. def OAI.ContinuumCoulomb.ContactHeightEvaluation.scheduledValue line 25
  7. theorem OAI.ContinuumCoulomb.ContactHeightEvaluation.bisect_mem line 27
  8. theorem OAI.ContinuumCoulomb.ContactHeightEvaluation.endpoint_signs line 36
  9. theorem OAI.ContinuumCoulomb.ContactHeightEvaluation.bisect_residual line 49
  10. theorem OAI.ContinuumCoulomb.ContactHeightEvaluation.scheduled_residual line 84
  11. theorem OAI.ContinuumCoulomb.ContactHeightEvaluation.scheduled_height_error line 124
  12. theorem OAI.ContinuumCoulomb.ContactHeightEvaluation.exists_scheduled_height_error line 140