OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCountertermSample.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The counterterms use only rational arithmetic and the fixed inverse-scale sample.

  1. theorem OAI.ContinuumCoulomb.QuantumAxisSample.factor_eq line 11
  2. theorem OAI.ContinuumCoulomb.QuantumAxisSample.counterA_eq line 23
  3. theorem OAI.ContinuumCoulomb.QuantumAxisSample.counterB_eq line 30
  4. def OAI.ContinuumCoulomb.QuantumAxisSample.shift line 38
  5. def OAI.ContinuumCoulomb.QuantumAxisSample.polarity line 39
  6. theorem OAI.ContinuumCoulomb.QuantumAxisSample.shift_cast line 41
  7. theorem OAI.ContinuumCoulomb.QuantumAxisSample.polarity_cast line 45
  8. theorem OAI.ContinuumCoulomb.QuantumAxisSample.sign_cast line 52
  9. def OAI.ContinuumCoulomb.QuantumAxisSample.factor line 57
  10. def OAI.ContinuumCoulomb.QuantumAxisSample.counterA line 58
  11. def OAI.ContinuumCoulomb.QuantumAxisSample.counterB line 59
  12. theorem OAI.ContinuumCoulomb.QuantumAxisSample.factor_error line 61
  13. theorem OAI.ContinuumCoulomb.QuantumAxisSample.counterA_error line 73
  14. theorem OAI.ContinuumCoulomb.QuantumAxisSample.counterB_error line 88