OAI/Geometry/TamingCompatibility/Hodge/HodgeGlobalKernelForms.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingFiberForm line 21
2. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.residualFiberForm line 26
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingFiberForm_smooth line 32
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.residualFiberForm_smooth line 40
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingFiberForm_encode line 49
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.residualFiberForm_encode line 70
7. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingKernelForm line 89
8. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.residualKernelForm line 92
9. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingKernelForm_smooth line 96
10. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.residualKernelForm_smooth line 108
11. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingKernelForm_encode line 121
12. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.residualKernelForm_encode line 134
13. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.framePairing line 163
14. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.framePairing_apply line 169
15. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.framePairing_continuous line 199
16. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.framePairing_bound line 211
17. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingKernelForm_pairing line 219
18. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.residualKernelForm_pairing line 230