Bianchi.lean`

50 declarations, 0 contain sorry, 0 declared as axioms

Concrete four-vector coordinates for a Bianchi gradient

The three quaternion actions are left multiplication by i,j,k on the real four-dimensional Euclidean space. A symmetric matrix of four-vectors is encoded by its three diagonal and three off-diagonal entries. Its divergence constraint is the actual quaternionic Bianchi constraint of Section 2.

abbrev OAI.PositiveEinsteinFour.Bianchi.Vec line 24
def OAI.PositiveEinsteinFour.Bianchi.quaternion line 27
Source documentation
The fixed positive quaternion triple.
```
def quaternion (i : Fin 3) (q : Vec) : Vec :=
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec
def OAI.PositiveEinsteinFour.Bianchi.next line 32
def OAI.PositiveEinsteinFour.Bianchi.previous line 34
theorem OAI.PositiveEinsteinFour.Bianchi.quaternion_add line 36
theorem OAI.PositiveEinsteinFour.Bianchi.quaternion_smul line 40
theorem OAI.PositiveEinsteinFour.Bianchi.quaternion_neg line 44
theorem OAI.PositiveEinsteinFour.Bianchi.quaternion_zero line 48
theorem OAI.PositiveEinsteinFour.Bianchi.quaternion_square line 51
theorem OAI.PositiveEinsteinFour.Bianchi.quaternion_injective line 55
theorem OAI.PositiveEinsteinFour.Bianchi.quaternion_norm_sq line 61
Source documentation
All three quaternion actions preserve the Euclidean metric.
```
@[simp] theorem quaternion_norm_sq (i : Fin 3) (q : Vec) :
    ‖quaternion i q‖ ^ 2 = ‖q‖ ^ 2 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.quaternion
theorem OAI.PositiveEinsteinFour.Bianchi.quaternion_norm line 66
structure OAI.PositiveEinsteinFour.Bianchi.Shape line 71
Source documentation
The normalized diagonal spectral shape.
```
structure Shape where
…
```
def OAI.PositiveEinsteinFour.Bianchi.difference line 78
Source documentation
This is √3 * s̃; using it avoids divisions by a square root in the coordinate inverse.
```
def difference (s : Fin 3 → ℝ) (i : Fin 3) : ℝ := s (next i) - s (previous i)
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.next, OAI.PositiveEinsteinFour.Bianchi.previous
theorem OAI.PositiveEinsteinFour.Bianchi.difference_sum line 80
theorem OAI.PositiveEinsteinFour.Bianchi.Shape.difference_square line 84
theorem OAI.PositiveEinsteinFour.Bianchi.difference_orthogonal line 91
theorem OAI.PositiveEinsteinFour.Bianchi.Shape.difference_next_sub_previous line 95
theorem OAI.PositiveEinsteinFour.Bianchi.Shape.frame line 102
Source documentation
Completeness relation of the two orthogonal normalized spectral vectors.
```
theorem Shape.frame (S : Shape) (i j : Fin 3) :
    S.s i * S.s j / 6 + difference S.s i * difference S.s j / 18 =
      (if i = j then 1 else 0) - 1 / 3 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.difference
structure OAI.PositiveEinsteinFour.Bianchi.Tensor line 116
Source documentation
Symmetric three-by-three matrix with four-vector entries. off i is the entry in positions (next i, previous i) and its transpose.
```
@[ext] structure Tensor where
…
```
def OAI.PositiveEinsteinFour.Bianchi.Tensor.matrix line 120
theorem OAI.PositiveEinsteinFour.Bianchi.Tensor.matrix_symmetric line 125
def OAI.PositiveEinsteinFour.Bianchi.Tensor.traceFree line 129
def OAI.PositiveEinsteinFour.Bianchi.Tensor.divergence line 132
Source documentation
Quaternionic divergence in each matrix column.
```
def Tensor.divergence (T : Tensor) (i : Fin 3) : Vec :=
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.Vec
theorem OAI.PositiveEinsteinFour.Bianchi.Tensor.divergence_eq_sum line 138
Source documentation
The concrete divergence is contraction of the quaternion action with an actual matrix column.
```
theorem Tensor.divergence_eq_sum (T : Tensor) (i : Fin 3) :
    T.divergence i = ∑ j, quaternion j (T.matrix j i) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.quaternion
def OAI.PositiveEinsteinFour.Bianchi.Tensor.bianchi line 143
def OAI.PositiveEinsteinFour.Bianchi.Tensor.auxiliary line 145
theorem OAI.PositiveEinsteinFour.Bianchi.Tensor.quaternion_divergence line 149
Source documentation
Multiplying the divergence equation by the corresponding complex structure gives the elementary cyclic constraint.
```
theorem Tensor.quaternion_divergence (T : Tensor) (i : Fin 3) :
    quaternion i (T.divergence i) =
      -(T.diagonal i + T.auxiliary (next i) - T.auxiliary (previous i)) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.quaternion, OAI.PositiveEinsteinFour.Bianchi.next, OAI.PositiveEinsteinFour.Bianchi.previous
