OAI/Analysis/LiebThirring/Multiplication.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SharpLiebThirring.OperatorProof.PotentialData line 11
2. def OAI.SharpLiebThirring.OperatorProof.potentialData line 22
3. lemma OAI.SharpLiebThirring.OperatorProof.memLp_integral_norm_sq line 27
4. lemma OAI.SharpLiebThirring.OperatorProof.potential_quadratic_bound line 32
5. def OAI.SharpLiebThirring.OperatorProof.weightedVal line 59
6. lemma OAI.SharpLiebThirring.OperatorProof.weightedVal_norm_sq line 62
7. lemma OAI.SharpLiebThirring.OperatorProof.weightedVal_memLp line 67
8. def OAI.SharpLiebThirring.OperatorProof.weightedLM line 77
9. lemma OAI.SharpLiebThirring.OperatorProof.weightedLM_norm_sq line 104
10. lemma OAI.SharpLiebThirring.OperatorProof.h1_norm_sq line 113
11. lemma OAI.SharpLiebThirring.OperatorProof.weightedLM_bound line 116
12. def OAI.SharpLiebThirring.OperatorProof.weightedL line 123