OAI/Geometry/SurfaceImmersion/Correction/ChartedAtlasMeanIdentity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual quadratic zero-phase terms of the charted free oscillations restore to the input global tensor plus the global nonlinear mean.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.charted_atlas_mean_identity line 32