OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PrefactorCalibration.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A fixed positive rational prefactor in the physical amplification is absorbed into the requested edge weight. This retains the proved evaluator and bisection, including their polynomial running times.

  1. def OAI.ContinuumCoulomb.PrefactorCalibration.adjustedWeight line 12
  2. def OAI.ContinuumCoulomb.PrefactorCalibration.precision line 13
  3. def OAI.ContinuumCoulomb.PrefactorCalibration.input line 14
  4. def OAI.ContinuumCoulomb.PrefactorCalibration.value line 16
  5. def OAI.ContinuumCoulomb.PrefactorCalibration.normalizedValue line 19
  6. theorem OAI.ContinuumCoulomb.PrefactorCalibration.normalizedValue_mem line 23
  7. theorem OAI.ContinuumCoulomb.PrefactorCalibration.target_scale line 29
  8. theorem OAI.ContinuumCoulomb.PrefactorCalibration.weight_polynomial_range line 37
  9. theorem OAI.ContinuumCoulomb.PrefactorCalibration.precision_error line 57
  10. theorem OAI.ContinuumCoulomb.PrefactorCalibration.exists_calibration line 65