MatrixSlotCubic.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The varying matrix-slot correction is the actual cubic trace in the weighted Hessian identity.

theorem OAI.PositiveEinsteinFour.Geometry.matrixPairing_eq_trace line 15
theorem OAI.PositiveEinsteinFour.Geometry.matrixSlotAction_eq line 20
theorem OAI.PositiveEinsteinFour.Geometry.matrixSlotAction_self_pairing line 29
theorem OAI.PositiveEinsteinFour.Geometry.matrixSlot_cubic_trace line 44
Source documentation
Summing over the derivative index gives the cubic trace, with no diagonalization assumption on the varying coefficient.
```
theorem matrixSlot_cubic_trace (A : Mat) (Z : Gradient)
    (hs : ∀ j, symmetric (Z j)) (ht : ∀ j, traceFree (Z j)) :
    inner ℝ (matrixSlotOperator A (gradientVector Z)) (gradientVector Z) =
      Matrix.trace (A * (∑ j, Z j * Z j)) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.matrixSlotOperator, OAI.PositiveEinsteinFour.Geometry.gradientVector