OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/SourceHubbardEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact finite-spin and scalar-offset identities for the literal source bond list. These identify the Hubbard center with the computed threshold center.

  1. theorem OAI.ContinuumCoulomb.source_graph_bottom line 14
  2. def OAI.ContinuumCoulomb.SourcePhysicalThreshold.exactHubbardEnergy line 34
  3. theorem OAI.ContinuumCoulomb.SourcePhysicalThreshold.hubbard_center_error line 45
  4. theorem OAI.ContinuumCoulomb.SourcePhysicalThreshold.exactHubbardEnergy_eq line 79