OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/AffinePhysicalThreshold.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The complete scalar shift in the unit-charge construction. Input endpoints already contain the exact mediator offset. The remaining finite shift is the sum of edge weights and the off-site Coulomb energy; only the latter and the one-particle reference require numerical approximation.

  1. abbrev OAI.ContinuumCoulomb.AffinePhysicalThreshold.Input line 14
  2. def OAI.ContinuumCoulomb.AffinePhysicalThreshold.pairPrecision line 16
  3. def OAI.ContinuumCoulomb.AffinePhysicalThreshold.pairValue line 19
  4. def OAI.ContinuumCoulomb.AffinePhysicalThreshold.finiteValue line 22
  5. def OAI.ContinuumCoulomb.AffinePhysicalThreshold.argument line 26
  6. def OAI.ContinuumCoulomb.AffinePhysicalThreshold.value line 29
  7. def OAI.ContinuumCoulomb.AffinePhysicalThreshold.exactFinite line 32
  8. def OAI.ContinuumCoulomb.AffinePhysicalThreshold.exactValue line 36
  9. theorem OAI.ContinuumCoulomb.AffinePhysicalThreshold.pair_budget line 42
  10. theorem OAI.ContinuumCoulomb.AffinePhysicalThreshold.reference_budget line 54
  11. theorem OAI.ContinuumCoulomb.AffinePhysicalThreshold.value_error line 60
  12. theorem OAI.ContinuumCoulomb.AffinePhysicalThreshold.actual_error line 104
  13. theorem OAI.ContinuumCoulomb.AffinePhysicalThreshold.gap line 115