OAI/Geometry/EinsteinFour/SphericalSixthMoment.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The degree-six formula follows from the infinitesimal rotation recurrence and the already proved quartic formula. Only positivity and finiteness of the unnormalized Hausdorff mass remain in the spherical input.

  1. theorem OAI.PositiveEinsteinFour.Angular.fiveOmit_vector line 15
  2. theorem OAI.PositiveEinsteinFour.Angular.delta_comm line 25
  3. theorem OAI.PositiveEinsteinFour.Angular.actual_spherical_sixth line 30
  4. theorem OAI.PositiveEinsteinFour.Angular.follandMoments_of_probability line 46