OAI/Analysis/LiebThirring/ContinuousRepresentative.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLiebThirring.OperatorProof.integral_norm_Icc_le_sqrt_length line 13
2. lemma OAI.SharpLiebThirring.OperatorProof.primitive_holder line 36
3. lemma OAI.SharpLiebThirring.OperatorProof.h1_exists_continuous_rep line 58