OAI/Geometry/TamingCompatibility/Hodge/HodgeParametrixInitial.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalDensity_continuous line 26
2. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalDensity_zero line 30
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingCoordinate_initial line 34
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalMap_slice_injective line 96
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalMap_slice_image line 104
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingPatch_change line 124
7. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingPatch_initial line 176