OAI/Geometry/TamingCompatibility/Hodge/HodgeParametrixFormWeak.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.weakSliceDomain line 24
2. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.weakSliceDomain_open line 28
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.cutoff_weakSliceDomain line 33
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.weakSliceDomain_normal line 38
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.weakSliceDomain_actual line 41
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.form_normal_smooth line 44
7. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.cutoff_form_weak_deriv line 51
8. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingSlice line 103
9. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingSlice_smooth line 107
10. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingSlice_normal line 115
11. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingSlice_tsupport line 129
12. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingSlice_compact line 166
13. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingSlice_domain line 173
14. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingSlice_normal_nhds line 182