OAI/Analysis/LiebThirring/SobolevBound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLiebThirring.OperatorProof.integral_norm_Icc_le_L2 line 13
2. lemma OAI.SharpLiebThirring.OperatorProof.primitive_pointwise_bound line 40
3. lemma OAI.SharpLiebThirring.OperatorProof.project_L2_norm_le line 78
4. lemma OAI.SharpLiebThirring.OperatorProof.h1_ae_bound line 86
5. lemma OAI.SharpLiebThirring.OperatorProof.h1_ae_sq_bound line 117
6. lemma OAI.SharpLiebThirring.OperatorProof.L2_norm_sq_eq_integral line 124