OAI/Analysis/LiebThirring/SpectralMoment.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLiebThirring.OperatorProof.IsOperatorEigenfunction line 11
2. def OAI.SharpLiebThirring.OperatorProof.eigenvalueMoment line 16

   Source documentation

   The entire negative eigenvalue moment, with multiplicity, of an actual partially defined operator. Energies here are the eigenvalues e, not scales.

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

   Mentions: OAI.SharpLiebThirring.OperatorProof.L2C

3. lemma OAI.SharpLiebThirring.OperatorProof.energy_weight line 21
4. lemma OAI.SharpLiebThirring.OperatorProof.negativeMoment_eq_eigenvalueMoment line 26