OAI/Analysis/LiebThirring/NegativeResolvent.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLiebThirring.OperatorProof.HasBoundedResolventAt line 14

   Source documentation

   Standard bounded-resolvent condition for a partially defined operator: R is a bounded everywhere-defined inverse of A-e on its full domain. The graph equivalence includes both inverse identities and domain membership.

   def HasBoundedResolventAt (A : L2C →ₗ.[ℂ] L2C) (e : ℝ) : Prop :=
   …

   Mentions: OAI.SharpLiebThirring.OperatorProof.L2C

2. lemma OAI.SharpLiebThirring.OperatorProof.hasBoundedResolventAt_not_eigenvalue line 18
3. lemma OAI.SharpLiebThirring.OperatorProof.energy_operator_graph line 26
4. lemma OAI.SharpLiebThirring.OperatorProof.energyFormMap_bijective_resolvent line 45
5. lemma OAI.SharpLiebThirring.OperatorProof.energyFormMap_alternative line 61
6. theorem OAI.SharpLiebThirring.OperatorProof.negative_resolvent_or_eigenvalue line 72

   Source documentation

   Below zero there is no continuous or residual spectrum: each real negative energy is an actual eigenvalue, or has a bounded inverse on the full L² space.

   theorem negative_resolvent_or_eigenvalue {γ : ℝ} {W : ℝ → ℝ} (hγ : 1/2 < γ)
       (hW : Admissible γ W) (d : PotentialData W) {e : ℝ} (he : e < 0) :
       HasBoundedResolventAt (operator d) e ∨
         ∃ f : L2C, f ≠ 0 ∧ IsOperatorEigenfunction (operator d) e f := by
   …

   Mentions: OAI.SharpLiebThirring.Admissible, OAI.SharpLiebThirring.OperatorProof.PotentialData, OAI.SharpLiebThirring.OperatorProof.HasBoundedResolventAt, OAI.SharpLiebThirring.OperatorProof.operator, OAI.SharpLiebThirring.OperatorProof.L2C, OAI.SharpLiebThirring.OperatorProof.IsOperatorEigenfunction