OAI/Analysis/LiebThirring/EigenvalueSum.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLiebThirring.OperatorProof.finite_family_le_moment line 13
2. lemma OAI.SharpLiebThirring.OperatorProof.eigenvalueSum_le_moment line 27
3. lemma OAI.SharpLiebThirring.OperatorProof.eigenBasis_finite line 40
4. lemma OAI.SharpLiebThirring.OperatorProof.eigenSpace_finiteDimensional line 58
5. lemma OAI.SharpLiebThirring.OperatorProof.finite_family_le_sum line 66
6. lemma OAI.SharpLiebThirring.OperatorProof.eigenvalueMoment_eq_sum line 104