OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumAxisSample.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Rational sampling of the fixed algebraic constants in the four-spin encoding.

  1. def OAI.ContinuumCoulomb.QuantumAxisSample.inverseScale line 12
  2. theorem OAI.ContinuumCoulomb.QuantumAxisSample.inverseScale_mul line 14
  3. theorem OAI.ContinuumCoulomb.QuantumAxisSample.inverseScale_bounds line 21
  4. def OAI.ContinuumCoulomb.QuantumAxisSample.value line 29
  5. theorem OAI.ContinuumCoulomb.QuantumAxisSample.root_nonneg line 32
  6. theorem OAI.ContinuumCoulomb.QuantumAxisSample.value_nonneg line 36
  7. theorem OAI.ContinuumCoulomb.QuantumAxisSample.value_error line 42
  8. theorem OAI.ContinuumCoulomb.QuantumAxisSample.value_bounds line 54
  9. theorem OAI.ContinuumCoulomb.QuantumAxisSample.product_error line 68
  10. def OAI.ContinuumCoulomb.QuantumAxisSample.radicand line 86
  11. theorem OAI.ContinuumCoulomb.QuantumAxisSample.radicand_nonneg line 88
  12. theorem OAI.ContinuumCoulomb.QuantumAxisSample.coupling_eq line 93
  13. theorem OAI.ContinuumCoulomb.QuantumAxisSample.radicand_error line 106
  14. def OAI.ContinuumCoulomb.QuantumAxisSample.coupling line 120
  15. theorem OAI.ContinuumCoulomb.QuantumAxisSample.coupling_error line 123