DirichletMatrix.lean`

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Finite block matrices for the Jacobi determinant approximation.

abbrev OAI.PositiveEinsteinFour.Jacobi.NormalMatrix line 15
def OAI.PositiveEinsteinFour.Jacobi.blockAt line 18
Source documentation
The normal-space matrix at one pair of mesh nodes.
```
def blockAt {N : ℕ} (M : Matrix (Fin 3 × Fin N) (Fin 3 × Fin N) ℝ)
    (i j : Fin N) : NormalMatrix := fun a b => M (a, i) (b, j)
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix
theorem OAI.PositiveEinsteinFour.Jacobi.blockAt_mul line 21
theorem OAI.PositiveEinsteinFour.Jacobi.blockAt_transpose line 28
theorem OAI.PositiveEinsteinFour.Jacobi.blockAt_diagonal line 32
theorem OAI.PositiveEinsteinFour.Jacobi.blockAt_mul_diagonal line 40
theorem OAI.PositiveEinsteinFour.Jacobi.blockDiagonal_quadratic line 48
theorem OAI.PositiveEinsteinFour.Jacobi.blockDiagonal_posDef line 58
Source documentation
Positive pivots give a positive block-diagonal form.
```
theorem blockDiagonal_posDef {N : ℕ} {S : Fin N → NormalMatrix}
    (hS : ∀ i, (S i).PosDef) : (Matrix.blockDiagonal S).PosDef := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix
def OAI.PositiveEinsteinFour.Jacobi.lowerBidiagonal line 80
Source documentation
A unit lower bidiagonal matrix, with arbitrary noncommuting blocks.
```
def lowerBidiagonal {N : ℕ} (A : Fin N → NormalMatrix) :
    Matrix (Fin 3 × Fin N) (Fin 3 × Fin N) ℝ := fun i j =>
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix
theorem OAI.PositiveEinsteinFour.Jacobi.lowerBidiagonal_triangular line 85
def OAI.PositiveEinsteinFour.Jacobi.nodeBlockEquiv line 93
theorem OAI.PositiveEinsteinFour.Jacobi.lowerBidiagonal_block_det line 102
theorem OAI.PositiveEinsteinFour.Jacobi.bidiagonal_factorization_block line 116
Source documentation
The block formula used to recover the tridiagonal matrix from its pivots. No products at different times have been interchanged.
```
theorem bidiagonal_factorization_block {N : ℕ} (A S : Fin N → NormalMatrix)
    (i j : Fin N) :
    blockAt (lowerBidiagonal A * Matrix.blockDiagonal S * (lowerBidiagonal A).transpose)
      i j = ∑ k, blockAt (lowerBidiagonal A) i k * S k *
        (blockAt (lowerBidiagonal A) j k).transpose := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.blockAt, OAI.PositiveEinsteinFour.Jacobi.lowerBidiagonal
theorem OAI.PositiveEinsteinFour.Jacobi.det_lowerBidiagonal line 125
Source documentation
Elimination by these factors never changes a block determinant.
```
theorem det_lowerBidiagonal {N : ℕ} (A : Fin N → NormalMatrix) :
    (lowerBidiagonal A).det = 1 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.lowerBidiagonal
theorem OAI.PositiveEinsteinFour.Jacobi.det_bidiagonal_factorization line 132
Source documentation
The determinant of an L D Lᵀ factorization is the product of the three-dimensional pivots, with their original order retained.
```
theorem det_bidiagonal_factorization {N : ℕ} (A S : Fin N → NormalMatrix) :
    (lowerBidiagonal A * Matrix.blockDiagonal S * (lowerBidiagonal A).transpose).det =
      ∏ i, (S i).det := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.lowerBidiagonal
theorem OAI.PositiveEinsteinFour.Jacobi.bidiagonal_factorization_posDef line 140
Source documentation
Positive pivots give a positive discrete Jacobi form after the unit triangular change of variables.
```
theorem bidiagonal_factorization_posDef {N : ℕ} (A S : Fin N → NormalMatrix)
    (hS : ∀ i, (S i).PosDef) :
    (lowerBidiagonal A * Matrix.blockDiagonal S * (lowerBidiagonal A).transpose).PosDef := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.lowerBidiagonal
theorem OAI.PositiveEinsteinFour.Jacobi.jacobi_pivot_recurrence line 153
Source documentation
The Jacobi recurrence is exactly the Schur-complement recurrence. The order of the factors follows from right division by the Jacobi matrix.
```
theorem jacobi_pivot_recurrence {Yprev Y Ynext D : NormalMatrix}
    (hprev : IsUnit Yprev.det) (hY : IsUnit Y.det)
    (hrec : Ynext = D * Y - Yprev) :
    Ynext * Y⁻¹ = D - (Y * Yprev⁻¹)⁻¹ := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix
theorem OAI.PositiveEinsteinFour.Jacobi.determinant_pivot_product line 163
Source documentation
The ordered Schur pivots telescope at the determinant level even when successive Jacobi matrices do not commute.
```
theorem determinant_pivot_product (Y : ℕ → NormalMatrix) (n : ℕ)
    (hY : ∀ i ≤ n, (Y i).det ≠ 0) :
    (∏ i ∈ Finset.range n, (Y (i + 1) * (Y i)⁻¹).det) =
      (Y n).det / (Y 0).det := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix