OAI/Geometry/SurfaceImmersion/Correction/UniformSmoothingInputProfiles.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The fixed low input norm supplies all profiles of the smoothed map and tensor, before the true input or either scale is chosen.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.uniform_smoothing_input_profiles line 36