OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/HoppingSchedule.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

An explicit polynomial mesh and inner precision for the actual compact hopping numerator. The displacement is an input rational, not an oracle.

  1. abbrev OAI.ContinuumCoulomb.HoppingSchedule.Input line 11
  2. def OAI.ContinuumCoulomb.HoppingSchedule.mesh line 13
  3. def OAI.ContinuumCoulomb.HoppingSchedule.accuracy line 14
  4. def OAI.ContinuumCoulomb.HoppingSchedule.argument line 16
  5. def OAI.ContinuumCoulomb.HoppingSchedule.approximate line 20
  6. theorem OAI.ContinuumCoulomb.HoppingSchedule.mesh_positive line 22
  7. theorem OAI.ContinuumCoulomb.HoppingSchedule.argument_step_nonnegative line 24
  8. theorem OAI.ContinuumCoulomb.HoppingSchedule.argument_endpoint line 28
  9. theorem OAI.ContinuumCoulomb.HoppingSchedule.argument_node_mem line 36
  10. theorem OAI.ContinuumCoulomb.HoppingSchedule.argument_nodes_norm line 45
  11. theorem OAI.ContinuumCoulomb.HoppingSchedule.numerical_budget line 56
  12. theorem OAI.ContinuumCoulomb.HoppingSchedule.approximation_error line 73