GradientMixedPairing.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Bilinear matrix-slot compression on two actual Bianchi gradients.

def OAI.PositiveEinsteinFour.Bianchi.addTensor line 15
theorem OAI.PositiveEinsteinFour.Bianchi.addTensor_matrix line 19
theorem OAI.PositiveEinsteinFour.Bianchi.addTensor_traceFree line 24
theorem OAI.PositiveEinsteinFour.Bianchi.addTensor_bianchi line 29

theorem OAI.PositiveEinsteinFour.Bianchi.generator_row_pairing line 37

Source documentation

Polarization of the exact generator norm identity.

theorem generator_row_pairing (s : Fin 3) (Z W : Tensor)
    (hz : Z.traceFree) (hbz : Z.bianchi) (hw : W.traceFree) (hbw : W.bianchi) :
    rawPairing (rawGradientGenerator s Z.matrix) (rawGradientGenerator s W.matrix) +
      40 * (∑ b, inner ℝ (Z.matrix s b) (W.matrix s b)) =
        25 * rawPairing Z.matrix W.matrix := by
…

Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.rawPairing, OAI.PositiveEinsteinFour.Bianchi.rawGradientGenerator

def OAI.PositiveEinsteinFour.Bianchi.diagonalGradientPairing line 54
Source documentation
The diagonal matrix-slot form keeps both Bianchi arguments.
```
def diagonalGradientPairing (t : Fin 3 → ℝ) (Z W : Tensor) : ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor
theorem OAI.PositiveEinsteinFour.Bianchi.weighted_generator_pairing line 57
def OAI.PositiveEinsteinFour.Bianchi.mixedCouplingPairing line 69
theorem OAI.PositiveEinsteinFour.Bianchi.mixedCouplingPairing_eq line 73
Source documentation
The one-fifth derivative-slot compression also holds in the bilinear form.
```
theorem mixedCouplingPairing_eq (s : Fin 3) (Z W : Tensor)
    (hz : Z.traceFree) (hbz : Z.bianchi) (hbw : W.bianchi) :
    mixedCouplingPairing s Z W = rawPairing Z.matrix W.matrix -
      (1 / 5 : ℝ) * rawPairing (rawGradientGenerator s Z.matrix)
        (rawGradientGenerator s W.matrix) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.mixedCouplingPairing, OAI.PositiveEinsteinFour.Bianchi.rawPairing, OAI.PositiveEinsteinFour.Bianchi.rawGradientGenerator
theorem OAI.PositiveEinsteinFour.Bianchi.weighted_mixedCouplingPairing line 97
Source documentation
Exact mixed compression, with arbitrary actual Bianchi tensors in both slots.
```
theorem weighted_mixedCouplingPairing (t : Fin 3 → ℝ) (ht : ∑ s, t s = 0)
    (Z W : Tensor) (hz : Z.traceFree) (hbz : Z.bianchi)
    (hw : W.traceFree) (hbw : W.bianchi) :
    (∑ s, t s * mixedCouplingPairing s Z W) = 8 * diagonalGradientPairing t Z W := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.mixedCouplingPairing, OAI.PositiveEinsteinFour.Bianchi.diagonalGradientPairing
def OAI.PositiveEinsteinFour.Bianchi.rawMatrixCurvature line 119
Source documentation
The actual trace-free anticommutator, applied independently in each derivative direction.
```
def rawMatrixCurvature (t : Fin 3 → ℝ) (Z : Tensor) : RawGradient := fun a b =>
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.RawGradient
theorem OAI.PositiveEinsteinFour.Bianchi.rawMatrixCurvature_component line 123
theorem OAI.PositiveEinsteinFour.Bianchi.rawMatrixCurvature_shape line 134
theorem OAI.PositiveEinsteinFour.Bianchi.rawMatrixCurvature_pairing line 141
Source documentation
The trace correction is orthogonal to the trace-free second argument.
```
theorem rawMatrixCurvature_pairing (t : Fin 3 → ℝ) (Z W : Tensor)
    (hw : W.traceFree) :
    rawPairing (rawMatrixCurvature t Z) W.matrix = diagonalGradientPairing t Z W := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.rawPairing, OAI.PositiveEinsteinFour.Bianchi.rawMatrixCurvature, OAI.PositiveEinsteinFour.Bianchi.diagonalGradientPairing
theorem OAI.PositiveEinsteinFour.Bianchi.weighted_mixed_rawMatrixCurvature line 179
Source documentation
The requested arbitrary-argument compression in actual matrix entries.
```
theorem weighted_mixed_rawMatrixCurvature (t : Fin 3 → ℝ) (ht : ∑ s, t s = 0)
    (Z W : Tensor) (hz : Z.traceFree) (hbz : Z.bianchi)
    (hw : W.traceFree) (hbw : W.bianchi) :
    (∑ s, t s * mixedCouplingPairing s Z W) =
      8 * rawPairing (rawMatrixCurvature t Z) W.matrix := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.mixedCouplingPairing, OAI.PositiveEinsteinFour.Bianchi.rawPairing, OAI.PositiveEinsteinFour.Bianchi.rawMatrixCurvature
