BianchiCurvatureProjection.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The actual matrix-slot curvature form and its Bianchi compression.

def OAI.PositiveEinsteinFour.Bianchi.matrixCurvatureTensor line 17
Source documentation
The uncompressed matrix-slot operator, specialized to the diagonal curvature block v * S.s.
```
def matrixCurvatureTensor (S : Shape) (v : ℝ) (Z : Tensor) : Tensor where
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Tensor
theorem OAI.PositiveEinsteinFour.Bianchi.matrixCurvatureTensor_traceFree line 23
Source documentation
The trace-free anticommutator lands in the actual trace-free matrix space.
```
theorem matrixCurvatureTensor_traceFree (S : Shape) (v : ℝ) (Z : Tensor) :
    (matrixCurvatureTensor S v Z).traceFree := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.matrixCurvatureTensor
theorem OAI.PositiveEinsteinFour.Bianchi.tensor_pairing_eq_raw line 30
Source documentation
The coordinate pairing used for the raw commutator has the expected normalization relative to the Bianchi energy metric.
```
theorem tensor_pairing_eq_raw (Z W : Tensor) :
    rawPairing Z.matrix W.matrix = 6 * Z.pairing W := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.rawPairing
def OAI.PositiveEinsteinFour.Bianchi.curvatureBilinear line 37
Source documentation
The symmetric bilinear version of the actual matrix contraction.
```
def curvatureBilinear (S : Shape) (v : ℝ) (Z W : Tensor) : ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Tensor
theorem OAI.PositiveEinsteinFour.Bianchi.matrixCurvatureTensor_matrix line 42
Source documentation
Matrix entries agree with the invariant trace-free anticommutator.
```
theorem matrixCurvatureTensor_matrix (S : Shape) (v : ℝ) (Z : Tensor)
    (a b : Fin 3) (j : Fin 4) :
    (matrixCurvatureTensor S v Z).matrix a b j =
      diagonalCurvatureAction (fun s => v * S.s s)
        (fun a b => Z.matrix a b j) a b := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.matrixCurvatureTensor, OAI.PositiveEinsteinFour.Bianchi.diagonalCurvatureAction
theorem OAI.PositiveEinsteinFour.Bianchi.matrixCurvatureTensor_pairing line 54
Source documentation
The trace correction vanishes when paired with a trace-free tensor.
```
theorem matrixCurvatureTensor_pairing (S : Shape) (v : ℝ) (Z W : Tensor)
    (hw : W.traceFree) :
    (matrixCurvatureTensor S v Z).pairing W = curvatureBilinear S v Z W := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.matrixCurvatureTensor, OAI.PositiveEinsteinFour.Bianchi.curvatureBilinear
theorem OAI.PositiveEinsteinFour.Bianchi.parameters_add_diagonal line 67
theorem OAI.PositiveEinsteinFour.Bianchi.parameters_add_off line 74
theorem OAI.PositiveEinsteinFour.Bianchi.curvatureAction_bilinear line 82
Source documentation
Polarization identifies the full operator, not only its quadratic form.
```
theorem curvatureAction_bilinear (S : Shape) (v : ℝ) (p k l p' k' l' : Vec) :
    (curvatureAction S v p k l).pairing (parameters S p' k' l') =
      curvatureBilinear S v (parameters S p k l) (parameters S p' k' l') := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.curvatureAction, OAI.PositiveEinsteinFour.Bianchi.parameters, OAI.PositiveEinsteinFour.Bianchi.curvatureBilinear
theorem OAI.PositiveEinsteinFour.Bianchi.curvatureAction_compression line 105
Source documentation
The transported operator represents matrix-slot curvature against every actual Bianchi gradient. This is the defining orthogonal compression property.
```
theorem curvatureAction_compression (S : Shape) (v : ℝ) (p k l : Vec)
    (W : Tensor) (hw : W.traceFree) (hb : W.bianchi) :
    (curvatureAction S v p k l).pairing W =
      (matrixCurvatureTensor S v (parameters S p k l)).pairing W := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.curvatureAction, OAI.PositiveEinsteinFour.Bianchi.matrixCurvatureTensor, OAI.PositiveEinsteinFour.Bianchi.parameters
theorem OAI.PositiveEinsteinFour.Bianchi.curvatureAction_compressed_energy line 115
Source documentation
The square of the compressed operator is its pairing with the actual uncompressed matrix action, so the energy formula is the required E_B.
```
theorem curvatureAction_compressed_energy (S : Shape) (v : ℝ) (p k l : Vec) :
    (matrixCurvatureTensor S v (parameters S p k l)).pairing
        (curvatureAction S v p k l) =
      (curvatureAction S v p k l).squaredNorm / 6 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.matrixCurvatureTensor, OAI.PositiveEinsteinFour.Bianchi.parameters, OAI.PositiveEinsteinFour.Bianchi.curvatureAction