OAI/Geometry/TamingCompatibility/Functional/NormalSymbol.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.LocalMatrixOperator.normalSymbol line 18
2. lemma OAI.TamingCompatibility.LocalMatrixOperator.normalSymbol_inner line 22
3. lemma OAI.TamingCompatibility.LocalMatrixOperator.normalSymbol_polarized line 28
4. lemma OAI.TamingCompatibility.LocalMatrixOperator.normalSymbol_adjoint line 35
5. lemma OAI.TamingCompatibility.LocalMatrixOperator.normalSymbol_adjoint_polarized line 46
6. lemma OAI.TamingCompatibility.LocalMatrixOperator.normalSymbol_geometric line 68
7. def OAI.TamingCompatibility.LocalMatrixOperator.frameTest line 97
8. lemma OAI.TamingCompatibility.LocalMatrixOperator.frameTest_zero line 100
9. lemma OAI.TamingCompatibility.LocalMatrixOperator.frameTest_tsupport line 104
10. lemma OAI.TamingCompatibility.LocalMatrixOperator.frameTest_smooth line 111
11. lemma OAI.TamingCompatibility.LocalMatrixOperator.frameTest_compact line 127
12. lemma OAI.TamingCompatibility.ManifoldForms.pullback_antiInvariantPart line 137
13. lemma OAI.TamingCompatibility.ManifoldForms.pullback_lift_antiInvariantPart line 151