OAI/Geometry/SurfaceImmersion/Correction/AtlasPolynomialOverlapCancellation.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_on line 33