FiniteRadialComparison.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The finite determinant comparison before the mesh limit.

theorem OAI.PositiveEinsteinFour.Jacobi.det_scalarLift line 14
theorem OAI.PositiveEinsteinFour.Jacobi.det_normalized_matrix line 21
Source documentation
Normalizing by a scalar comparison matrix divides the determinant by the cube of its scalar determinant.
```
theorem det_normalized_matrix {N : ℕ}
    (G L : Matrix (Fin N) (Fin N) ℝ)
    (K : Matrix (Fin 3 × Fin N) (Fin 3 × Fin N) ℝ) (hG : G * L * G = 1) :
    (scalarLift G * K * scalarLift G).det = K.det / L.det ^ 3 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.scalarLift

theorem OAI.PositiveEinsteinFour.Jacobi.finite_normalized_radial_comparison line 42

Source documentation

The first scalar mode bounds the determinant of the normalized Jacobi matrix. Positivity and the scalar eigenmode are explicit here; the orthogonal completion and complementary trace estimate are proved.

theorem finite_normalized_radial_comparison {N : ℕ} (hN : 0 < N)
    (G L : Matrix (Fin N) (Fin N) ℝ) (A : Fin N → NormalMatrix)
    (w : Fin N → ℝ) (a g : ℝ)
    (hw : ∑ i, w i ^ 2 = 1) (hGsymm : Gᵀ = G) (hG : G * L * G = 1)
    (heigen : G *ᵥ w = g • w) (hA : ∀ i, (A i).trace = 0)
    (hpos : (scalarLift G * (scalarLift L - a ^ 2 • Matrix.blockDiagonal A) *
      scalarLift G).PosDef) :
    (scalarLift G * (scalarLift L - a ^ 2 • Matrix.blockDiagonal A) * scalarLift G).det ≤
      ((1 : NormalMatrix) - (a * g) ^ 2 • (∑ i, w i ^ 2 • A i)).det := by
…

Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.scalarLift