OAI/Geometry/TamingCompatibility/DifferentialForms/SymbolMap.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.HodgeNormalSymbol.normalSymbol_add_covector line 11
2. lemma OAI.TamingCompatibility.HodgeNormalSymbol.normalSymbol_smul_covector line 18
3. def OAI.TamingCompatibility.HodgeNormalSymbol.symbolMap line 25
4. lemma OAI.TamingCompatibility.HodgeNormalSymbol.symbolMap_apply line 31
5. def OAI.TamingCompatibility.GeometricHilbert.CoordinateOperator.firstOrder line 39
6. def OAI.TamingCompatibility.GeometricHilbert.CoordinateOperator.pullCoefficient line 43
7. lemma OAI.TamingCompatibility.GeometricHilbert.CoordinateOperator.basis_expansion line 46
8. lemma OAI.TamingCompatibility.GeometricHilbert.CoordinateOperator.firstOrder_pull line 50
9. lemma OAI.TamingCompatibility.GeometricHilbert.CoordinateOperator.pullCoefficient_symbol line 64
10. lemma OAI.TamingCompatibility.GeometricHilbert.CoordinateOperator.pullCoefficient_polarized line 79
11. lemma OAI.TamingCompatibility.GeometricHilbert.CoordinateOperator.pullCoefficient_contDiff line 89
12. lemma OAI.TamingCompatibility.GeometricHilbert.CoordinateOperator.intrinsic_firstOrder_pull line 96
13. abbrev OAI.TamingCompatibility.GeometricHilbert.OrthogonalJets.End line 124
14. def OAI.TamingCompatibility.GeometricHilbert.OrthogonalJets.gauge line 126
15. lemma OAI.TamingCompatibility.GeometricHilbert.OrthogonalJets.gauge_zero line 129
16. lemma OAI.TamingCompatibility.GeometricHilbert.OrthogonalJets.gauge_contDiff line 132
17. lemma OAI.TamingCompatibility.GeometricHilbert.OrthogonalJets.gauge_hasFDerivAt_zero line 138
18. lemma OAI.TamingCompatibility.GeometricHilbert.OrthogonalJets.gauge_unitary line 144
19. lemma OAI.TamingCompatibility.GeometricHilbert.OrthogonalJets.gauge_inner line 150
20. lemma OAI.TamingCompatibility.GeometricHilbert.OrthogonalJets.gauge_norm line 155