OAI/Geometry/TamingCompatibility/Hodge/HodgeAtlasPatches.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.normalCutoff line 25
2. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.normalCompact line 28
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.normalCompact_compact line 31
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.normalCutoff_tsupport line 34
5. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.normalChart line 40
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.normalCompact_source line 44
7. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.physicalCompact line 46
8. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.physicalCompact_compact line 48
9. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.physicalCompact_domain line 51
10. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.coordinatePartition_centerSupport line 63
11. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.partition_patch_support line 71
12. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.partitionLeading line 77
13. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.partitionResidual line 82
14. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.partitionLeading_smooth line 88
15. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.partitionResidual_smooth line 99
16. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.partitionLeading_tsupport line 109
17. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.partitionResidual_tsupport line 117
18. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.partitionLeading_gaussian line 124
19. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.partitionResidual_gaussian line 137
20. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.physicalCompact_actual line 168
21. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.density_actual line 174
22. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.partitionLeading_density line 183
23. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.partitionLeading_initial line 194