OAI/Geometry/SurfaceImmersion/Correction/TensorAtlasFiniteMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite nonlinear mean adjustment for the actual global atlas operator. All local trial radii and the smallness threshold precede the local maps.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensor_atlas_finite_mean line 31