OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CalibratedBisectionLocation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Every returned rational remains in its original search interval. This geometric invariant does not need an accuracy or residual-sign hypothesis.

  1. theorem OAI.ContinuumCoulomb.bisection_step_nested line 10
  2. theorem OAI.ContinuumCoulomb.bisection_run_nested line 24
  3. theorem OAI.ContinuumCoulomb.bisection_value_mem line 36
  4. theorem OAI.ContinuumCoulomb.CalibratedEvaluation.bisect_mem line 49
  5. theorem OAI.ContinuumCoulomb.CalibratedEvaluation.scheduledValue_mem line 53