GradientCasimir.lean`

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The actual Bianchi coupling operator on first derivatives.

def OAI.PositiveEinsteinFour.Bianchi.matrixRotation line 15
Source documentation
Matrix-slot rotation, retaining the actual tangent four-vectors.
```
def matrixRotation (s : Fin 3) (Z : Tensor) (a b : Fin 3) : Vec :=
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.Vec
def OAI.PositiveEinsteinFour.Bianchi.gradientCoupling line 20
Source documentation
The coupling in the Bianchi projector (6-C)/10.
```
def gradientCoupling (Z : Tensor) (a b : Fin 3) : Vec :=
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.Vec
theorem OAI.PositiveEinsteinFour.Bianchi.diagonal_zero_from_bianchi line 23
theorem OAI.PositiveEinsteinFour.Bianchi.diagonal_one_from_bianchi line 29
theorem OAI.PositiveEinsteinFour.Bianchi.diagonal_two_from_bianchi line 35
theorem OAI.PositiveEinsteinFour.Bianchi.gradientCoupling_zero line 41
theorem OAI.PositiveEinsteinFour.Bianchi.gradientCoupling_one line 52
theorem OAI.PositiveEinsteinFour.Bianchi.gradientCoupling_two line 63
theorem OAI.PositiveEinsteinFour.Bianchi.gradientCoupling_eq line 75
Source documentation
The Bianchi equation puts every gradient in the actual C=-4 subspace.
```
theorem gradientCoupling_eq (Z : Tensor) (hb : Z.bianchi) (a b : Fin 3) :
    gradientCoupling Z a b = (-4 : ℝ) • Z.matrix a b := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.gradientCoupling
theorem OAI.PositiveEinsteinFour.Bianchi.quaternion_inner line 83
Source documentation
Quaternion multiplication preserves the full Euclidean inner product.
```
theorem quaternion_inner (s : Fin 3) (p q : Vec) :
    inner ℝ (quaternion s p) (quaternion s q) = inner ℝ p q := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.quaternion
theorem OAI.PositiveEinsteinFour.Bianchi.quaternion_inner_skew line 91
Source documentation
The infinitesimal quaternion action is skew-adjoint.
```
theorem quaternion_inner_skew (s : Fin 3) (p q : Vec) :
    inner ℝ (quaternion s p) q = -inner ℝ p (quaternion s q) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.quaternion
theorem OAI.PositiveEinsteinFour.Bianchi.rotate_sums line 97
theorem OAI.PositiveEinsteinFour.Bianchi.matrixRotation_component line 112
theorem OAI.PositiveEinsteinFour.Bianchi.matrixRotation_energy line 120
Source documentation
The matrix-spin Casimir on the actual four-vector-valued tensor.
```
theorem matrixRotation_energy (Z : Tensor) (hz : Z.traceFree) :
    (∑ a, ∑ b, ∑ s, ‖matrixRotation s Z a b‖ ^ 2) = 24 * Z.squaredNorm := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.matrixRotation
def OAI.PositiveEinsteinFour.Bianchi.gradientGenerator line 146
Source documentation
The actual total plus generator on a Bianchi gradient.
```
def gradientGenerator (s : Fin 3) (Z : Tensor) (a b : Fin 3) : Vec :=
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.Vec
theorem OAI.PositiveEinsteinFour.Bianchi.gradientGenerator_energy line 150
Source documentation
The Bianchi gradient has the exact inner Casimir energy 35.
```
theorem gradientGenerator_energy (Z : Tensor) (hz : Z.traceFree) (hb : Z.bianchi) :
    (∑ a, ∑ b, ∑ s, ‖gradientGenerator s Z a b‖ ^ 2) = 35 * Z.squaredNorm := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.gradientGenerator