OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/MoserVelocityNumerics.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Stable algebraic evaluation of the actual Moser velocity. The denominator is clamped below by the fixed positive density; this clamp does not affect the exact field and cannot increase denominator error.

  1. theorem OAI.ContinuumCoulomb.MoserVelocityNumerics.component_formula line 14
  2. theorem OAI.ContinuumCoulomb.MoserVelocityNumerics.denominator_lower line 24
  3. theorem OAI.ContinuumCoulomb.MoserVelocityNumerics.clamp_error line 39
  4. theorem OAI.ContinuumCoulomb.MoserVelocityNumerics.quotient_error line 47
  5. theorem OAI.ContinuumCoulomb.MoserVelocityNumerics.component_error line 74