OAI/Geometry/SurfaceImmersion/Primitive/PeriodicAnsatzMetric.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.PeriodicExpansion.Geometry.xTangent_value line 25
  2. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.yTangent_value line 42
  3. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.finiteAnsatz_x line 56
  4. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.finiteAnsatz_y line 88