OAI/Geometry/SurfaceImmersion/Atlas/AtlasCombinedCancellation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Cancel every nonzero quadratic phase of the actual global polynomial metric using its derived local linearized solvers.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.global_polynomial_quadratic_cancellation line 32