OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/GraphCoefficientStability.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual shifted Heisenberg spectral bottom is stable under edgewise coefficient errors. This attaches numerical calibration to Hubbard's exact second-order identity without choosing a nearby exact root.

  1. theorem OAI.ContinuumCoulomb.HubbardGlobal.graphSourceForm_stability line 15
  2. theorem OAI.ContinuumCoulomb.HubbardGlobal.graphSourceBottom_minimizer line 37
  3. theorem OAI.ContinuumCoulomb.HubbardGlobal.graphSourceBottom_stability line 61
  4. theorem OAI.ContinuumCoulomb.HubbardGlobal.calibrated_graphSourceBottom_error line 73