OAI/Geometry/EinsteinFour/SphericalMomentRecurrence.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The infinitesimal rotation identity for the degree-six spherical moment. The five factors left after differentiation determine the recurrence.

  1. def OAI.PositiveEinsteinFour.Angular.fiveProduct line 14
  2. def OAI.PositiveEinsteinFour.Angular.fiveOmit line 16
  3. def OAI.PositiveEinsteinFour.Angular.sphereRotationGenerator line 19
  4. theorem OAI.PositiveEinsteinFour.Angular.fiveProduct_eq_mul_omit line 23
  5. theorem OAI.PositiveEinsteinFour.Angular.sum_sphereRotationGenerator line 28
  6. theorem OAI.PositiveEinsteinFour.Angular.integral_sphereRotationGenerator_zero line 70
  7. theorem OAI.PositiveEinsteinFour.Angular.spherical_sixth_recurrence line 141
  8. theorem OAI.PositiveEinsteinFour.Angular.fiveOmit_eq_succAbove line 166