OAI/Geometry/SurfaceImmersion/Correction/AtlasPolynomialNonlinearProfiles.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform nonlinear error bounds from the global norms used by the iteration.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlas_polynomial_nonlinear_profiles line 20