DiscreteSpectrum.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.SharpLiebThirring.OperatorProof.finite_eigenvalues_below line 13
Source documentation
Negative eigenvalues at or below a threshold form a finite set whenever one positive spectral moment is finite. No enumeration is presupposed.
```
lemma finite_eigenvalues_below {γ : ℝ} (hγ : 0 < γ) {A : L2C →ₗ.[ℂ] L2C}
    (hA : IsSelfAdjoint A) (hfin : eigenvalueSum γ A hA ≠ ∞)
    {a : ℝ} (ha : 0 < a) :
    {e : ℝ | e ≤ -a ∧ ∃ f : L2C, f ≠ 0 ∧ IsOperatorEigenfunction A e f}.Finite := by
…
```
Mentions: OAI.SharpLiebThirring.OperatorProof.L2C, OAI.SharpLiebThirring.OperatorProof.eigenvalueSum, OAI.SharpLiebThirring.OperatorProof.IsOperatorEigenfunction
lemma OAI.SharpLiebThirring.OperatorProof.negative_eigenvalue_isolated line 35
Source documentation
Every negative eigenvalue is isolated from all other negative eigenvalues.
```
lemma negative_eigenvalue_isolated {γ : ℝ} (hγ : 0 < γ) {A : L2C →ₗ.[ℂ] L2C}
    (hA : IsSelfAdjoint A) (hfin : eigenvalueSum γ A hA ≠ ∞) {e : ℝ} (he : e < 0) :
    ∃ ε : ℝ, 0 < ε ∧ ∀ t : ℝ, |t-e| < ε →
      (∃ f : L2C, f ≠ 0 ∧ IsOperatorEigenfunction A t f) → t = e := by
…
```
Mentions: OAI.SharpLiebThirring.OperatorProof.L2C, OAI.SharpLiebThirring.OperatorProof.eigenvalueSum, OAI.SharpLiebThirring.OperatorProof.IsOperatorEigenfunction

theorem OAI.SharpLiebThirring.OperatorProof.schrodinger_negative_spectrum line 59

Source documentation

The negative part of the operator has only isolated finite-multiplicity eigenvalues, with zero as its only possible finite accumulation point. The first clause excludes continuous/residual spectrum.

theorem schrodinger_negative_spectrum {γ : ℝ} (hγ₀ : 1/2 < γ) (hγ₁ : γ < 3/2)
    {W : ℝ → ℝ} (hW : Admissible γ W) :
    (∀ e : ℝ, e < 0 →
      (¬ HasBoundedResolventAt (schrodingerOperator hγ₀ hW) e ↔
        ∃ f : L2C, f ≠ 0 ∧ IsOperatorEigenfunction (schrodingerOperator hγ₀ hW) e f)) ∧
    (∀ e : NegativeEnergy, FiniteDimensional ℂ (eigenSpace (schrodingerOperator hγ₀ hW) e.1)) ∧
    (∀ a : ℝ, 0 < a →
      {e : ℝ | e ≤ -a ∧ ∃ f : L2C, f ≠ 0 ∧
        IsOperatorEigenfunction (schrodingerOperator hγ₀ hW) e f}.Finite) ∧
    (∀ e : ℝ, e < 0 → ∃ ε : ℝ, 0 < ε ∧ ∀ t : ℝ, |t-e| < ε →
      (∃ f : L2C, f ≠ 0 ∧ IsOperatorEigenfunction (schrodingerOperator hγ₀ hW) t f) → t = e) := by
…

Mentions: OAI.SharpLiebThirring.Admissible, OAI.SharpLiebThirring.OperatorProof.HasBoundedResolventAt, OAI.SharpLiebThirring.OperatorProof.schrodingerOperator, OAI.SharpLiebThirring.OperatorProof.L2C, OAI.SharpLiebThirring.OperatorProof.IsOperatorEigenfunction, OAI.SharpLiebThirring.OperatorProof.NegativeEnergy, OAI.SharpLiebThirring.OperatorProof.eigenSpace