OAI/Geometry/TamingCompatibility/Elliptic/PrincipalDerivativeError.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.HilbertSobolev.distribution_derivatives_commute line 20
2. lemma OAI.TamingCompatibility.HilbertSobolev.helmholtz_derivative line 31
3. def OAI.TamingCompatibility.HilbertSobolev.principalDerivativeError line 43
4. lemma OAI.TamingCompatibility.HilbertSobolev.perturbedHelmholtz_derivative line 49
5. lemma OAI.TamingCompatibility.HilbertSobolev.principalDerivativeError_memSobolev line 64
6. theorem OAI.TamingCompatibility.HilbertSobolev.principal_H1_bootstrap line 76
7. theorem OAI.TamingCompatibility.HilbertSobolev.matrix_H1_bootstrap line 109