AngularSixth.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Sixth spherical moments for the directional derivative of normal curvature. All moments are the explicit Folland specialization from SphericalMoments.

theorem OAI.PositiveEinsteinFour.Angular.fourth_single_contraction line 15
Source documentation
Contracting one fourth moment with a matrix.
```
theorem fourth_single_contraction (D : Fin 4 → Fin 4 → ℝ) (a b : Fin 4) :
    (∑ k, ∑ l, D k l * momentFour a b k l) =
      (delta a b * (∑ k, D k k) + D a b + D b a) / 24 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Angular.momentFour, OAI.PositiveEinsteinFour.Angular.delta
theorem OAI.PositiveEinsteinFour.Angular.delta_symm line 27
theorem OAI.PositiveEinsteinFour.Angular.momentFour_cycle line 30

theorem OAI.PositiveEinsteinFour.Angular.sixth_sum_recursion line 37

Source documentation

Group the fifteen pairings by the partner of the first index.

theorem sixth_sum_recursion (C D : Fin 4 → Fin 4 → ℝ) (a b : Fin 4) :
    (∑ i, ∑ j, ∑ k, ∑ l, C i j * D k l * momentSix a b i j k l) =
      (delta a b * (∑ i, ∑ j, ∑ k, ∑ l, C i j * D k l * momentFour i j k l) +
        (∑ j, C a j * (∑ k, ∑ l, D k l * momentFour b j k l)) +
        (∑ i, C i a * (∑ k, ∑ l, D k l * momentFour b i k l)) +
        (∑ l, D a l * (∑ i, ∑ j, C i j * momentFour b l i j)) +
        (∑ k, D k a * (∑ i, ∑ j, C i j * momentFour b k i j))) / 8 := by
…

Mentions: OAI.PositiveEinsteinFour.Angular.momentSix, OAI.PositiveEinsteinFour.Angular.delta, OAI.PositiveEinsteinFour.Angular.momentFour

theorem OAI.PositiveEinsteinFour.Angular.fourth_single_contraction_traceFree line 105

theorem OAI.PositiveEinsteinFour.Angular.sixth_sum_traceFree line 112

Source documentation

A fourth-degree harmonic has no second-degree spherical moment.

theorem sixth_sum_traceFree (C D : Fin 4 → Fin 4 → ℝ)
    (hC : ∑ k, C k k = 0) (hD : ∑ k, D k k = 0)
    (hCs : ∀ i j, C i j = C j i) (hDs : ∀ i j, D i j = D j i)
    (a b : Fin 4) :
    (∑ i, ∑ j, ∑ k, ∑ l, C i j * D k l * momentSix a b i j k l) =
      delta a b * (∑ i, ∑ j, C i j * D i j) / 96 +
        ((∑ k, C a k * D k b) + (∑ k, D a k * C k b)) / 48 := by
…

Mentions: OAI.PositiveEinsteinFour.Angular.momentSix, OAI.PositiveEinsteinFour.Angular.delta

theorem OAI.PositiveEinsteinFour.Angular.integral_weighted_quadratic_mul line 141
Source documentation
The raw weighted quadratic product is exactly a sixth-moment contraction.
```
theorem integral_weighted_quadratic_mul (h : FollandMoments)
    (C D : Mat4) (a b : Fin 4) :
    (∫ q, q.val a * q.val b * (quadratic C q * quadratic D q) ∂sphereMeasure) =
      ∑ i, ∑ j, ∑ k, ∑ l, C i j * D k l * momentSix a b i j k l := by
…
```
Mentions: OAI.PositiveEinsteinFour.Angular.FollandMoments, OAI.PositiveEinsteinFour.Angular.Mat4, OAI.PositiveEinsteinFour.Angular.quadratic, OAI.PositiveEinsteinFour.Angular.sphereMeasure, OAI.PositiveEinsteinFour.Angular.momentSix
theorem OAI.PositiveEinsteinFour.Angular.integral_weighted_quadratic_mul_traceFree line 192
Source documentation
The useful matrix form of the sixth moment.
```
theorem integral_weighted_quadratic_mul_traceFree (h : FollandMoments)
    (C D : Mat4) (hC : C.trace = 0) (hD : D.trace = 0)
    (hCs : Cᵀ = C) (hDs : Dᵀ = D) (a b : Fin 4) :
    (∫ q, q.val a * q.val b * (quadratic C q * quadratic D q) ∂sphereMeasure) =
      delta a b * (∑ i, ∑ j, C i j * D i j) / 96 +
        (C * D + D * C) a b / 48 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Angular.FollandMoments, OAI.PositiveEinsteinFour.Angular.Mat4, OAI.PositiveEinsteinFour.Angular.quadratic, OAI.PositiveEinsteinFour.Angular.sphereMeasure, OAI.PositiveEinsteinFour.Angular.delta