OAI/Geometry/SurfaceImmersion/Correction/AtlasPolynomialMetric.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The actual globally restored polynomial perturbation of the metric, with its exact first, second and higher-order variation decomposition.

  1. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinate_polynomial_taylor_identity line 15
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlasPolynomialValue line 50
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlasPolynomialMetric line 54
  4. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlasPolynomialVariation line 58
  5. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlasPolynomialQuadratic line 63
  6. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlasPolynomialRemainder line 68
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlasPolynomialValue_symmetric line 74
  8. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlasPolynomialMetric_symmetric line 80
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlasPolynomialValue_smooth line 88
  10. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlasPolynomialMetric_smooth line 97
  11. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.jetChartMap_add line 106
  12. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlas_polynomial_taylor_identity line 116
  13. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlas_polynomial_metric_taylor_identity line 135