OAI/Analysis/LiebThirring/LocalCompactness.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLiebThirring.OperatorProof.continuousRep line 11
2. lemma OAI.SharpLiebThirring.OperatorProof.continuousRep_continuous line 12
3. lemma OAI.SharpLiebThirring.OperatorProof.continuousRep_ae line 14
4. lemma OAI.SharpLiebThirring.OperatorProof.valL_norm_le line 16
5. lemma OAI.SharpLiebThirring.OperatorProof.gradL_norm_le line 20
6. lemma OAI.SharpLiebThirring.OperatorProof.continuousRep_norm line 24
7. lemma OAI.SharpLiebThirring.OperatorProof.continuousRep_holder line 29
8. abbrev OAI.SharpLiebThirring.OperatorProof.Interval line 37
9. def OAI.SharpLiebThirring.OperatorProof.localRep line 39
10. lemma OAI.SharpLiebThirring.OperatorProof.localRep_compact line 43