OAI/Analysis/LiebThirring/WeightedCutoff.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpLiebThirring.OperatorProof.cutoff_memLp line 11
  2. def OAI.SharpLiebThirring.OperatorProof.cutoffLM line 14
  3. lemma OAI.SharpLiebThirring.OperatorProof.cutoffLM_norm line 39
  4. def OAI.SharpLiebThirring.OperatorProof.cutoffL line 47
  5. lemma OAI.SharpLiebThirring.OperatorProof.cutoffL_ae line 50
  6. def OAI.SharpLiebThirring.OperatorProof.extendedBCF line 55
  7. lemma OAI.SharpLiebThirring.OperatorProof.extendedBCF_continuous line 58
  8. lemma OAI.SharpLiebThirring.OperatorProof.weightedBCF_memLp line 62
  9. def OAI.SharpLiebThirring.OperatorProof.weightedBCF line 70
  10. lemma OAI.SharpLiebThirring.OperatorProof.weightedBCF_ae line 73
  11. lemma OAI.SharpLiebThirring.OperatorProof.weightedBCF_lipschitz line 77
  12. lemma OAI.SharpLiebThirring.OperatorProof.weightedBCF_continuous line 87
  13. lemma OAI.SharpLiebThirring.OperatorProof.weightedBCF_localRep_ae line 91
  14. lemma OAI.SharpLiebThirring.OperatorProof.localRep_isCompact line 101
  15. lemma OAI.SharpLiebThirring.OperatorProof.weightedBCF_localRep_isCompact line 106