JacobiSchemeMatrix.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Identifying the concrete Jacobi recurrence with the finite curvature matrix.

theorem OAI.PositiveEinsteinFour.Jacobi.scalarLift_sub_diagonal line 15
theorem OAI.PositiveEinsteinFour.Jacobi.curvatureDirichlet_eq line 31

theorem OAI.PositiveEinsteinFour.Jacobi.curvatureDirichlet_determinant line 41

Source documentation

All diagonal blocks of the discrete Jacobi recurrence are the actual curvature blocks. This identity includes the time-index shift.

theorem curvatureDirichlet_determinant {N : ℕ} {t : ℝ} (ht : t ≠ 0)
    (R : ℕ → NormalMatrix)
    (hsym : ∀ i, (R i).transpose = R i)
    (hunit : ∀ i, 1 ≤ i → i ≤ N + 1 →
      IsUnit (normalizedDiscrete R (t / (N + 1)) i).det) :
    (curvatureDirichlet t (fun i : Fin N => R (i.val + 1) - 1)).det =
      (normalizedDiscrete R (t / (N + 1)) (N + 1)).det := by
…

Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.normalizedDiscrete, OAI.PositiveEinsteinFour.Jacobi.curvatureDirichlet