OAI/MathematicalPhysics/ContinuumCoulomb/Programs/AutomaticCalibrationProgram.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The automatic distance program computes its polynomial query bounds, scale and inverse-power target from unary source size, then runs the certified rational-interval calibrated bisection.

  1. def OAI.ContinuumCoulomb.AutomaticCalibration.inputCode line 12
  2. def OAI.ContinuumCoulomb.AutomaticCalibration.unaryPowerProgram line 14
  3. opaque OAI.ContinuumCoulomb.AutomaticCalibration.baseProgram line 20
  4. opaque OAI.ContinuumCoulomb.AutomaticCalibration.tailProgram line 23
  5. opaque OAI.ContinuumCoulomb.AutomaticCalibration.precisionProgram line 26
  6. opaque OAI.ContinuumCoulomb.AutomaticCalibration.coefficientProgram line 29
  7. opaque OAI.ContinuumCoulomb.AutomaticCalibration.scaledSizeProgram line 32
  8. opaque OAI.ContinuumCoulomb.AutomaticCalibration.queryProgram line 35
  9. opaque OAI.ContinuumCoulomb.AutomaticCalibration.scaleProgram line 40
  10. opaque OAI.ContinuumCoulomb.AutomaticCalibration.targetScaleProgram line 43
  11. opaque OAI.ContinuumCoulomb.AutomaticCalibration.environmentProgram line 48
  12. opaque OAI.ContinuumCoulomb.AutomaticCalibration.intervalProgram line 53
  13. opaque OAI.ContinuumCoulomb.AutomaticCalibration.argumentProgram line 57
  14. opaque OAI.ContinuumCoulomb.AutomaticCalibration.program line 62
  15. def OAI.ContinuumCoulomb.AutomaticCalibration.certificate line 67