OAI/Geometry/EinsteinFour/SphericalFourthMoment.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The quartic sphere moments from the explicit orthogonal coordinate changes. Probability normalization remains separate from the moment proof.

  1. theorem OAI.PositiveEinsteinFour.Angular.sqrt_two_fourth line 17
  2. theorem OAI.PositiveEinsteinFour.Angular.integral_fourth_three_mixed line 22
  3. theorem OAI.PositiveEinsteinFour.Angular.sum_single_exception line 62
  4. theorem OAI.PositiveEinsteinFour.Angular.integral_coordinate_fourth line 73
  5. theorem OAI.PositiveEinsteinFour.Angular.integral_coordinate_square_square line 99
  6. theorem OAI.PositiveEinsteinFour.Angular.actual_spherical_fourth line 105