OAI/Geometry/TamingCompatibility/Elliptic/CriticalH1Linear.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.HilbertSobolev.schwartz_derivative_L2_H1 line 20
2. lemma OAI.TamingCompatibility.HilbertSobolev.critical_norm_H1 line 27
3. def OAI.TamingCompatibility.HilbertSobolev.linearH line 78
4. lemma OAI.TamingCompatibility.HilbertSobolev.linearH_spec line 81
5. lemma OAI.TamingCompatibility.HilbertSobolev.linearH_schwartz line 85
6. lemma OAI.TamingCompatibility.HilbertSobolev.linear_schwartz_H_bound line 94
7. lemma OAI.TamingCompatibility.HilbertSobolev.critical_linear_H1 line 121
8. theorem OAI.TamingCompatibility.HilbertSobolev.normalized_scalar_uniform_regular line 150