OAI/Geometry/TamingCompatibility/Elliptic/RealSobolevLift.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.HilbertSobolev.realSobolevLift line 19
2. lemma OAI.TamingCompatibility.HilbertSobolev.realSobolevLift_spec line 27
3. def OAI.TamingCompatibility.HilbertSobolev.realBoundedLift line 34
4. lemma OAI.TamingCompatibility.HilbertSobolev.realBoundedLift_spec line 40
5. lemma OAI.TamingCompatibility.HilbertSobolev.schwartz_bessel_surjective line 60
6. lemma OAI.TamingCompatibility.HilbertSobolev.schwartzLp_dense line 76
7. lemma OAI.TamingCompatibility.HilbertSobolev.schwartzToH_coe line 81
8. lemma OAI.TamingCompatibility.HilbertSobolev.schwartzToH_dense line 86
9. lemma OAI.TamingCompatibility.HilbertSobolev.sobolevToBounded_lipschitz_bound line 90
10. def OAI.TamingCompatibility.HilbertSobolev.sobolevEval line 127
11. lemma OAI.TamingCompatibility.HilbertSobolev.sobolevEval_continuous line 131