OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ManufacturedOrbitalNuclearError.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual uncut orbital matrix elements of the manufactured grid potential. The only external analytic input is the published C4 flow theorem.

  1. theorem OAI.ContinuumCoulomb.manufactured_orbital_nuclear_error line 15