OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumSamplePrecision.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic precision, computed from binary numerators, suffices for the physical error budget.

  1. def OAI.ContinuumCoulomb.QuantumAxisSample.precision line 11
  2. theorem OAI.ContinuumCoulomb.QuantumAxisSample.rational_le_numerator line 13
  3. theorem OAI.ContinuumCoulomb.QuantumAxisSample.precision_error line 25
  4. def OAI.ContinuumCoulomb.QuantumAxisSample.precisionCode line 41
  5. opaque OAI.ContinuumCoulomb.QuantumAxisSample.numeratorMagnitudeProgram line 43
  6. opaque OAI.ContinuumCoulomb.QuantumAxisSample.numeratorSizeProgram line 47
  7. opaque OAI.ContinuumCoulomb.QuantumAxisSample.denominatorSizeProgram line 52
  8. opaque OAI.ContinuumCoulomb.QuantumAxisSample.precisionProgram line 56
  9. def OAI.ContinuumCoulomb.QuantumAxisSample.precisionCertificate line 59