HydrogenInput.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Minimal published hydrogen input for isolated-well energies

Gerald Teschl, Mathematical Methods in Quantum Mechanics, second edition, AMS Graduate Studies in Mathematics 157 (2014), Theorem 10.10, equations (10.5) and (10.64): the lowest eigenvalue of -Δ-γ/|x| is -γ²/4. Set γ=2, divide the operator by two, and translate the centre. The exact specialization used below is PublishedHydrogenBottom. Spin contributes two identical summands and does not alter the bottom. https://www.mat.univie.ac.at/~gerald/ftp/book-schroe/schroe2.pdf .

This conditional interface assumes the unperturbed hydrogen bottom. The isolated-well comparison follows by a variational perturbation argument.

def OAI.ContinuumCoulomb.PublishedHydrogenBottom line 24
Source documentation
Exact published hydrogen bottom, specialized to the unperturbed well.
```
def PublishedHydrogenBottom : Prop :=
…
```
theorem OAI.ContinuumCoulomb.isolatedWellEnergy_near_hydrogen line 27
theorem OAI.ContinuumCoulomb.binary_isolatedWellEnergy_bound line 49
Source documentation
The actual rationally computed integer charges give the required uniform energy closeness throughout the displacement cube, conditionally only on the published unperturbed hydrogen bottom.
```
theorem binary_isolatedWellEnergy_bound (hhydrogen : PublishedHydrogenBottom)
    {D m : ℕ} (hm : 0 < m) (hscale : 10010 * m ≤ D)
    (center displacement : Fin m → Position) (hdisp : ∀ j, ‖displacement j‖ ≤ 4)
    (site : Fin m) :
    |(isolatedWellEnergy D (binaryPrimaryRatio D m) (binarySecondaryRatio D m)
      center displacement site).toReal + 1 / 2| ≤ 45045 * m / (D : ℝ) := by
…
```
Mentions: OAI.ContinuumCoulomb.PublishedHydrogenBottom, OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.isolatedWellEnergy, OAI.ContinuumCoulomb.binaryPrimaryRatio, OAI.ContinuumCoulomb.binarySecondaryRatio