OAI/Analysis/LiebThirring/LowestEigenvalue.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLiebThirring.OperatorProof.eigenBasis_nonempty line 11
2. lemma OAI.SharpLiebThirring.OperatorProof.oneEigenvalueMoment_eq_iSup line 22
3. lemma OAI.SharpLiebThirring.OperatorProof.exists_max_weight line 37
4. theorem OAI.SharpLiebThirring.OperatorProof.one_state_is_lowest line 56

   Source documentation

   If there is a negative eigenvalue, retaining one state means precisely the lowest negative eigenvalue, not an assumed minimizer or a finite spectral cutoff.

   theorem one_state_is_lowest {γ : ℝ} (hγ : 0 < γ) {A : L2C →ₗ.[ℂ] L2C}
       (hA : IsSelfAdjoint A) (hfin : eigenvalueSum γ A hA ≠ ∞)
       (hex : ∃ (e : ℝ) (f : L2C), e < 0 ∧ f ≠ 0 ∧ IsOperatorEigenfunction A e f) :
       ∃ (e : ℝ) (f : L2C), e < 0 ∧ inner ℂ f f = 1 ∧
         IsOperatorEigenfunction A e f ∧
         oneEigenvalueMoment γ A = (ENNReal.ofReal |e|)^γ ∧
         ∀ (t : ℝ) (g : L2C), t < 0 → g ≠ 0 → IsOperatorEigenfunction A t g → e ≤ t := by
   …

   Mentions: OAI.SharpLiebThirring.OperatorProof.L2C, OAI.SharpLiebThirring.OperatorProof.eigenvalueSum, OAI.SharpLiebThirring.OperatorProof.IsOperatorEigenfunction, OAI.SharpLiebThirring.OperatorProof.oneEigenvalueMoment