OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CalibrationGraphBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A uniform coefficient budget for the actual calibrated Hubbard graph. The residual is measured against the analytic hopping target, while the conclusion concerns the finite-spin variational bottom.

  1. theorem OAI.ContinuumCoulomb.calibrated_coefficient_uniform_error line 13
  2. theorem OAI.ContinuumCoulomb.HubbardGlobal.calibrated_graphSourceBottom_uniform_error line 36