OAI/MathematicalPhysics/ContinuumCoulomb/Programs/PrefactorCalibrationProgram.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The fixed rational prefactor needs only two extra arithmetic operations before the existing certified calibration program.

  1. opaque OAI.ContinuumCoulomb.PrefactorCalibration.weightProgram line 11
  2. opaque OAI.ContinuumCoulomb.PrefactorCalibration.precisionProgram line 15
  3. opaque OAI.ContinuumCoulomb.PrefactorCalibration.inputProgram line 18
  4. opaque OAI.ContinuumCoulomb.PrefactorCalibration.program line 26
  5. def OAI.ContinuumCoulomb.PrefactorCalibration.certificate line 30
  6. opaque OAI.ContinuumCoulomb.PrefactorCalibration.normalizedProgram line 34
  7. def OAI.ContinuumCoulomb.PrefactorCalibration.normalizedCertificate line 39