OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CoulombTruncationSchedule.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Explicit polynomial cap and box schedules. The single natural guard is fixed by the fixed one-well density; it is not an input or an oracle.

  1. def OAI.ContinuumCoulomb.CoulombTruncationSchedule.guard line 11
  2. def OAI.ContinuumCoulomb.CoulombTruncationSchedule.scale line 15
  3. def OAI.ContinuumCoulomb.CoulombTruncationSchedule.radius line 16
  4. def OAI.ContinuumCoulomb.CoulombTruncationSchedule.epsilon line 17
  5. theorem OAI.ContinuumCoulomb.CoulombTruncationSchedule.guard_one_le line 19
  6. theorem OAI.ContinuumCoulomb.CoulombTruncationSchedule.guard_cap line 26
  7. theorem OAI.ContinuumCoulomb.CoulombTruncationSchedule.guard_tail line 35
  8. theorem OAI.ContinuumCoulomb.CoulombTruncationSchedule.scale_eight_le line 44
  9. theorem OAI.ContinuumCoulomb.CoulombTruncationSchedule.epsilon_positive line 48
  10. theorem OAI.ContinuumCoulomb.CoulombTruncationSchedule.radius_positive line 54
  11. theorem OAI.ContinuumCoulomb.CoulombTruncationSchedule.scalar_budget line 60
  12. theorem OAI.ContinuumCoulomb.CoulombTruncationSchedule.error line 83