OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/EulerSchedule.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Polynomial step count, sample precision, and register denominator for unit-time integration with fixed speed/Lipschitz guards. The same step count is used as the velocity sample precision.

  1. def OAI.ContinuumCoulomb.EulerRegisters.steps line 11
  2. def OAI.ContinuumCoulomb.EulerRegisters.denominator line 12
  3. theorem OAI.ContinuumCoulomb.EulerRegisters.steps_positive line 14
  4. theorem OAI.ContinuumCoulomb.EulerRegisters.schedule_budget line 18