OAI/MathematicalPhysics/ContinuumCoulomb/Programs/SmoothTransitionProgram.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Literal polynomial-time rational programs for the smooth transition and the fixed transverse cutoff. All large parameters are unary and each Taylor exponent has already been bounded in RationalSmoothTransition.

  1. abbrev OAI.ContinuumCoulomb.SmoothTransitionProgram.Input line 15
  2. def OAI.ContinuumCoulomb.SmoothTransitionProgram.inputCode line 16
  3. opaque OAI.ContinuumCoulomb.SmoothTransitionProgram.clipProgram line 18
  4. opaque OAI.ContinuumCoulomb.SmoothTransitionProgram.flatProgram line 34
  5. opaque OAI.ContinuumCoulomb.SmoothTransitionProgram.precisionProgram line 55
  6. opaque OAI.ContinuumCoulomb.SmoothTransitionProgram.program line 59
  7. def OAI.ContinuumCoulomb.SmoothTransitionProgram.certificate line 70
  8. def OAI.ContinuumCoulomb.SmoothTransitionProgram.cutoffArgument line 74
  9. def OAI.ContinuumCoulomb.SmoothTransitionProgram.cutoff line 75
  10. opaque OAI.ContinuumCoulomb.SmoothTransitionProgram.cutoffArgumentProgram line 78
  11. opaque OAI.ContinuumCoulomb.SmoothTransitionProgram.cutoffProgram line 86
  12. def OAI.ContinuumCoulomb.SmoothTransitionProgram.cutoffCertificate line 90