HighestGram.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The Casimir lower bound with arbitrary symmetric matrix coefficients. Positive semidefiniteness is applied to each actual tensor coordinate.

def OAI.PositiveEinsteinFour.HighestHessian.hessianGram line 17
Source documentation
The matrix-weighted Gram form of three actual Hessian arrays.
```
def hessianGram (A : Mat) (F : Fin 3 → Hessian) : ℝ :=
…
```
theorem OAI.PositiveEinsteinFour.HighestHessian.hessianGram_nonneg line 22
Source documentation
A positive semidefinite coefficient matrix gives a nonnegative Gram form on the entire four-slot tensor space.
```
theorem hessianGram_nonneg (A : Mat) (hA : A.PosSemidef) (F : Fin 3 → Hessian) :
    0 ≤ hessianGram A F := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.hessianGram
theorem OAI.PositiveEinsteinFour.HighestHessian.hessianGram_shift line 52
Source documentation
Adding a scalar identity adds that scalar times the total energy.
```
theorem hessianGram_shift (A : Mat) (x : ℝ) (F : Fin 3 → Hessian) :
    hessianGram (A + x • (1 : Mat)) F =
      hessianGram A F + x * ∑ r, hessianNormSq (F r) := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.hessianGram
def OAI.PositiveEinsteinFour.HighestHessian.generalCasimirCurvatureForm line 61
Source documentation
The same local Casimir expression accepts complete Weyl matrices.
```
def generalCasimirCurvatureForm (A U : Mat) (X : Hessian) : ℝ :=
…
```
theorem OAI.PositiveEinsteinFour.HighestHessian.generalCasimirCurvatureForm_lower line 67
Source documentation
The sharp lower constant follows from the two proved Casimir energies and positive semidefinite shifted Weyl matrices; no eigenframe is used.
```
theorem generalCasimirCurvatureForm_lower (A U : Mat) (X : Hessian)
    (hX : condition X) (x y : ℝ)
    (hA : (A + x • (1 : Mat)).PosSemidef)
    (hU : (U + y • (1 : Mat)).PosSemidef) :
    (4 - 2 * x - 2 * y) * hessianNormSq X ≤ generalCasimirCurvatureForm A U X := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.condition, OAI.PositiveEinsteinFour.HighestHessian.generalCasimirCurvatureForm
theorem OAI.PositiveEinsteinFour.HighestHessian.generalCasimirCurvatureForm_nonneg line 84
Source documentation
Positivity includes the closed sectional boundary.
```
theorem generalCasimirCurvatureForm_nonneg (A U : Mat) (X : Hessian)
    (hX : condition X) (x y : ℝ)
    (hA : (A + x • (1 : Mat)).PosSemidef)
    (hU : (U + y • (1 : Mat)).PosSemidef) (hxy : x + y ≤ 2) :
    0 ≤ generalCasimirCurvatureForm A U X := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.condition, OAI.PositiveEinsteinFour.HighestHessian.generalCasimirCurvatureForm