HighestProjection.lean`

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

The orthogonal projection is constructed from the actual tensor subspace.

abbrev OAI.PositiveEinsteinFour.HighestHessian.HessianSpace line 17
def OAI.PositiveEinsteinFour.HighestHessian.hessianVector line 19
def OAI.PositiveEinsteinFour.HighestHessian.vectorHessian line 21
theorem OAI.PositiveEinsteinFour.HighestHessian.vectorHessian_hessianVector line 23
theorem OAI.PositiveEinsteinFour.HighestHessian.hessianVector_vectorHessian line 26
theorem OAI.PositiveEinsteinFour.HighestHessian.hessianVector_injective line 32
theorem OAI.PositiveEinsteinFour.HighestHessian.hessianVector_inner line 36
def OAI.PositiveEinsteinFour.HighestHessian.highestLinearMap line 43
Source documentation
The explicit twenty-one-coordinate map, regarded as a linear map into the Euclidean space of all four-slot tensors.
```
def highestLinearMap : (Fin 21 → ℝ) →ₗ[ℝ] HessianSpace where
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.HessianSpace
def OAI.PositiveEinsteinFour.HighestHessian.highestSubspace line 58
def OAI.PositiveEinsteinFour.HighestHessian.highestProjection line 61
Source documentation
The actual orthogonal projection onto the symmetry/trace/Bianchi subspace.
```
def highestProjection (X : Hessian) : Hessian :=
…
```
theorem OAI.PositiveEinsteinFour.HighestHessian.highestProjection_has_coordinates line 64
theorem OAI.PositiveEinsteinFour.HighestHessian.highestProjection_condition line 73
theorem OAI.PositiveEinsteinFour.HighestHessian.highestSubspace_mem line 78
theorem OAI.PositiveEinsteinFour.HighestHessian.highestProjection_pairing_right line 84
Source documentation
Orthogonality is with respect to the original tensor Frobenius pairing.
```
theorem highestProjection_pairing_right (X Y : Hessian) (hY : condition Y) :
    hessianPairing (highestProjection X) Y = hessianPairing X Y := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.condition, OAI.PositiveEinsteinFour.HighestHessian.highestProjection
theorem OAI.PositiveEinsteinFour.HighestHessian.highestProjection_pairing_left line 94
theorem OAI.PositiveEinsteinFour.HighestHessian.highestProjection_norm_split line 99
theorem OAI.PositiveEinsteinFour.HighestHessian.highestProjection_norm_le line 108
theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_condition line 117
theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_condition line 123
theorem OAI.PositiveEinsteinFour.HighestHessian.plusProjection_pairing line 129
theorem OAI.PositiveEinsteinFour.HighestHessian.minusProjection_pairing line 138
theorem OAI.PositiveEinsteinFour.HighestHessian.curvaturePairing_highestProjection line 148
Source documentation
The mixed curvature term retains the whole unsymmetrized weight tensor.
```
theorem curvaturePairing_highestProjection (t u : Fin 3 → ℝ)
    (X L : Hessian) (hX : condition X) :
    curvaturePairing t u X (highestProjection L) = curvaturePairing t u X L := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.condition, OAI.PositiveEinsteinFour.HighestHessian.curvaturePairing, OAI.PositiveEinsteinFour.HighestHessian.highestProjection
theorem OAI.PositiveEinsteinFour.HighestHessian.weighted_highestProjection_square line 156
Source documentation
The weighted square with a constructed projection, without a projected tensor or a projection identity among its hypotheses.
```
theorem weighted_highestProjection_square (X L : Hessian) (hX : condition X)
    (t u : Fin 3 → ℝ) (x y m : ℝ) (hm : 0 < m)
    (ht : ∀ s, -x ≤ t s) (hu : ∀ s, -y ≤ u s) (hxy : x + y ≤ 2) :
    0 ≤ (m / 6) * curvaturePairing t u X X + curvaturePairing t u X L / 6 +
      curvaturePairing t u (highestProjection L) (highestProjection L) / (24 * m) := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.condition, OAI.PositiveEinsteinFour.HighestHessian.curvaturePairing, OAI.PositiveEinsteinFour.HighestHessian.highestProjection
def OAI.PositiveEinsteinFour.HighestHessian.weightTensor line 166
Source documentation
The unsymmetrized weight derivative tensor dm ⊗ ∇T.
```
def weightTensor (a : Vec) (Z : Tensor) : Hessian :=
…
```
theorem OAI.PositiveEinsteinFour.HighestHessian.weightTensor_norm line 169