AngularQuadratic.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Angular averages of two quadratic forms, from the precise fourth spherical moment. This is used for the two Weyl blocks in the normal Jacobi matrix; no curvature average is an input.

abbrev OAI.PositiveEinsteinFour.Angular.Mat4 line 15
def OAI.PositiveEinsteinFour.Angular.quadratic line 17
theorem OAI.PositiveEinsteinFour.Angular.continuous_quadratic line 20
theorem OAI.PositiveEinsteinFour.Angular.integral_quadratic_mul line 24

theorem OAI.PositiveEinsteinFour.Angular.fourth_sum_formula line 60

Source documentation

The finite contraction is stated on functions so that no matrix coercion is unfolded inside the simplifier.

theorem fourth_sum_formula (C D : Fin 4 → Fin 4 → ℝ) :
    (∑ i, ∑ j, ∑ k, ∑ l, C i j * D k l * momentFour i j k l) =
      ((∑ i, C i i) * (∑ j, D j j) + (∑ i, ∑ j, C i j * D i j) +
        (∑ i, ∑ j, C i j * D j i)) / 24 := by
…

Mentions: OAI.PositiveEinsteinFour.Angular.momentFour

theorem OAI.PositiveEinsteinFour.Angular.integral_quadratic_mul_formula line 75
Source documentation
Fourth moments give the complete bilinear quadratic-form formula.
```
theorem integral_quadratic_mul_formula (h : FollandMoments) (C D : Mat4) :
    (∫ q, quadratic C q * quadratic D q ∂sphereMeasure) =
      (C.trace * D.trace + (∑ i, ∑ j, C i j * D i j) +
        (∑ i, ∑ j, C i j * D j i)) / 24 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Angular.FollandMoments, OAI.PositiveEinsteinFour.Angular.Mat4, OAI.PositiveEinsteinFour.Angular.quadratic, OAI.PositiveEinsteinFour.Angular.sphereMeasure
theorem OAI.PositiveEinsteinFour.Angular.integral_quadratic_mul_traceFree line 82