OAI/Geometry/SurfaceImmersion/Atlas/CoordinateTaylorIdentity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact Taylor identity for the metric plus its finite polynomial perturbation, in the coordinates of the forced-mode construction.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinatePolynomialValue line 13
  2. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinateMetricMap line 17
  3. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinateFullQuadratic line 21
  4. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinateTaylorRemainder line 25
  5. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinate_metric_taylor_identity line 30