OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/ComputableAmplification.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Rational Taylor construction of the large charge scale

Only 4D²+4 rational Taylor terms are used. The absolute exponential error is at most one half, so rounding this explicit rational number gives the constant-factor amplification required by the construction. No real-number floor operation or unknown spectral quantity occurs in the algorithm.

  1. def OAI.ContinuumCoulomb.amplificationOrder line 19
  2. def OAI.ContinuumCoulomb.amplificationTaylor line 21
  3. def OAI.ContinuumCoulomb.taylorAmplification line 24
  4. theorem OAI.ContinuumCoulomb.amplification_factorial_bound line 26
  5. theorem OAI.ContinuumCoulomb.amplificationTaylor_error line 51
  6. theorem OAI.ContinuumCoulomb.amplificationTaylor_ge_scale line 76
  7. theorem OAI.ContinuumCoulomb.taylorAmplification_ge_scale line 85
  8. theorem OAI.ContinuumCoulomb.taylorAmplification_pos line 90
  9. theorem OAI.ContinuumCoulomb.taylorAmplification_bounds line 94