OAI/Geometry/SurfaceImmersion/Correction/PolynomialCubicRemainder.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A fixed atlas constant gives polynomial dependence of the actual cubic metric remainder on the free and forced displacement budgets.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.global_cubic_remainder_uniform_budget line 30