OAI/Geometry/SurfaceImmersion/Atlas/TensorFiberCoordinates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The three independent coordinates of a symmetric surface tensor, with an explicit continuous linear reconstruction into the full tensor fiber.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.planeFirst line 21
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.planeSecond line 24
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.fiberToThree line 27
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.fiberToThree_apply line 34
  5. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.fiberFromThree line 38
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.fiberFromThree_apply line 44
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.fiberToThree_fromThree line 49
  8. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.plane_basis_expansion line 57
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.fiberFromThree_toThree line 64
  10. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.fiberFromThree_symmetric line 79