OAI/Geometry/TamingCompatibility/Elliptic/MatrixH1Smooth.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TamingCompatibility.HilbertSobolev.matrix_H1_smooth line 17
2. lemma OAI.TamingCompatibility.HilbertSobolev.cutoff_product_eq line 44
3. lemma OAI.TamingCompatibility.HilbertSobolev.cutoff_derivative_product_zero line 51
4. lemma OAI.TamingCompatibility.HilbertSobolev.cutoff_second_product_zero line 61
5. lemma OAI.TamingCompatibility.HilbertSobolev.cutoff_mul_cutoff line 74
6. lemma OAI.TamingCompatibility.HilbertSobolev.cutoff_mul_derivative line 80
7. lemma OAI.TamingCompatibility.HilbertSobolev.cutoff_mul_second line 89
8. lemma OAI.TamingCompatibility.HilbertSobolev.cutoff_secondCommutator_zero line 98
9. lemma OAI.TamingCompatibility.HilbertSobolev.localizationError_cutoff_zero line 110
10. lemma OAI.TamingCompatibility.HilbertSobolev.perturbedHelmholtz_locality line 119
11. lemma OAI.TamingCompatibility.HilbertSobolev.matrixLowerOrder_locality line 128
12. theorem OAI.TamingCompatibility.HilbertSobolev.matrix_cutoff_succ_regular line 148