JacobiDirichletPositivity.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Positive Jacobi pivot ratios give the actual finite curvature matrix.

theorem OAI.PositiveEinsteinFour.Jacobi.curvatureDirichlet_posDef_of_ratios line 16

Source documentation

The positive ratios are the ordered Schur pivots of the concrete curvature Dirichlet matrix. No commutation between time samples is used.

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

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