HighestMinusForm.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Identification of the actual anti-self-dual derivative curvature term.

def OAI.PositiveEinsteinFour.HighestHessian.rightDerivativeSlotForm line 15
Source documentation
The uncontracted right-quaternion curvature on the two derivative slots.
```
def rightDerivativeSlotForm (s : Fin 3) (X : Hessian) : ℝ :=
…
```
theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_slice_square line 19
theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_square line 28
Source documentation
A single generator square is the actual derivative curvature contraction. This identity holds on the full tensor space, before imposing Bianchi.
```
theorem totalMinus_square (s : Fin 3) (X : Hessian) :
    hessianNormSq (totalMinus s X) =
      2 * hessianNormSq X - 2 * rightDerivativeSlotForm s X := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.totalMinus, OAI.PositiveEinsteinFour.HighestHessian.rightDerivativeSlotForm
def OAI.PositiveEinsteinFour.HighestHessian.minusDerivativeCurvatureForm line 36
Source documentation
The anti-self-dual curvature term, with the normalization of equation (11).
```
def minusDerivativeCurvatureForm (u : Fin 3 → ℝ) (X : Hessian) : ℝ :=
…
```
theorem OAI.PositiveEinsteinFour.HighestHessian.minusDerivativeCurvatureForm_eq line 39
def OAI.PositiveEinsteinFour.HighestHessian.originalCurvatureForm line 49
Source documentation
The complete original curvature form on an actual four-slot tensor.
```
def originalCurvatureForm (t u : Fin 3 → ℝ) (X : Hessian) : ℝ :=
…
```
theorem OAI.PositiveEinsteinFour.HighestHessian.originalCurvatureForm_eq line 53
Source documentation
Both curvature contractions agree exactly with the computed total actions.
```
theorem originalCurvatureForm_eq (X : Hessian) (hX : condition X)
    (t u : Fin 3 → ℝ) (ht : ∑ s, t s = 0) (hu : ∑ s, u s = 0) :
    originalCurvatureForm t u X = casimirCurvatureForm t u X := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.condition, OAI.PositiveEinsteinFour.HighestHessian.originalCurvatureForm, OAI.PositiveEinsteinFour.HighestHessian.casimirCurvatureForm

theorem OAI.PositiveEinsteinFour.HighestHessian.originalCurvatureForm_nonneg line 62

Source documentation

Positivity of the tensor curvature form.

theorem originalCurvatureForm_nonneg (X : Hessian) (hX : condition X)
    (t u : Fin 3 → ℝ) (ht : ∑ s, t s = 0) (hu : ∑ s, u s = 0)
    (x y : ℝ) (htx : ∀ s, -x ≤ t s) (huy : ∀ s, -y ≤ u s)
    (hxy : x + y ≤ 2) : 0 ≤ originalCurvatureForm t u X := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.condition, OAI.PositiveEinsteinFour.HighestHessian.originalCurvatureForm

theorem OAI.PositiveEinsteinFour.HighestHessian.originalCurvatureForm_lower line 70

Source documentation

The precise coercive constant is retained, for use before integration.

theorem originalCurvatureForm_lower (X : Hessian) (hX : condition X)
    (t u : Fin 3 → ℝ) (ht : ∑ s, t s = 0) (hu : ∑ s, u s = 0)
    (x y : ℝ) (htx : ∀ s, -x ≤ t s) (huy : ∀ s, -y ≤ u s) :
    (4 - 2 * x - 2 * y) * hessianNormSq X ≤ originalCurvatureForm t u X := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.condition, OAI.PositiveEinsteinFour.HighestHessian.originalCurvatureForm