SphericalMoments.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

The finite sphere moments needed for the angular Jacobi calculation. The conditional input below is precisely the degree 2, 4 and 6 specialization of Folland, How to Integrate a Polynomial over a Sphere, American Mathematical Monthly 108 (2001), 446–448, Theorem on p.447, after division by the area of S³. DOI: 10.1080/00029890.2001.11919774. It contains no curvature or geometric inequality.

abbrev OAI.PositiveEinsteinFour.Angular.Directions line 20
instance OAI.PositiveEinsteinFour.Angular.(instance at line 22) line 22
def OAI.PositiveEinsteinFour.Angular.sphereMeasure line 28
Source documentation
The normalized spherical measure is fixed, not an arbitrary probability measure satisfying the desired curvature averages.
```
def sphereMeasure : Measure Directions :=
…
```
Mentions: OAI.PositiveEinsteinFour.Angular.Directions
def OAI.PositiveEinsteinFour.Angular.delta line 32
def OAI.PositiveEinsteinFour.Angular.momentTwo line 34
def OAI.PositiveEinsteinFour.Angular.momentFour line 36
def OAI.PositiveEinsteinFour.Angular.momentSix line 40
Source documentation
The fifteen pairings of six indices, grouped by the partner of i.
```
def momentSix (i j k l m n : Fin 4) : ℝ :=
…
```
structure OAI.PositiveEinsteinFour.Angular.FollandMoments line 46
Source documentation
Finite angular moment identities.
```
structure FollandMoments : Prop where
…
```
theorem OAI.PositiveEinsteinFour.Angular.continuous_coordinate line 57
theorem OAI.PositiveEinsteinFour.Angular.continuous_integrable line 60
theorem OAI.PositiveEinsteinFour.Angular.integral_sum line 65
theorem OAI.PositiveEinsteinFour.Angular.integral_sum4 line 70
theorem OAI.PositiveEinsteinFour.Angular.integral_quadratic line 87
theorem OAI.PositiveEinsteinFour.Angular.integral_directional_square line 100
Source documentation
A directional derivative has one fourth of its full squared norm on S³.
```
theorem integral_directional_square (h : FollandMoments) (v : Fin 4 → ℝ) :
    (∫ q : Directions, (∑ i, q.val i * v i) ^ 2 ∂sphereMeasure) =
      (∑ i, v i ^ 2) / 4 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Angular.FollandMoments, OAI.PositiveEinsteinFour.Angular.Directions, OAI.PositiveEinsteinFour.Angular.sphereMeasure