OAI/Analysis/LiebThirring/OperatorForm.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLiebThirring.OperatorProof.weightedL_inner line 11
2. lemma OAI.SharpLiebThirring.OperatorProof.form_eq_inner line 29
3. def OAI.SharpLiebThirring.OperatorProof.shiftedFormMap line 35
4. lemma OAI.SharpLiebThirring.OperatorProof.shiftedFormMap_inner line 39
5. lemma OAI.SharpLiebThirring.OperatorProof.shiftedFormMap_coercive line 52
6. lemma OAI.SharpLiebThirring.OperatorProof.shiftedFormMap_symmetric line 65