OAI/Geometry/EinsteinFour/ActualSphericalMoments.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The degree-two, four and six Folland formulas for the actual normalized Hausdorff measure. Both the moments and its probability normalization are proved here, so the geometric application need not assume them.

  1. theorem OAI.PositiveEinsteinFour.Angular.actual_follandMoments line 12