OAI/Geometry/TamingCompatibility/Hodge/HodgePatchLocalInitial.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingCoordinate_initial_local line 22
2. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.partitionLeading_initial_local line 73
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.partitionLeading_initial_form line 103
4. lemma OAI.TamingCompatibility.GeometricHilbert.CoordinateOperator.sum_pullCoefficient_inverse line 125
5. lemma OAI.TamingCompatibility.GeometricHilbert.CoordinateOperator.firstOrder_inverse_pull line 139
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.pulled_firstOrder line 159
7. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.pulled_energy line 174