OAI/Geometry/EinsteinFour/SphericalSecondMoment.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The quadratic spherical moment follows from actual Hausdorff-measure invariance and the unit-sphere equation. Only probability normalization is needed; no moment identity is assumed.

  1. def OAI.PositiveEinsteinFour.Angular.coordinateFlip line 15
  2. theorem OAI.PositiveEinsteinFour.Angular.coordinateFlip_apply line 20
  3. def OAI.PositiveEinsteinFour.Angular.coordinatePermutation line 26
  4. theorem OAI.PositiveEinsteinFour.Angular.coordinatePermutation_apply line 29
  5. theorem OAI.PositiveEinsteinFour.Angular.sphereIntegral_odd line 33
  6. theorem OAI.PositiveEinsteinFour.Angular.integral_coordinate_mul_zero line 40
  7. theorem OAI.PositiveEinsteinFour.Angular.integral_coordinate_pow_eq line 46
  8. theorem OAI.PositiveEinsteinFour.Angular.integral_coordinate_square_eq line 53
  9. theorem OAI.PositiveEinsteinFour.Angular.integral_two_powers_odd line 58
  10. theorem OAI.PositiveEinsteinFour.Angular.sum_coordinate_sq line 65
  11. def OAI.PositiveEinsteinFour.Angular.coordinateMonomial line 69
  12. theorem OAI.PositiveEinsteinFour.Angular.coordinateMonomial_flip line 72
  13. theorem OAI.PositiveEinsteinFour.Angular.integral_coordinateMonomial_odd line 89
  14. theorem OAI.PositiveEinsteinFour.Angular.sphere_continuous_integrable line 97
  15. theorem OAI.PositiveEinsteinFour.Angular.integral_coordinate_square line 101
  16. theorem OAI.PositiveEinsteinFour.Angular.actual_spherical_second line 114