OAI/Geometry/TamingCompatibility/Hodge/HodgeFiniteFrameResolution.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.HodgeFrame.reconstruct_basisFun line 15
2. lemma OAI.TamingCompatibility.GeometricAdjoint.pairing_two_chart line 25
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalFrame_zero line 49
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalFrame_pullback line 59
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalFrame_resolution_chart line 68
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalFrame_resolution line 104
7. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalFrame_full_resolution line 125
8. lemma OAI.TamingCompatibility.ManifoldForms.Smooth.sum line 144
9. abbrev OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.FrameSpace line 163
10. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameEncode line 165
11. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameDecode line 169
12. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameEncode_apply line 174
13. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameDecode_apply line 179
14. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameDecode_encode line 191
15. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameProjection line 196
16. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameProjection_idempotent line 201
17. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameProjection_encode line 211
18. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameEncode_section_smooth line 217
19. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameDecode_section_smooth line 224