HighestCurvature.lean`

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The original derivative-slot curvature form on the highest tensors.

def OAI.PositiveEinsteinFour.HighestHessian.derivativeSlotForm line 15
Source documentation
Twice the diagonal curvature-block contribution on the derivative slots.
```
def derivativeSlotForm (s : Fin 3) (X : Hessian) : ℝ :=
…
```
def OAI.PositiveEinsteinFour.HighestHessian.matrixSlotForm line 20
Source documentation
The coefficient of the diagonal matrix-slot curvature form.
```
def matrixSlotForm (s : Fin 3) (X : Hessian) : ℝ :=
…
```
theorem OAI.PositiveEinsteinFour.HighestHessian.curvature_identity_zero line 23
theorem OAI.PositiveEinsteinFour.HighestHessian.curvature_identity_one line 33
theorem OAI.PositiveEinsteinFour.HighestHessian.curvature_identity_two line 43
theorem OAI.PositiveEinsteinFour.HighestHessian.curvature_form_identity line 54
Source documentation
Exact curvature compression, derived from the constrained coordinates.
```
theorem curvature_form_identity (c : Fin 21 → ℝ) (t : Fin 3 → ℝ)
    (ht : ∑ s, t s = 0) :
    (1 / 2 : ℝ) * ∑ s, t s * derivativeSlotForm s (highest c) +
      2 * ∑ s, t s * matrixSlotForm s (highest c) =
        -(∑ s, t s * hessianNormSq (totalPlus s (highest c))) / 20 := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.derivativeSlotForm, OAI.PositiveEinsteinFour.HighestHessian.highest, OAI.PositiveEinsteinFour.HighestHessian.matrixSlotForm, OAI.PositiveEinsteinFour.HighestHessian.totalPlus
def OAI.PositiveEinsteinFour.HighestHessian.originalPlusCurvatureForm line 67
Source documentation
The original plus part 4 − (5/6)T_D − (5/3)B_F(T).
```
def originalPlusCurvatureForm (t : Fin 3 → ℝ) (X : Hessian) : ℝ :=
…
```
theorem OAI.PositiveEinsteinFour.HighestHessian.originalPlusCurvatureForm_eq line 73
Source documentation
Exact identification of the original plus curvature form with its total rotation expression; no representation-theoretic premise is used.
```
theorem originalPlusCurvatureForm_eq (c : Fin 21 → ℝ) (t : Fin 3 → ℝ)
    (ht : ∑ s, t s = 0) :
    originalPlusCurvatureForm t (highest c) = 4 * hessianNormSq (highest c) +
      (∑ s, t s * hessianNormSq (totalPlus s (highest c))) / 24 := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.originalPlusCurvatureForm, OAI.PositiveEinsteinFour.HighestHessian.highest, OAI.PositiveEinsteinFour.HighestHessian.totalPlus
def OAI.PositiveEinsteinFour.HighestHessian.casimirCurvatureForm line 82
Source documentation
The quadratic form after the two exact Casimir normalizations.
```
def casimirCurvatureForm (t u : Fin 3 → ℝ) (X : Hessian) : ℝ :=
…
```
theorem OAI.PositiveEinsteinFour.HighestHessian.casimirCurvatureForm_lower line 88
Source documentation
Sectional spectral bounds give the sharp coercive constant.
```
theorem casimirCurvatureForm_lower (c : Fin 21 → ℝ) (t u : Fin 3 → ℝ)
    (x y : ℝ) (ht : ∀ s, -x ≤ t s) (hu : ∀ s, -y ≤ u s) :
    (4 - 2 * x - 2 * y) * hessianNormSq (highest c) ≤
      casimirCurvatureForm t u (highest c) := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.highest, OAI.PositiveEinsteinFour.HighestHessian.casimirCurvatureForm
theorem OAI.PositiveEinsteinFour.HighestHessian.casimirCurvatureForm_nonneg line 98
Source documentation
Positivity on the whole closed sectional domain, including its boundary.
```
theorem casimirCurvatureForm_nonneg (c : Fin 21 → ℝ) (t u : Fin 3 → ℝ)
    (x y : ℝ) (ht : ∀ s, -x ≤ t s) (hu : ∀ s, -y ≤ u s)
    (hxy : x + y ≤ 2) : 0 ≤ casimirCurvatureForm t u (highest c) := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.casimirCurvatureForm, OAI.PositiveEinsteinFour.HighestHessian.highest
theorem OAI.PositiveEinsteinFour.HighestHessian.originalPlusCurvatureForm_eq_of_condition line 111
Source documentation
The original-form identity for any tensor satisfying the actual local symmetry, trace and Bianchi constraints.
```
theorem originalPlusCurvatureForm_eq_of_condition (X : Hessian) (hX : condition X)
    (t : Fin 3 → ℝ) (ht : ∑ s, t s = 0) :
    originalPlusCurvatureForm t X = 4 * hessianNormSq X +
      (∑ s, t s * hessianNormSq (totalPlus s X)) / 24 := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.condition, OAI.PositiveEinsteinFour.HighestHessian.originalPlusCurvatureForm, OAI.PositiveEinsteinFour.HighestHessian.totalPlus
theorem OAI.PositiveEinsteinFour.HighestHessian.casimirCurvatureForm_nonneg_of_condition line 118