theorem OAI.PositiveEinsteinFour.Bianchi.Tensor.bianchi_iff line 155
def OAI.PositiveEinsteinFour.Bianchi.parameters line 167
Source documentation
Explicit equation (2), in terms of √3 * s̃.
```
def parameters (S : Shape) (p k l : Vec) : Tensor where
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.Tensor
theorem OAI.PositiveEinsteinFour.Bianchi.parameters_auxiliary line 171
theorem OAI.PositiveEinsteinFour.Bianchi.parameters_traceFree line 176
theorem OAI.PositiveEinsteinFour.Bianchi.parameters_bianchi line 183
def OAI.PositiveEinsteinFour.Bianchi.radialCoordinate line 203
Source documentation
Radial coordinate recovered directly from the diagonal entries.
```
def radialCoordinate (S : Shape) (T : Tensor) : Vec :=
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.Vec
def OAI.PositiveEinsteinFour.Bianchi.secondCoordinate line 207
Source documentation
Orthogonal diagonal coordinate recovered directly from the entries.
```
def secondCoordinate (S : Shape) (T : Tensor) : Vec :=
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.Vec
theorem OAI.PositiveEinsteinFour.Bianchi.radialCoordinate_parameters line 210
theorem OAI.PositiveEinsteinFour.Bianchi.secondCoordinate_parameters line 218
theorem OAI.PositiveEinsteinFour.Bianchi.diagonal_reconstruction line 230
Source documentation
Every trace-free diagonal triple is recovered by the two coordinates.
```
theorem diagonal_reconstruction (S : Shape) (T : Tensor) (ht : T.traceFree) (i : Fin 3) :
    T.diagonal i = S.s i • radialCoordinate S T - difference S.s i • secondCoordinate S T := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.radialCoordinate, OAI.PositiveEinsteinFour.Bianchi.difference, OAI.PositiveEinsteinFour.Bianchi.secondCoordinate
def OAI.PositiveEinsteinFour.Bianchi.thirdCoordinate line 247
Source documentation
The final free coordinate is the common residual in the three off-diagonal quaternion coordinates.
```
def thirdCoordinate (S : Shape) (T : Tensor) : Vec :=
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.Vec
theorem OAI.PositiveEinsteinFour.Bianchi.thirdCoordinate_eq line 252
Source documentation
More transparent defining expression for the third coordinate.
```
theorem thirdCoordinate_eq (S : Shape) (T : Tensor) :
    thirdCoordinate S T = T.auxiliary 0 - S.s 0 • secondCoordinate S T -
      (difference S.s 0 / 3) • radialCoordinate S T := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.thirdCoordinate, OAI.PositiveEinsteinFour.Bianchi.secondCoordinate, OAI.PositiveEinsteinFour.Bianchi.difference, OAI.PositiveEinsteinFour.Bianchi.radialCoordinate
theorem OAI.PositiveEinsteinFour.Bianchi.thirdCoordinate_parameters line 258
theorem OAI.PositiveEinsteinFour.Bianchi.parameters_reconstruction line 266
Source documentation
A quaternionic Bianchi tensor is exactly the explicit parameter tensor; this also gives uniqueness by the three coordinate recovery identities.
```
theorem parameters_reconstruction (S : Shape) (T : Tensor)
    (ht : T.traceFree) (hb : T.bianchi) :
    parameters S (radialCoordinate S T) (secondCoordinate S T) (thirdCoordinate S T) = T := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.parameters, OAI.PositiveEinsteinFour.Bianchi.radialCoordinate, OAI.PositiveEinsteinFour.Bianchi.secondCoordinate, OAI.PositiveEinsteinFour.Bianchi.thirdCoordinate
def OAI.PositiveEinsteinFour.Bianchi.Tensor.squaredNorm line 319
Source documentation
Squared Hilbert--Schmidt norm of the symmetric vector-valued matrix.
```
def Tensor.squaredNorm (T : Tensor) : ℝ := ∑ i, ∑ j, ‖T.matrix i j‖ ^ 2
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor
theorem OAI.PositiveEinsteinFour.Bianchi.Tensor.squaredNorm_eq line 321
theorem OAI.PositiveEinsteinFour.Bianchi.sum_norm_two line 326
theorem OAI.PositiveEinsteinFour.Bianchi.sum_norm_three line 334
theorem OAI.PositiveEinsteinFour.Bianchi.parameters_diagonal_energy line 343
theorem OAI.PositiveEinsteinFour.Bianchi.parameters_off_energy line 350
theorem OAI.PositiveEinsteinFour.Bianchi.parameters_energy line 372
Source documentation
The exact energy identity in (2), including the multiplicity of the symmetric off-diagonal entries.
```
theorem parameters_energy (S : Shape) (p k l : Vec) :
    (parameters S p k l).squaredNorm / 6 =
      (5 / 3) * ‖p‖ ^ 2 + 5 * ‖k‖ ^ 2 + ‖l‖ ^ 2 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.parameters
theorem OAI.PositiveEinsteinFour.Bianchi.refined_kato line 380
Source documentation
The refined Kato inequality follows from the full parametrization for every symmetric tensor satisfying the actual Bianchi constraint.
```
theorem refined_kato (S : Shape) (T : Tensor) (ht : T.traceFree) (hb : T.bianchi) :
    (5 / 3) * ‖radialCoordinate S T‖ ^ 2 ≤ T.squaredNorm / 6 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.radialCoordinate