MinusProjectionCost.lean`

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The sharp anti-self-dual upper cost on actual derivative tensors.

def OAI.PositiveEinsteinFour.HighestHessian.rightTwist line 16
Source documentation
Simultaneous right-quaternion action on the two derivative slots.
```
def rightTwist (s : Fin 3) (X : Hessian) : Hessian := fun i j a b =>
…
```
def OAI.PositiveEinsteinFour.HighestHessian.rightSector line 20
Source documentation
The four orthogonal sectors of the two real quaternion slots.
```
def rightSector (r : Fin 4) (X : Hessian) : Hessian := fun i j a b =>
…
```
theorem OAI.PositiveEinsteinFour.HighestHessian.rightSector_partition_slice line 26
theorem OAI.PositiveEinsteinFour.HighestHessian.rightSector_partition line 33
Source documentation
The sector squared norms sum to the actual tensor squared norm.
```
theorem rightSector_partition (X : Hessian) :
    (∑ r : Fin 4, hessianNormSq (rightSector r X)) = hessianNormSq X := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.rightSector
theorem OAI.PositiveEinsteinFour.HighestHessian.rightSector_twist_slice_0 line 44
theorem OAI.PositiveEinsteinFour.HighestHessian.rightSector_twist_slice_1 line 53
theorem OAI.PositiveEinsteinFour.HighestHessian.rightSector_twist_slice_2 line 62
theorem OAI.PositiveEinsteinFour.HighestHessian.rightSector_twist_slice line 71
theorem OAI.PositiveEinsteinFour.HighestHessian.rightDerivativeSlotForm_sector line 83
Source documentation
Exact simultaneous spectral decomposition, proved from the real matrices.
```
theorem rightDerivativeSlotForm_sector (s : Fin 3) (X : Hessian) :
    rightDerivativeSlotForm s X = 2 * hessianNormSq (rightSector 0 X) +
      2 * hessianNormSq (rightSector s.succ X) - hessianNormSq X := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.rightDerivativeSlotForm, OAI.PositiveEinsteinFour.HighestHessian.rightSector
theorem OAI.PositiveEinsteinFour.HighestHessian.minusDerivativeCurvatureForm_sector line 96
Source documentation
The anti-self-dual form is a weighted sum of the three nontrivial sectors.
```
theorem minusDerivativeCurvatureForm_sector (u : Fin 3 → ℝ)
    (hu : ∑ s, u s = 0) (X : Hessian) :
    minusDerivativeCurvatureForm u X =
      ∑ s, u s * hessianNormSq (rightSector s.succ X) := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.minusDerivativeCurvatureForm, OAI.PositiveEinsteinFour.HighestHessian.rightSector
theorem OAI.PositiveEinsteinFour.HighestHessian.minusDerivativeCurvatureForm_lower line 107
Source documentation
The sharp cost has coefficient one, including all boundary cases.
```
theorem minusDerivativeCurvatureForm_lower (u : Fin 3 → ℝ)
    (hu : ∑ s, u s = 0) (y : ℝ) (hy : 0 ≤ y)
    (huy : ∀ s, -y ≤ u s) (X : Hessian) :
    -y * hessianNormSq X ≤ minusDerivativeCurvatureForm u X := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.minusDerivativeCurvatureForm
theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_energy_le line 130
Source documentation
The full two-derivative space has minus Casimir energy at most eight.
```
theorem totalMinus_energy_le (X : Hessian) :
    (∑ s : Fin 3, hessianNormSq (totalMinus s X)) ≤ 8 * hessianNormSq X := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.totalMinus
theorem OAI.PositiveEinsteinFour.HighestHessian.curvaturePairing_nonneg_of_plus_energy line 146
Source documentation
A full-space coercive estimate whenever the plus energy is the already computed spin-three value; the minus estimate requires no type assumption.
```
theorem curvaturePairing_nonneg_of_plus_energy
    (t u : Fin 3 → ℝ) (x y : ℝ) (X : Hessian)
    (ht : ∀ s, -x ≤ t s) (hu : ∀ s, -y ≤ u s)
    (hy : 0 ≤ y) (hxy : x + y ≤ 2)
    (hplus : (∑ s : Fin 3, hessianNormSq (totalPlus s X)) = 48 * hessianNormSq X) :
    0 ≤ curvaturePairing t u X X := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.totalPlus, OAI.PositiveEinsteinFour.HighestHessian.curvaturePairing