SpectralMain.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SharpLiebThirring.OperatorProof.schrodingerOperator line 12
Source documentation
The unbounded self-adjoint operator associated with exactly the H¹ form.
```
def schrodingerOperator {γ : ℝ} (hγ : 1/2 < γ) {W : ℝ → ℝ} (hW : Admissible γ W) :
    L2C →ₗ.[ℂ] L2C := operator (potentialData hγ hW)
```
Mentions: OAI.SharpLiebThirring.Admissible, OAI.SharpLiebThirring.OperatorProof.L2C, OAI.SharpLiebThirring.OperatorProof.operator, OAI.SharpLiebThirring.OperatorProof.potentialData
lemma OAI.SharpLiebThirring.OperatorProof.schrodingerOperator_selfAdjoint line 15
lemma OAI.SharpLiebThirring.OperatorProof.schrodingerOperator_associated line 19
lemma OAI.SharpLiebThirring.OperatorProof.eigenvalueSum_eq_negativeMoment line 23
def OAI.SharpLiebThirring.OperatorProof.spectralMoment line 40
Source documentation
The trace: sum of every negative eigenvalue of the form operator, counted once for each member of a full eigenspace basis.
```
def spectralMoment {γ : ℝ} (hγ : 1/2 < γ) {W : ℝ → ℝ} (hW : Admissible γ W) : ℝ≥0∞ :=
…
```
Mentions: OAI.SharpLiebThirring.Admissible
lemma OAI.SharpLiebThirring.OperatorProof.spectralMoment_eq line 43
def OAI.SharpLiebThirring.OperatorProof.spectralOptimalConstant line 48
def OAI.SharpLiebThirring.OperatorProof.spectralOneStateConstant line 52
lemma OAI.SharpLiebThirring.OperatorProof.spectralOptimalConstant_eq line 56
lemma OAI.SharpLiebThirring.OperatorProof.spectralOneStateConstant_eq line 65
theorem OAI.SharpLiebThirring.OperatorProof.sharp_bound_for_associated_operator line 76
Source documentation
The sharp bound for the infinite eigenvalue sum of any self-adjoint operator associated with the form, together with finite multiplicities.
```
theorem sharp_bound_for_associated_operator {γ : ℝ} (hγ₀ : 1/2 < γ) (hγ₁ : γ < 3/2)
    {W : ℝ → ℝ} (hW : Admissible γ W) {A : L2C →ₗ.[ℂ] L2C}
    (hA : IsSelfAdjoint A) (ha : IsAssociated W A) :
    eigenvalueSum γ A hA ≤ ENNReal.ofReal (sharpConstant γ)*potentialMass γ W ∧
      ∀ e : NegativeEnergy, FiniteDimensional ℂ (eigenSpace A e.1) := by
…
```
Mentions: OAI.SharpLiebThirring.Admissible, OAI.SharpLiebThirring.OperatorProof.L2C, OAI.SharpLiebThirring.OperatorProof.IsAssociated, OAI.SharpLiebThirring.OperatorProof.eigenvalueSum, OAI.SharpLiebThirring.sharpConstant, OAI.SharpLiebThirring.potentialMass, OAI.SharpLiebThirring.OperatorProof.NegativeEnergy, OAI.SharpLiebThirring.OperatorProof.eigenSpace
theorem OAI.SharpLiebThirring.OperatorProof.sharp_lieb_thirring_spectral line 90
Source documentation
All main conclusions in the actual-operator formulation. Its operator is constructed unconditionally; no existence, trace equivalence, spectral estimate, or finiteness assumption is used as an input.
```
theorem sharp_lieb_thirring_spectral {γ : ℝ} (hγ₀ : 1/2 < γ) (hγ₁ : γ < 3/2) :
    (∀ (W : ℝ → ℝ) (hW : Admissible γ W),
      spectralMoment hγ₀ hW ≤ ENNReal.ofReal (sharpConstant γ)*potentialMass γ W) ∧
    spectralOptimalConstant hγ₀ = ENNReal.ofReal (sharpConstant γ) ∧
    spectralOneStateConstant hγ₀ = ENNReal.ofReal (sharpConstant γ) ∧
    ∃ hW : Admissible γ (equalityPotential γ),
      0 < potentialMass γ (equalityPotential γ) ∧
      spectralMoment hγ₀ hW = ENNReal.ofReal (sharpConstant γ)*potentialMass γ (equalityPotential γ) := by
…
```
Mentions: OAI.SharpLiebThirring.Admissible, OAI.SharpLiebThirring.OperatorProof.spectralMoment, OAI.SharpLiebThirring.sharpConstant, OAI.SharpLiebThirring.potentialMass, OAI.SharpLiebThirring.OperatorProof.spectralOptimalConstant, OAI.SharpLiebThirring.OperatorProof.spectralOneStateConstant, OAI.SharpLiebThirring.equalityPotential