OAI/Geometry/EinsteinFour/JacobiPivots.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The finite Dirichlet determinant is the determinant of the discrete Jacobi solution, on the nonsingular range used before conjugacy.

  1. def OAI.PositiveEinsteinFour.Jacobi.jacobiPivot line 14
  2. theorem OAI.PositiveEinsteinFour.Jacobi.jacobiPivot_symmetric line 18
  3. theorem OAI.PositiveEinsteinFour.Jacobi.jacobiPivot_eq_ratio line 26
  4. theorem OAI.PositiveEinsteinFour.Jacobi.predecessor_sum_zero line 39
  5. theorem OAI.PositiveEinsteinFour.Jacobi.predecessor_sum_succ line 42
  6. theorem OAI.PositiveEinsteinFour.Jacobi.pivotDiagonal_jacobiPivot line 59
  7. theorem OAI.PositiveEinsteinFour.Jacobi.dirichlet_determinant_eq_jacobi line 72

    Source documentation

    The determinant identity required for the preconjugate comparison. The hypotheses on Y are its recurrence and nonsingularity.

    theorem dirichlet_determinant_eq_jacobi (D Y : ℕ → NormalMatrix) (N : ℕ)
    (hD : ∀ i, (D i).transpose = D i)
    (h0 : Y 0 = 0) (h1 : Y 1 = 1)
    (hrec : ∀ i, Y (i + 2) = D i * Y (i + 1) - Y i)
    (hunit : ∀ i, 1 ≤ i → i ≤ N + 1 → IsUnit (Y i).det) :
    (dirichletMatrix (fun i : Fin N => D i.val)).det = (Y (N + 1)).det := by
…

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