OAI/Analysis/LiebThirring/Resolvent.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLiebThirring.OperatorProof.shiftedFormMap_bijective line 11
2. def OAI.SharpLiebThirring.OperatorProof.formEquiv line 15
3. def OAI.SharpLiebThirring.OperatorProof.solveL line 20
4. lemma OAI.SharpLiebThirring.OperatorProof.shifted_solve line 23
5. lemma OAI.SharpLiebThirring.OperatorProof.solve_shifted line 27
6. def OAI.SharpLiebThirring.OperatorProof.resolvent line 31
7. lemma OAI.SharpLiebThirring.OperatorProof.val_adjoint_injective line 33
8. lemma OAI.SharpLiebThirring.OperatorProof.resolvent_injective line 39
9. lemma OAI.SharpLiebThirring.OperatorProof.resolvent_symmetric line 43
10. lemma OAI.SharpLiebThirring.OperatorProof.resolvent_dense line 52
11. lemma OAI.SharpLiebThirring.OperatorProof.solve_form line 60