OAI/Geometry/EinsteinFour/SphericalMeasureInvariance.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The fixed Hausdorff spherical measure is invariant under all orthogonal changes of coordinates. This is the measure-theoretic input for the finite second, fourth and sixth moment computation.

  1. def OAI.PositiveEinsteinFour.Angular.directionIsometry line 15
  2. theorem OAI.PositiveEinsteinFour.Angular.sphereMeasure_preserving line 22
  3. theorem OAI.PositiveEinsteinFour.Angular.sphereIntegral_isometry line 29