OAI/Geometry/NodalSets/Coefficients/ComplexChartCoefficient.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Yau.Geometry.complexPrincipal line 14
2. def OAI.Yau.Geometry.complexDrift line 17
3. theorem OAI.Yau.Geometry.complex_chart_coefficient_extensions line 22
4. theorem OAI.Yau.Geometry.extended_actual_metric_normal_jets line 50
5. theorem OAI.Yau.Geometry.parametric_taylor_family line 80