Model.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

The form domain is H¹(R;C), represented by an L² function together with its L² weak derivative. Null-set changes do not affect any definition below. negativeMoment is the extended nonnegative sum over negative eigenvalues, counting multiplicities: equivalently the supremum over all finite orthonormal families of weak eigenfunctions of the form. This does not assume in advance finiteness of the moment or a finite number of eigenvalues.

structure OAI.SharpLiebThirring.H1 line 23
Also declared: ComparatorChallenges/LiebThirring.lean:23 (same declaration text).
def OAI.SharpLiebThirring.l2Pairing line 31
Also declared: ComparatorChallenges/LiebThirring.lean:31 (same declaration text).
def OAI.SharpLiebThirring.schrodingerForm line 34
Source documentation
The polarized form of -d²/dx² - W, on exactly H¹.
Also declared: ComparatorChallenges/LiebThirring.lean:34 (same declaration text).
```
def schrodingerForm (W : ℝ → ℝ) (u v : H1) : ℂ :=
…
```
Mentions: OAI.SharpLiebThirring.H1
def OAI.SharpLiebThirring.IsNegativeEigenfunction line 39
Source documentation
Weak eigenfunction at the negative energy -k².
Also declared: ComparatorChallenges/LiebThirring.lean:39 (same declaration text).
```
def IsNegativeEigenfunction (W : ℝ → ℝ) (k : ℝ) (u : H1) : Prop :=
…
```
Mentions: OAI.SharpLiebThirring.H1
def OAI.SharpLiebThirring.IsOrthonormalFamily line 42
Also declared: ComparatorChallenges/LiebThirring.lean:42 (same declaration text).
def OAI.SharpLiebThirring.negativeMoment line 46
Source documentation
An unlimited finite-family-size supremum, in ℝ≥0∞, includes the entire sum.
Also declared: ComparatorChallenges/LiebThirring.lean:46 (same declaration text).
```
def negativeMoment (γ : ℝ) (W : ℝ → ℝ) : ℝ≥0∞ :=
…
```
def OAI.SharpLiebThirring.oneStateMoment line 52
Source documentation
The moment retaining at most one negative eigenvalue.
Also declared: ComparatorChallenges/LiebThirring.lean:52 (same declaration text).
```
def oneStateMoment (γ : ℝ) (W : ℝ → ℝ) : ℝ≥0∞ :=
…
```
def OAI.SharpLiebThirring.Admissible line 56
Also declared: ComparatorChallenges/LiebThirring.lean:56 (same declaration text).
def OAI.SharpLiebThirring.potentialMass line 59
Also declared: ComparatorChallenges/LiebThirring.lean:59 (same declaration text).
def OAI.SharpLiebThirring.semiclassicalConstant line 62
Also declared: ComparatorChallenges/LiebThirring.lean:62 (same declaration text).
def OAI.SharpLiebThirring.sharpConstant line 65
Also declared: ComparatorChallenges/LiebThirring.lean:65 (same declaration text).
def OAI.SharpLiebThirring.optimalConstant line 68
Also declared: ComparatorChallenges/LiebThirring.lean:68 (same declaration text).
def OAI.SharpLiebThirring.oneStateConstant line 72
Also declared: ComparatorChallenges/LiebThirring.lean:72 (same declaration text).
def OAI.SharpLiebThirring.equalityPotential line 76
Also declared: ComparatorChallenges/LiebThirring.lean:76 (same declaration text).
def OAI.SharpLiebThirring.MainClaim line 81
Source documentation
The full spectral bound, optimal constants, and attainment at the explicit potential.
Also declared: ComparatorChallenges/LiebThirring.lean:81 (same declaration text).
```
def MainClaim : Prop :=
…
```