OAI/Geometry/EinsteinFour/SphericalRotation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Actual coordinate-plane rotations on the unit sphere, with their ordinary derivatives. These yield the sixth-moment recurrence.

  1. def OAI.PositiveEinsteinFour.Angular.planeLinear line 14
  2. theorem OAI.PositiveEinsteinFour.Angular.planeLinear_apply line 41
  3. theorem OAI.PositiveEinsteinFour.Angular.planeLinear_norm line 45
  4. theorem OAI.PositiveEinsteinFour.Angular.planeLinear_inverse line 70
  5. def OAI.PositiveEinsteinFour.Angular.planeIsometry line 89
  6. def OAI.PositiveEinsteinFour.Angular.planeRotation line 102
  7. theorem OAI.PositiveEinsteinFour.Angular.planeRotation_apply line 107
  8. theorem OAI.PositiveEinsteinFour.Angular.planeRotation_zero line 113
  9. def OAI.PositiveEinsteinFour.Angular.planeCoordinateDerivative line 120
  10. theorem OAI.PositiveEinsteinFour.Angular.hasDerivAt_planeRotation_coordinate line 124
  11. theorem OAI.PositiveEinsteinFour.Angular.continuous_planeRotation_coordinate line 140
  12. theorem OAI.PositiveEinsteinFour.Angular.continuous_planeCoordinateDerivative line 152
  13. theorem OAI.PositiveEinsteinFour.Angular.planeCoordinateDerivative_zero line 164