OAI/Geometry/SurfaceImmersion/Correction/PolynomialRotationFrame.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Polynomial rotation columns from a three-coordinate quaternion. They fill a twice-winding planar frame by allowing its first column to move.

  1. abbrev OAI.ClosedSurfaceR4.FiniteOrderSmoothing.FrameTarget line 13
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.rotationFirst line 15
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.rotationSecond line 17
  4. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.polynomialRotationFrame line 19
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.polynomialRotationFrame_apply line 23
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.rotationFirst_sq line 28
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.rotationSecond_sq line 33
  8. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.rotation_columns_orthogonal line 38
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.polynomialRotationFrame_injective line 45
  10. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.polynomialRotationFrame_smooth line 71
  11. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.polynomialRotationFrame_boundary line 83