OAI/MathematicalPhysics/ContinuumCoulomb/Programs/BisectionProgram.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Literal polynomial-time bisection with a supplied polynomial-time rational evaluator. The evaluator environment and tolerance remain in the input registers; they are not fixed nonuniform advice.

  1. abbrev OAI.ContinuumCoulomb.BisectionProgram.Config line 14
  2. def OAI.ContinuumCoulomb.BisectionProgram.configCode line 16
  3. def OAI.ContinuumCoulomb.BisectionProgram.advance line 19
  4. theorem OAI.ContinuumCoulomb.BisectionProgram.iterate_config line 22
  5. theorem OAI.ContinuumCoulomb.BisectionProgram.config_length line 31
  6. theorem OAI.ContinuumCoulomb.BisectionProgram.iterate_code_bound line 37
  7. def OAI.ContinuumCoulomb.BisectionProgram.rationalLess line 51
  8. def OAI.ContinuumCoulomb.BisectionProgram.middleProgram line 59
  9. def OAI.ContinuumCoulomb.BisectionProgram.advanceProgram line 68
  10. def OAI.ContinuumCoulomb.BisectionProgram.repeatProgram line 103
  11. def OAI.ContinuumCoulomb.BisectionProgram.initialProgram line 111
  12. abbrev OAI.ContinuumCoulomb.BisectionProgram.Input line 126
  13. def OAI.ContinuumCoulomb.BisectionProgram.inputCode line 128
  14. def OAI.ContinuumCoulomb.BisectionProgram.approximate line 132
  15. def OAI.ContinuumCoulomb.BisectionProgram.program line 135
  16. def OAI.ContinuumCoulomb.BisectionProgram.certificate line 154
  17. theorem OAI.ContinuumCoulomb.BisectionProgram.residual line 160