OAI/Geometry/SurfaceImmersion/Atlas/PhaseChartBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The local phase-coordinate polynomial operator keeps the original fixed scale exponent and derivative loss.

  1. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.phaseChartPolynomialOperator_bounds line 16