PlanarSpectralInput.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The published negative-ground-energy gap consequence used conditionally.

Gerald Teschl, Mathematical Methods in Quantum Mechanics, second edition, AMS Graduate Studies in Mathematics 157 (2014), Theorems 10.2, 10.13 and 4.12 (including its quadratic-form-domain version). Author's text: https://www.mat.univie.ac.at/~gerald/ftp/book-schroe/schroe2.pdf

For a bounded compactly supported real potential in dimension two, Theorem 10.2 gives the self-adjoint Schrödinger operator, its smooth compact core and essential spectrum [0,∞). Theorem 10.13 makes an attained ground energy simple. At a negative ground energy the next max-min value is strictly larger; Theorem 4.12 states the corresponding inequality on the form domain. Below we assume only that useful form consequence, then apply it to the actual manufactured well and its attained bottom. The spectral consequence is a premise of this conditional interface.

def OAI.ContinuumCoulomb.PlanarSobolev.compactPotentialForm line 32
def OAI.ContinuumCoulomb.PlanarSobolev.PublishedNegativePlanarGroundGap line 39
Source documentation
The negative-ground-energy specialization of Teschl's Theorems 10.2, 10.13 and 4.12. Its premises and conclusion concern the actual closed H¹ graph and the actual multiplication operator for a compact C¹ potential.
```
def PublishedNegativePlanarGroundGap : Prop :=
…
```
theorem OAI.ContinuumCoulomb.PlanarSobolev.compactPotentialForm_well line 47
def OAI.ContinuumCoulomb.PlanarSobolev.ManufacturedPlanarGroundGap line 52
Source documentation
The single well-specific consequence actually used by the construction.
```
def ManufacturedPlanarGroundGap : Prop :=
…
```
theorem OAI.ContinuumCoulomb.PlanarSobolev.manufacturedPlanarWell_gap line 60
Source documentation
Conditional gap for the actual resolvent-generated well, using only the published spectral consequence above. Membership, normalization and energy of this specific mode and the all-domain lower bound are proved separately.
```
theorem manufacturedPlanarWell_gap (hpublished : PublishedNegativePlanarGroundGap) :
    ∃ γ : ℝ, 0 < γ ∧ ∀ u : Sobolev,
      inner ℝ u.val.1 normalizedMode.val.1 = 0 →
      ((-1 / 2 : ℝ) + γ) * ‖u.val.1‖ ^ 2 ≤ form u.val := by
…
```
Mentions: OAI.ContinuumCoulomb.PlanarSobolev.PublishedNegativePlanarGroundGap, OAI.ContinuumCoulomb.PlanarSobolev.Sobolev, OAI.ContinuumCoulomb.PlanarSobolev.form