OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/RationalSmoothTransition.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Rational approximation of the explicit smooth transition. Exponents near the flat junction are truncated before Taylor evaluation, keeping both the magnitude parameter and the error polynomial in the precision.

  1. def OAI.ContinuumCoulomb.RationalSmoothTransition.clip line 13
  2. theorem OAI.ContinuumCoulomb.RationalSmoothTransition.clip_bounds line 15
  3. theorem OAI.ContinuumCoulomb.RationalSmoothTransition.clip_error line 20
  4. def OAI.ContinuumCoulomb.RationalSmoothTransition.flat line 36
  5. theorem OAI.ContinuumCoulomb.RationalSmoothTransition.flat_bounds line 41
  6. theorem OAI.ContinuumCoulomb.RationalSmoothTransition.two_pow_bound line 47
  7. theorem OAI.ContinuumCoulomb.RationalSmoothTransition.flat_error line 54
  8. theorem OAI.ContinuumCoulomb.RationalSmoothTransition.transition_denominator_lower line 100
  9. def OAI.ContinuumCoulomb.RationalSmoothTransition.precision line 117
  10. def OAI.ContinuumCoulomb.RationalSmoothTransition.approximate line 119
  11. theorem OAI.ContinuumCoulomb.RationalSmoothTransition.quotient_error line 122
  12. theorem OAI.ContinuumCoulomb.RationalSmoothTransition.approximation_error line 158