Jacobi.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The scalar determinant loss in the radial comparison, using the three eigenvalues of the averaged normal Jacobi curvature matrix.

def OAI.PositiveEinsteinFour.Jacobi.loss line 12
def OAI.PositiveEinsteinFour.Jacobi.lossFactor line 14
theorem OAI.PositiveEinsteinFour.Jacobi.loss_identity line 16
theorem OAI.PositiveEinsteinFour.Jacobi.loss_one_negative line 23
theorem OAI.PositiveEinsteinFour.Jacobi.other_eigenvalues_nonneg line 56
theorem OAI.PositiveEinsteinFour.Jacobi.preconjugate_loss line 74
Source documentation
The full determinant-loss bound before the first conjugate point. The semidefinite compression is expressed by β*a, β*b, β*c ≤ 1. No positive definiteness or inversion at its singular endpoint is required.
```
theorem preconjugate_loss {β a b c : ℝ}
    (hβ : 0 ≤ β) (htrace : a + b + c = 0)
    (ha : -1 ≤ a) (hb : -1 ≤ b) (hc : -1 ≤ c)
    (hβa : β * a ≤ 1) (hβb : β * b ≤ 1) (hβc : β * c ≤ 1) :
    lossFactor β / 6 * (a ^ 2 + b ^ 2 + c ^ 2) ≤ loss β a b c := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.lossFactor, OAI.PositiveEinsteinFour.Jacobi.loss

theorem OAI.PositiveEinsteinFour.Jacobi.norm_sq_le_six line 116

Source documentation

The eigenvalue box and trace condition give the global squared-norm cap.

theorem norm_sq_le_six {a b c : ℝ} (htrace : a + b + c = 0)
    (ha : a ∈ Set.Icc (-1 : ℝ) 2) (hb : b ∈ Set.Icc (-1 : ℝ) 2)
    (hc : c ∈ Set.Icc (-1 : ℝ) 2) : a ^ 2 + b ^ 2 + c ^ 2 ≤ 6 := by
…

theorem OAI.PositiveEinsteinFour.Jacobi.postconjugate_loss line 126

Source documentation

After conjugacy the truncated determinant is zero, and the same bound follows from the norm cap.

theorem postconjugate_loss {β a b c : ℝ}
    (htrace : a + b + c = 0)
    (ha : a ∈ Set.Icc (-1 : ℝ) 2) (hb : b ∈ Set.Icc (-1 : ℝ) 2)
    (hc : c ∈ Set.Icc (-1 : ℝ) 2) :
    lossFactor β / 6 * (a ^ 2 + b ^ 2 + c ^ 2) ≤ 1 := by
…

Mentions: OAI.PositiveEinsteinFour.Jacobi.lossFactor