OAI/Geometry/TamingCompatibility/DifferentialForms/Bessel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.RellichWeight.bessel line 12
2. lemma OAI.TamingCompatibility.RellichWeight.bessel_decay line 19
3. def OAI.TamingCompatibility.LocalRellich.realize line 46
4. theorem OAI.TamingCompatibility.LocalRellich.realize_compact line 50
5. def OAI.TamingCompatibility.LocalRestriction.restore line 81
6. lemma OAI.TamingCompatibility.LocalRestriction.restore_restrict line 85
7. lemma OAI.TamingCompatibility.HilbertSobolev.liftOperator_exists line 116
8. def OAI.TamingCompatibility.HilbertSobolev.liftOperator line 123
9. lemma OAI.TamingCompatibility.HilbertSobolev.toDistribution_liftOperator line 149
10. def OAI.TamingCompatibility.HilbertSobolev.derivative line 158
11. lemma OAI.TamingCompatibility.HilbertSobolev.toDistribution_derivative line 161