OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/PhysicalThreshold.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Canonical rational thresholds with the physical energy offset. The finite-model threshold is multiplied by lambda, while the one-particle reference energy is multiplied by lambda squared times the electron count.

  1. abbrev OAI.ContinuumCoulomb.PhysicalThreshold.Geometry line 13
  2. abbrev OAI.ContinuumCoulomb.PhysicalThreshold.Input line 14
  3. def OAI.ContinuumCoulomb.PhysicalThreshold.amplification line 16
  4. def OAI.ContinuumCoulomb.PhysicalThreshold.precision line 18
  5. def OAI.ContinuumCoulomb.PhysicalThreshold.reference line 21
  6. def OAI.ContinuumCoulomb.PhysicalThreshold.offset line 25
  7. def OAI.ContinuumCoulomb.PhysicalThreshold.value line 28
  8. def OAI.ContinuumCoulomb.PhysicalThreshold.actualReference line 32
  9. def OAI.ContinuumCoulomb.PhysicalThreshold.actualOffset line 35
  10. theorem OAI.ContinuumCoulomb.PhysicalThreshold.reference_error line 38
  11. theorem OAI.ContinuumCoulomb.PhysicalThreshold.amplification_bound line 58
  12. theorem OAI.ContinuumCoulomb.PhysicalThreshold.offset_error line 67
  13. theorem OAI.ContinuumCoulomb.PhysicalThreshold.lower_error line 99
  14. theorem OAI.ContinuumCoulomb.PhysicalThreshold.upper_error line 104
  15. theorem OAI.ContinuumCoulomb.PhysicalThreshold.gap line 109