OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CalibratedBisection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Deterministic bisection with the concrete hopping/Coulomb evaluator. The premises are endpoint signs and the already proved separated-site gap; there is no numeric evaluator assumption.

  1. abbrev OAI.ContinuumCoulomb.CalibratedEvaluation.BisectionInput line 15
  2. def OAI.ContinuumCoulomb.CalibratedEvaluation.bisectionInputCode line 17
  3. def OAI.ContinuumCoulomb.CalibratedEvaluation.tolerance line 20
  4. def OAI.ContinuumCoulomb.CalibratedEvaluation.bisectionArgument line 22
  5. def OAI.ContinuumCoulomb.CalibratedEvaluation.bisect line 25
  6. opaque OAI.ContinuumCoulomb.CalibratedEvaluation.bisectionArgumentProgram line 28
  7. def OAI.ContinuumCoulomb.CalibratedEvaluation.residual line 46
  8. def OAI.ContinuumCoulomb.CalibratedEvaluation.residualLipschitz line 50
  9. theorem OAI.ContinuumCoulomb.CalibratedEvaluation.bisect_residual line 54