OAI/Geometry/TamingCompatibility/DifferentialForms/Helmholtz.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.EuclideanGreen.multiplier_add line 14
2. lemma OAI.TamingCompatibility.EuclideanGreen.bessel_two line 21
3. def OAI.TamingCompatibility.EuclideanGreen.helmholtz line 31
4. lemma OAI.TamingCompatibility.EuclideanGreen.bessel_two_eq_helmholtz line 34
5. theorem OAI.TamingCompatibility.EuclideanGreen.helmholtz_green line 41
6. theorem OAI.TamingCompatibility.EuclideanGreen.green_helmholtz line 46
7. theorem OAI.TamingCompatibility.EuclideanGreen.memSobolev_helmholtz_iff line 53
8. theorem OAI.TamingCompatibility.EuclideanGreen.green_regularity line 57
9. abbrev OAI.TamingCompatibility.HilbertSobolev.basisIndex line 72
10. def OAI.TamingCompatibility.HilbertSobolev.recover line 74
11. lemma OAI.TamingCompatibility.HilbertSobolev.recover_distribution line 78
12. lemma OAI.TamingCompatibility.HilbertSobolev.recover_gradient line 87
13. lemma OAI.TamingCompatibility.HilbertSobolev.recover_norm_le line 104
14. theorem OAI.TamingCompatibility.HilbertSobolev.norm_le_gradient line 115