OAI/Analysis/LiebThirring/PotentialCompactness.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLiebThirring.OperatorProof.small_bounded_plus_L1 line 11
2. lemma OAI.SharpLiebThirring.OperatorProof.integrable_tail_small line 38
3. lemma OAI.SharpLiebThirring.OperatorProof.h1Graph_ae_sq_bound line 58
4. lemma OAI.SharpLiebThirring.OperatorProof.tail_weighted_norm_sq line 63
5. lemma OAI.SharpLiebThirring.OperatorProof.weightedL_compact line 102