OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CalibrationSquareError.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Scalar error propagation for the square root appearing in the calibrated hopping target. Negative numerical gaps are clipped at zero.

  1. theorem OAI.ContinuumCoulomb.clipped_difference_error line 11
  2. theorem OAI.ContinuumCoulomb.clipped_sqrt_difference_error line 22
  3. theorem OAI.ContinuumCoulomb.calibrated_residual_error line 34