OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CorrectedRemainderGap.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The manufactured spectral gap applies to the actual weak-H1 remainder of the finite corrected-orbital projection, with an exact mass deficit.

  1. theorem OAI.ContinuumCoulomb.manufacturedSlab_projected_remainder_gap line 12