OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CalibratedBisectionSchedule.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Polynomial unary iteration and evaluation-precision choices for the actual calibrated bisection.

  1. def OAI.ContinuumCoulomb.CalibratedEvaluation.refinedEnvironment line 11
  2. def OAI.ContinuumCoulomb.CalibratedEvaluation.iterations line 14
  3. def OAI.ContinuumCoulomb.CalibratedEvaluation.scheduledValue line 17
  4. theorem OAI.ContinuumCoulomb.CalibratedEvaluation.bisection_scalar_budget line 20
  5. theorem OAI.ContinuumCoulomb.CalibratedEvaluation.scheduled_residual line 51