OAI/Geometry/TamingCompatibility/Elliptic/CriticalRescaleH1.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.HilbertSobolev.schwartzToH_zero line 21
2. lemma OAI.TamingCompatibility.HilbertSobolev.schwartzToH_inclusion line 24
3. lemma OAI.TamingCompatibility.HilbertSobolev.schwartz_H1_norm_le line 29
4. lemma OAI.TamingCompatibility.HilbertSobolev.schwartz_derivative_smul line 50
5. lemma OAI.TamingCompatibility.HilbertSobolev.cutoff_rescale_derivative_L2 line 63
6. theorem OAI.TamingCompatibility.HilbertSobolev.cutoff_rescale_H1 line 85
7. lemma OAI.TamingCompatibility.CriticalSobolev.opNorm_le_sum_basis line 143
8. lemma OAI.TamingCompatibility.ScalarPair.critical_sobolev_jet line 169