theorem OAI.PositiveEinsteinFour.Bianchi.diagonalGradientPairing_curvatureBilinear line 189
Source documentation
The row pairing is the actual matrix-slot curvature operator, with its normalization inherited from the Frobenius tensor pairing.
```
theorem diagonalGradientPairing_curvatureBilinear (S : Shape) (v : ℝ) (Z W : Tensor) :
    diagonalGradientPairing (fun s => v * S.s s) Z W =
      6 * curvatureBilinear S v Z W := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.diagonalGradientPairing, OAI.PositiveEinsteinFour.Bianchi.curvatureBilinear
theorem OAI.PositiveEinsteinFour.Bianchi.weighted_mixed_matrixCurvature line 199
Source documentation
The weighted mixed operator agrees with eight times the actual uncompressed matrix-slot operator, against every Bianchi test tensor.
```
theorem weighted_mixed_matrixCurvature (S : Shape) (v : ℝ) (Z W : Tensor)
    (hz : Z.traceFree) (hbz : Z.bianchi) (hw : W.traceFree) (hbw : W.bianchi) :
    (∑ s, (v * S.s s) * mixedCouplingPairing s Z W) =
      8 * rawPairing (matrixCurvatureTensor S v Z).matrix W.matrix := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.mixedCouplingPairing, OAI.PositiveEinsteinFour.Bianchi.rawPairing, OAI.PositiveEinsteinFour.Bianchi.matrixCurvatureTensor
theorem OAI.PositiveEinsteinFour.Bianchi.weighted_mixed_curvatureAction line 212
Source documentation
After orthogonal Bianchi compression the same bilinear identity pairs with the concrete transported operator, including when the test tensor is that operator itself.
```
theorem weighted_mixed_curvatureAction (S : Shape) (v : ℝ) (p k l : Vec)
    (W : Tensor) (hw : W.traceFree) (hbw : W.bianchi) :
    (∑ s, (v * S.s s) * mixedCouplingPairing s (parameters S p k l) W) =
      48 * (curvatureAction S v p k l).pairing W := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.mixedCouplingPairing, OAI.PositiveEinsteinFour.Bianchi.parameters, OAI.PositiveEinsteinFour.Bianchi.curvatureAction
theorem OAI.PositiveEinsteinFour.Bianchi.weighted_mixed_curvatureAction_energy line 223
Source documentation
Testing with the compressed curvature action gives its exact squared energy, the term used in the nonparallel matrix-slot Green identity.
```
theorem weighted_mixed_curvatureAction_energy (S : Shape) (v : ℝ) (p k l : Vec) :
    (∑ s, (v * S.s s) * mixedCouplingPairing s (parameters S p k l)
      (curvatureAction S v p k l)) =
        8 * (curvatureAction S v p k l).squaredNorm := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.mixedCouplingPairing, OAI.PositiveEinsteinFour.Bianchi.parameters, OAI.PositiveEinsteinFour.Bianchi.curvatureAction