OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRawCoefficientBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounds for the actual rational four-spin coefficients. The sampling precision does not enter these bounds.

  1. theorem OAI.ContinuumCoulomb.QuantumAxisSample.fieldValue_abs line 11
  2. theorem OAI.ContinuumCoulomb.QuantumAxisSample.crossValue_abs line 20
  3. theorem OAI.ContinuumCoulomb.QuantumAxisSample.shiftValue_abs line 33
  4. theorem OAI.ContinuumCoulomb.QuantumAxisSample.offset_abs line 39