OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/RationalExponential.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A rational Taylor approximation with an explicit magnitude and binary precision parameter. This applies to the negative rational exponents in the Gaussian heat kernel as well as to positive arguments.

  1. def OAI.ContinuumCoulomb.RationalExponential.order line 13
  2. def OAI.ContinuumCoulomb.RationalExponential.taylorSum line 15
  3. def OAI.ContinuumCoulomb.RationalExponential.approximate line 18
  4. theorem OAI.ContinuumCoulomb.RationalExponential.factorial_bound line 20
  5. theorem OAI.ContinuumCoulomb.RationalExponential.error line 40