OAI/Analysis/LiebThirring/OperatorGraph.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SharpLiebThirring.OperatorProof.L2C line 11
  2. abbrev OAI.SharpLiebThirring.OperatorProof.ProductL2 line 12
  3. abbrev OAI.SharpLiebThirring.OperatorProof.TestFunction line 13
  4. def OAI.SharpLiebThirring.OperatorProof.testLp line 15
  5. lemma OAI.SharpLiebThirring.OperatorProof.inner_star_testLp line 18
  6. def OAI.SharpLiebThirring.OperatorProof.constraint line 27
  7. lemma OAI.SharpLiebThirring.OperatorProof.constraint_eq line 32
  8. def OAI.SharpLiebThirring.OperatorProof.h1Graph line 40
  9. lemma OAI.SharpLiebThirring.OperatorProof.mem_h1Graph_iff line 42
  10. lemma OAI.SharpLiebThirring.OperatorProof.h1Graph_closed line 47
  11. abbrev OAI.SharpLiebThirring.OperatorProof.H1C line 51
  12. instance OAI.SharpLiebThirring.OperatorProof.(instance at line 52) line 52
  13. def OAI.SharpLiebThirring.OperatorProof.valL line 54
  14. def OAI.SharpLiebThirring.OperatorProof.gradL line 55
  15. def OAI.SharpLiebThirring.OperatorProof.toH1 line 57
  16. def OAI.SharpLiebThirring.OperatorProof.ofH1 line 64
  17. lemma OAI.SharpLiebThirring.OperatorProof.valL_ofH1 line 72
  18. lemma OAI.SharpLiebThirring.OperatorProof.gradL_ofH1 line 73
  19. lemma OAI.SharpLiebThirring.OperatorProof.valL_injective line 75
  20. lemma OAI.SharpLiebThirring.OperatorProof.valL_dense line 102
  21. lemma OAI.SharpLiebThirring.OperatorProof.toLp_toH1 line 116
  22. lemma OAI.SharpLiebThirring.OperatorProof.grad_toLp_toH1 line 118
  23. lemma OAI.SharpLiebThirring.OperatorProof.l2Pairing_eq_inner line 121
  24. lemma OAI.SharpLiebThirring.OperatorProof.gradPairing_eq_inner line 129