OAI/Geometry/Kahler/BaseChartNormalization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PinchedHartogs.BaseConstruction.iteratedFDeriv_add_mul line 20
2. lemma OAI.PinchedHartogs.BaseConstruction.baseHessian_add_mul line 30
3. lemma OAI.PinchedHartogs.BaseConstruction.psi_baseHessian_chart_eventually line 37
4. lemma OAI.PinchedHartogs.BaseConstruction.psi_baseHessian_center line 54
5. lemma OAI.PinchedHartogs.BaseConstruction.psi_baseHessian_value line 60
6. lemma OAI.PinchedHartogs.BaseConstruction.baseHessian_chart_normalize line 67
7. lemma OAI.PinchedHartogs.BaseConstruction.baseHessian_congr_derivatives line 80