MatrixSlotCompression.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The bounded matrix-slot operator and the concrete Bianchi compression use the same Euclidean pairing and normalization.

def OAI.PositiveEinsteinFour.Geometry.rawGradientVector line 16
def OAI.PositiveEinsteinFour.Geometry.tensorGradientVector line 19
theorem OAI.PositiveEinsteinFour.Geometry.inner_rawGradientVector line 21
theorem OAI.PositiveEinsteinFour.Geometry.inner_tensorGradientVector line 29
theorem OAI.PositiveEinsteinFour.Geometry.tensorGradientVector_norm_sq line 34
theorem OAI.PositiveEinsteinFour.Geometry.tensorGradientVector_trace line 40
theorem OAI.PositiveEinsteinFour.Geometry.matrixSlotOperator_tensor line 47
Source documentation
The CLM has exactly the actual trace-free anticommutator entries.
```
theorem matrixSlotOperator_tensor (S : Shape) (v : ℝ) (Z : Tensor) (hz : Z.traceFree) :
    matrixSlotOperator (Matrix.diagonal (fun s => v * S.s s)) (tensorGradientVector Z) =
      tensorGradientVector (matrixCurvatureTensor S v Z) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.matrixSlotOperator, OAI.PositiveEinsteinFour.Geometry.tensorGradientVector
theorem OAI.PositiveEinsteinFour.Geometry.matrixSlotOperator_pairing line 62
Source documentation
Its uncompressed pairing against any trace-free tensor has the same normalization as the algebraic curvature form.
```
theorem matrixSlotOperator_pairing (S : Shape) (v : ℝ) (Z W : Tensor)
    (hz : Z.traceFree) (hw : W.traceFree) :
    inner ℝ (matrixSlotOperator (Matrix.diagonal (fun s => v * S.s s))
      (tensorGradientVector Z)) (tensorGradientVector W) =
        6 * curvatureBilinear S v Z W := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.matrixSlotOperator, OAI.PositiveEinsteinFour.Geometry.tensorGradientVector

theorem OAI.PositiveEinsteinFour.Geometry.matrixSlotOperator_compressed_energy line 72

Source documentation

The E_B term in the operator Green identity is the square of the actual orthogonal Bianchi compression.

theorem matrixSlotOperator_compressed_energy (S : Shape) (v : ℝ) (p k l : Vec) :
    inner ℝ (matrixSlotOperator (Matrix.diagonal (fun s => v * S.s s))
      (tensorGradientVector (parameters S p k l)))
      (tensorGradientVector (curvatureAction S v p k l)) =
        (curvatureAction S v p k l).squaredNorm := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.matrixSlotOperator, OAI.PositiveEinsteinFour.Geometry.tensorGradientVector