OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/LocalizedOverlapSpacing.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

One fixed logarithmic spacing controls actual orbital Gram row sums for all polynomial site counts, with no independent small-overlap premise.

  1. theorem OAI.ContinuumCoulomb.localizedOverlapBound_log line 11
  2. theorem OAI.ContinuumCoulomb.exists_localizedOverlap_spacing line 19
  3. theorem OAI.ContinuumCoulomb.exists_uniform_localizedOrbitals line 46