OAI/Geometry/SurfaceImmersion/Primitive/LocalPeriodicAnsatzMetric.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Identifying the finite metric polynomial with derivatives of the actual map.

  1. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.xTangent_value line 30
  2. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.yTangent_value line 47
  3. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.finiteAnsatz_x line 61
  4. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.finiteAnsatz_y line 93