OAI/Geometry/SurfaceImmersion/Correction/PolynomialPhaseChartInverse.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Polynomial inverse-chart jets from forward jets and the actual Jacobian lower bound. The exponent is fixed before the chart and numerical bounds.

  1. lemma OAI.ClosedSurfaceR4.PhaseGeometry.inverse_chart_derivative_eq_field line 14
  2. theorem OAI.ClosedSurfaceR4.PhaseGeometry.polynomial_inverse_chart_bound line 28