OAI/Geometry/EinsteinFour/FrameRotation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Complete each unit direction to its quaternionic orthonormal frame. This relates spherical fiber averages to actual orthonormal frames.

  1. def OAI.PositiveEinsteinFour.Geometry.directionFrameMatrix line 16
  2. theorem OAI.PositiveEinsteinFour.Geometry.directionFrameMatrix_zero line 22
  3. theorem OAI.PositiveEinsteinFour.Geometry.directionFrameMatrix_succ line 26
  4. theorem OAI.PositiveEinsteinFour.Geometry.directionFrameMatrix_orthogonal line 32
  5. def OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.turn line 47
  6. theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.turn_first line 60
  7. def OAI.PositiveEinsteinFour.Geometry.frameTurn line 68