OAI/Geometry/TamingCompatibility/Elliptic/PrincipalTransport.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.HilbertSobolev.directionalPrincipal_linear line 24
2. lemma OAI.TamingCompatibility.HilbertSobolev.directionalPrincipal_zoom line 33
3. lemma OAI.TamingCompatibility.HilbertSobolev.matrixLowerOrder_linear line 42
4. lemma OAI.TamingCompatibility.HilbertSobolev.matrixLowerOrder_zoom line 54
5. lemma OAI.TamingCompatibility.HilbertSobolev.inner_linear_basis line 65
6. lemma OAI.TamingCompatibility.HilbertSobolev.sum_gram_transform line 71
7. lemma OAI.TamingCompatibility.HilbertSobolev.gram_covariance line 89
8. lemma OAI.TamingCompatibility.HilbertSobolev.localized_coefficient_congr line 115
9. lemma OAI.TamingCompatibility.HilbertSobolev.local_frozen_product line 128
10. lemma OAI.TamingCompatibility.HilbertSobolev.local_frozen_helmholtz line 153