OAI/Geometry/TamingCompatibility/Hodge/HodgeParametrixWeakEquation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.actual_cutoff_weak_deriv line 27
2. structure OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData line 73
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.parametrixData_nonempty line 95
4. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.parametrixData line 108
5. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.source line 116
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.source_open line 119
7. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.mem_source line 122
8. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.source_subset line 125
9. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.centers_actual line 127
10. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.actual line 134
11. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.source_image_subset line 139
12. theorem OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.finite_parametrix_partition line 146
13. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.parametrix_coordinateSupport line 165