OAI/Geometry/SurfaceImmersion/Correction/AtlasSupportedPolynomialVariation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The variation of a globally defined polynomial in a chart-supported direction is the restoration of that chart's actual local linearization.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.restore_chart_read_on_weight line 32
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.supported_polynomial_variation line 47