OAI/Geometry/TamingCompatibility/Elliptic/DerivativeIndex.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TamingCompatibility.ManifoldLocalization.DerivativeIndex line 17
2. abbrev OAI.TamingCompatibility.ManifoldLocalization.ChartH1 line 18
3. def OAI.TamingCompatibility.ManifoldLocalization.jetComponent line 20
4. def OAI.TamingCompatibility.ManifoldLocalization.localizeH1 line 27
5. lemma OAI.TamingCompatibility.ManifoldLocalization.localizeH1_apply line 37
6. lemma OAI.TamingCompatibility.ManifoldLocalization.localizeH1_none line 41
7. def OAI.TamingCompatibility.ManifoldLocalization.globalH1 line 44
8. instance OAI.TamingCompatibility.ManifoldLocalization.globalH1_complete line 47
9. def OAI.TamingCompatibility.ManifoldLocalization.zeroth line 50
10. lemma OAI.TamingCompatibility.ManifoldLocalization.zeroth_mem_globalL2 line 53
11. def OAI.TamingCompatibility.ManifoldLocalization.h1ToL2 line 61
12. def OAI.TamingCompatibility.ManifoldLocalization.jetDistribution line 64
13. lemma OAI.TamingCompatibility.ManifoldLocalization.jetDistribution_localize line 70
14. lemma OAI.TamingCompatibility.ManifoldLocalization.derivative_relation line 78
15. lemma OAI.TamingCompatibility.ManifoldLocalization.h1ToL2_injective line 94