GradientProjection.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The compressed derivative generator in the actual quaternion model.

theorem OAI.PositiveEinsteinFour.Bianchi.quaternion_anticommutator line 15
Source documentation
The Clifford anticommutator, with the normalization of the fixed frame.
```
theorem quaternion_anticommutator (r s : Fin 3) (q : Vec) :
    quaternion r (quaternion s q) + quaternion s (quaternion r q) =
      if r = s then (-2 : ℝ) • q else 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.quaternion
def OAI.PositiveEinsteinFour.Bianchi.diagonalCurvatureAction line 23
Source documentation
The matrix-slot curvature operator for a diagonal trace-free curvature block.
```
def diagonalCurvatureAction (t : Fin 3 → ℝ) (M : Mat) : Mat := fun a b =>
…
```
theorem OAI.PositiveEinsteinFour.Bianchi.weighted_matrixAction_square line 29
Source documentation
The normalization of the spin-two curvature operator is a direct five-coordinate identity.
```
theorem weighted_matrixAction_square (t : Fin 3 → ℝ) (ht : ∑ s, t s = 0)
    (M : Mat) (hs : symmetric M) (hm : traceFree M) :
    (∑ s, t s • matrixAction s (matrixAction s M)) =
      (24 : ℝ) • diagonalCurvatureAction t M := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.diagonalCurvatureAction
def OAI.PositiveEinsteinFour.Bianchi.derivativeQuaternion line 48
Source documentation
Apply a quaternion only in the derivative slot of a matrix-valued tensor.
```
def derivativeQuaternion (r : Fin 3) (Z : Tensor) : Tensor where
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor
theorem OAI.PositiveEinsteinFour.Bianchi.derivativeQuaternion_matrix line 52
theorem OAI.PositiveEinsteinFour.Bianchi.matrixRotation_derivativeQuaternion line 58
Source documentation
Matrix rotations commute with the action on the derivative slot.
```
theorem matrixRotation_derivativeQuaternion (r s : Fin 3) (Z : Tensor)
    (a b : Fin 3) :
    matrixRotation s (derivativeQuaternion r Z) a b =
      quaternion r (matrixRotation s Z a b) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.matrixRotation, OAI.PositiveEinsteinFour.Bianchi.derivativeQuaternion, OAI.PositiveEinsteinFour.Bianchi.quaternion
theorem OAI.PositiveEinsteinFour.Bianchi.gradientCoupling_anticommutator line 67
Source documentation
The exact anticommutator between the Bianchi coupling and a derivative quaternion. No irreducible-representation assertion is assumed.
```
theorem gradientCoupling_anticommutator (r : Fin 3) (Z : Tensor)
    (a b : Fin 3) :
    gradientCoupling (derivativeQuaternion r Z) a b +
      quaternion r (gradientCoupling Z a b) = (-2 : ℝ) • matrixRotation r Z a b := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.gradientCoupling, OAI.PositiveEinsteinFour.Bianchi.derivativeQuaternion, OAI.PositiveEinsteinFour.Bianchi.quaternion, OAI.PositiveEinsteinFour.Bianchi.matrixRotation
def OAI.PositiveEinsteinFour.Bianchi.gradientProjection line 89
Source documentation
The polynomial expression for the orthogonal Bianchi projector.
```
def gradientProjection (Z : Tensor) (a b : Fin 3) : Vec :=
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.Vec
theorem OAI.PositiveEinsteinFour.Bianchi.gradientProjection_eq line 93
Source documentation
The projector fixes every actual Bianchi tensor.
```
theorem gradientProjection_eq (Z : Tensor) (hb : Z.bianchi) (a b : Fin 3) :
    gradientProjection Z a b = Z.matrix a b := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.gradientProjection
theorem OAI.PositiveEinsteinFour.Bianchi.gradientProjection_derivativeQuaternion line 100
Source documentation
Compressing the derivative quaternion to the Bianchi subspace gives one fifth of the total inner generator, with the coefficient derived explicitly.
```
theorem gradientProjection_derivativeQuaternion (r : Fin 3) (Z : Tensor)
    (hb : Z.bianchi) (a b : Fin 3) :
    gradientProjection (derivativeQuaternion r Z) a b =
      (1 / 5 : ℝ) • gradientGenerator r Z a b := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.gradientProjection, OAI.PositiveEinsteinFour.Bianchi.derivativeQuaternion, OAI.PositiveEinsteinFour.Bianchi.gradientGenerator