OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarGapFromUniqueness.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual planar well has a positive excitation gap once its zero-form space is the line of the proved normalized ground mode. Compactness here is proved directly, with no spectral or planar-gap input used.

  1. theorem OAI.ContinuumCoulomb.PlanarSobolev.normalized_gap_of_ground_uniqueness line 19
  2. theorem OAI.ContinuumCoulomb.PlanarSobolev.shiftedForm_smul line 61
  3. theorem OAI.ContinuumCoulomb.PlanarSobolev.planar_gap_of_ground_uniqueness line 69