OAI/Analysis/LiebThirring/OneState.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLiebThirring.OperatorProof.oneEigenvalueMoment line 13

   Source documentation

   Retain the largest weight of a single negative eigenvalue of the actual operator. The supremum of the empty family is zero.

   def oneEigenvalueMoment (γ : ℝ) (A : L2C →ₗ.[ℂ] L2C) : ℝ≥0∞ :=
   …

   Mentions: OAI.SharpLiebThirring.OperatorProof.L2C

2. lemma OAI.SharpLiebThirring.OperatorProof.oneStateMoment_eq_oneEigenvalueMoment line 17