DirichletFactorization.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The tridiagonal Jacobi matrix and its ordered Schur pivots.

def OAI.PositiveEinsteinFour.Jacobi.dirichletMatrix line 14
Source documentation
The Dirichlet matrix with diagonal blocks D and both off-diagonals -1.
```
def dirichletMatrix {N : ℕ} (D : Fin N → NormalMatrix) :
    Matrix (Fin 3 × Fin N) (Fin 3 × Fin N) ℝ := fun i j =>
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix
def OAI.PositiveEinsteinFour.Jacobi.pivotDiagonal line 22
Source documentation
The diagonal determined by the pivots. The predecessor sum has at most one term; its use also covers the first node without a separate convention.
```
def pivotDiagonal {N : ℕ} (S : Fin N → NormalMatrix) (i : Fin N) : NormalMatrix :=
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix
theorem OAI.PositiveEinsteinFour.Jacobi.blockAt_lower line 25
theorem OAI.PositiveEinsteinFour.Jacobi.blockAt_dirichlet line 33
theorem OAI.PositiveEinsteinFour.Jacobi.pivot_left_block line 42
theorem OAI.PositiveEinsteinFour.Jacobi.pivot_right_block line 53
theorem OAI.PositiveEinsteinFour.Jacobi.pivot_summand line 64

theorem OAI.PositiveEinsteinFour.Jacobi.pivot_factorization_blocks line 77

Source documentation

The precise block formula before the predecessor sums are collapsed.

theorem pivot_factorization_blocks {N : ℕ} (S : Fin N → NormalMatrix)
    (hunit : ∀ k, IsUnit (S k).det) (hsym : ∀ k, (S k).transpose = S k)
    (i j : Fin N) :
    blockAt (lowerBidiagonal (fun k => -(S k)⁻¹) * Matrix.blockDiagonal S *
      (lowerBidiagonal (fun k => -(S k)⁻¹)).transpose) i j =
    (∑ k, if i = k ∧ j = k then S k else 0) +
      (∑ k, if i = k ∧ k.val + 1 = j.val then -1 else 0) +
      (∑ k, if j = k ∧ k.val + 1 = i.val then -1 else 0) +
      (∑ k, if k.val + 1 = i.val ∧ k.val + 1 = j.val then (S k)⁻¹ else 0) := by
…

Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.blockAt, OAI.PositiveEinsteinFour.Jacobi.lowerBidiagonal

theorem OAI.PositiveEinsteinFour.Jacobi.pivot_sum_collapse line 90
theorem OAI.PositiveEinsteinFour.Jacobi.dirichlet_pivot_factorization line 118
Source documentation
The full tridiagonal matrix is the L D Lᵀ factorization of its Schur pivots, with neither time ordering nor matrix multiplication commuted.
```
theorem dirichlet_pivot_factorization {N : ℕ} (S : Fin N → NormalMatrix)
    (hunit : ∀ k, IsUnit (S k).det) (hsym : ∀ k, (S k).transpose = S k) :
    dirichletMatrix (pivotDiagonal S) =
      lowerBidiagonal (fun k => -(S k)⁻¹) * Matrix.blockDiagonal S *
        (lowerBidiagonal (fun k => -(S k)⁻¹)).transpose := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.dirichletMatrix, OAI.PositiveEinsteinFour.Jacobi.pivotDiagonal, OAI.PositiveEinsteinFour.Jacobi.lowerBidiagonal
theorem OAI.PositiveEinsteinFour.Jacobi.det_dirichlet_pivots line 131
theorem OAI.PositiveEinsteinFour.Jacobi.dirichlet_pivots_posDef line 136