AngularDerivativeMoments.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The opposite Weyl blocks have zero mixed directional energy.

def OAI.PositiveEinsteinFour.Angular.weightedMixingMoment line 14
theorem OAI.PositiveEinsteinFour.Angular.weightedMixingMoment_symm line 17

theorem OAI.PositiveEinsteinFour.Angular.symmetric_contraction line 36

Source documentation

Symmetrize a finite contraction against a symmetric matrix.

theorem symmetric_contraction (T X : Fin 3 → Fin 3 → ℝ)
    (hT : ∀ i j, T i j = T j i) :
    2 * (∑ i, ∑ j, T i j * X i j) =
      ∑ i, ∑ j, T i j * (X i j + X j i) := by
…

theorem OAI.PositiveEinsteinFour.Angular.sum4_swap line 51
theorem OAI.PositiveEinsteinFour.Angular.weighted_mixing_contraction_zero line 72
Source documentation
The sixth moment cancels against a symmetric trace-free plus block. No differential Bianchi premise is needed for this angular identity.
```
theorem weighted_mixing_contraction_zero (h : FollandMoments)
    (T U : Fin 3 → Fin 3 → ℝ) (hT : ∀ i j, T i j = T j i)
    (ht : ∑ i, T i i = 0) (a b : Fin 4) :
    (∑ i, ∑ j, ∑ k, ∑ l,
      T i j * U k l * weightedMixingMoment a b i j k l) = 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Angular.FollandMoments, OAI.PositiveEinsteinFour.Angular.weightedMixingMoment
theorem OAI.PositiveEinsteinFour.Angular.integral_weighted_pairing_zero line 103
Source documentation
A weighted mixed contraction vanishes pointwise over the base.
```
theorem integral_weighted_pairing_zero (h : FollandMoments) (T U : Mat3)
    (hTs : Tᵀ = T) (hTt : T.trace = 0) (a b : Fin 4) :
    (∫ q, q.val a * q.val b * pairing T (rotated U q) ∂sphereMeasure) = 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Angular.FollandMoments, OAI.PositiveEinsteinFour.Angular.Mat3, OAI.PositiveEinsteinFour.Angular.pairing, OAI.PositiveEinsteinFour.Angular.rotated, OAI.PositiveEinsteinFour.Angular.sphereMeasure
def OAI.PositiveEinsteinFour.Angular.angularPairingLinear line 132
Source documentation
The Frobenius pairing, packaged only to expand finite directional sums.
```
def angularPairingLinear : Mat3 →ₗ[ℝ] Mat3 →ₗ[ℝ] ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Angular.Mat3
def OAI.PositiveEinsteinFour.Angular.rotatedLinear line 145
theorem OAI.PositiveEinsteinFour.Angular.directional_pairing line 148
theorem OAI.PositiveEinsteinFour.Angular.integral_directional_pairing_zero line 164
Source documentation
The exact derivative mixed cancellation uses only symmetry and zero trace.
```
theorem integral_directional_pairing_zero (h : FollandMoments) (Z W : Gradient)
    (hZs : ∀ a, (Z a)ᵀ = Z a) (hZt : ∀ a, (Z a).trace = 0) :
    (∫ q, pairing (directional Z q) (rotated (directional W q) q) ∂sphereMeasure) = 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Angular.FollandMoments, OAI.PositiveEinsteinFour.Angular.Gradient, OAI.PositiveEinsteinFour.Angular.pairing, OAI.PositiveEinsteinFour.Angular.directional, OAI.PositiveEinsteinFour.Angular.rotated, OAI.PositiveEinsteinFour.Angular.sphereMeasure
theorem OAI.PositiveEinsteinFour.Angular.integral_normalDerivative_squareNorm_exact line 184
Source documentation
The second exact angular energy identity used by the radial estimate.
```
theorem integral_normalDerivative_squareNorm_exact (h : FollandMoments) (Z W : Gradient)
    (hZs : ∀ a, (Z a)ᵀ = Z a) (hZt : ∀ a, (Z a).trace = 0) :
    (∫ q, squareNorm (normalDerivative Z W q) ∂sphereMeasure) =
      (gradientSquareNorm Z + gradientSquareNorm W) / 16 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Angular.FollandMoments, OAI.PositiveEinsteinFour.Angular.Gradient, OAI.PositiveEinsteinFour.Angular.squareNorm, OAI.PositiveEinsteinFour.Angular.normalDerivative, OAI.PositiveEinsteinFour.Angular.sphereMeasure, OAI.PositiveEinsteinFour.Angular.gradientSquareNorm