Matrix decompositions and linear systems

Factorizations of matrices (singular value, polar, Schur and LU decompositions), Gaussian elimination and the solvability of linear systems, iterative methods and condition numbers.

• Condition numbers of sign matrices
• Conjugate gradient method
• Gaussian elimination and row echelon form
• LU decomposition
• Singular value decomposition
• Polar decomposition

TheoremConvergence of the Jacobi method for strictly diagonally dominant matrices#●ready to prove

Let \(A\) be a real square matrix with rows and columns indexed by a finite type, and let \(b\) be a real vector. Suppose \(A\) is strictly diagonally dominant: \(\sum_{j \ne i} |A_{ij}| < |A_{ii}|\) for every \(i\). Define the Jacobi sweep \(J\) by \(J(x)_i = \bigl(b_i - \sum_{j \ne i} A_{ij} x_j\bigr) / A_{ii}\). Then there is a vector \(x^*\) with \(A x^* = b\) such that, for every starting vector \(x_0\), the iterates \(J^k(x_0)\) converge to \(x^*\) as \(k \to \infty\).

public theorem_wanted jacobi_iteration_converges
    (A : Matrix n n ℝ) (b : n → ℝ)
    (hA : ∀ i, ∑ j ∈ Finset.univ.erase i, |A i j| < |A i i|) :
    ∃ xStar : n → ℝ, A.mulVec xStar = b ∧ ∀ x₀ : n → ℝ,
      Filter.Tendsto
        (fun k =>
          (fun x : n → ℝ => fun i => (b i - ∑ j ∈ Finset.univ.erase i, A i j * x j) / A i i)^[k]
            x₀)
        Filter.atTop (𝓝 xStar)

Sources

• G. H. Golub and C. F. Van Loan, Matrix Computations, 4th ed., Johns Hopkins Univ. Press, 2013, §11.2; https://en.wikipedia.org/wiki/Jacobi_method

TheoremRouché–Capelli theorem#✓fully proved

Let \(K\) be a field, let \(m\) be a set and \(n\) a finite set, let \(A\) be an \(m \times n\) matrix over \(K\), and let \(b \in K^m\). Then the linear system \(Ax = b\) has a solution \(x \in K^n\) if and only if the rank of \(A\) equals the rank of the augmented matrix \((A \mid b)\), whose columns are the columns of \(A\) followed by the single column \(b\).

Proof: Following the column-space argument in Wikipedia, Rouché–Capelli theorem, "Proof", solvability is membership of \(b\) in the column span, which we compare before and after adjoining \(b\).

theorem rouche_capelli {m n : Type*} [Fintype n] {K : Type*} [Field K]
    (A : Matrix m n K) (b : m → K) :
    (∃ x : n → K, A *ᵥ x = b) ↔
      A.rank =
        (Matrix.of (fun i => Sum.elim (A i) (fun _ : Fin 1 => b i)) :
          Matrix m (n ⊕ Fin 1) K).rank

Sources

• https://en.wikipedia.org/wiki/Rouch%C3%A9%E2%80%93Capelli_theorem.

TheoremSchur decomposition of a complex square matrix#✓fully proved

Let \(A\) be a square complex matrix whose rows and columns are indexed by a finite linearly ordered type \(n\). Then there are a unitary matrix \(U\), with conjugate transpose \(U^*\), and a matrix \(T\) that is upper triangular with respect to the order on \(n\) (that is, \(T_{ij} = 0\) whenever \(j < i\)) such that \(A = U T U^*\).

theorem exists_unitaryGroup_isUpperTriangular (A : Matrix n n ℂ) :
    ∃ (U : Matrix.unitaryGroup n ℂ) (T : Matrix n n ℂ),
      T.IsUpperTriangular ∧ A = (U : Matrix n n ℂ) * T * star (U : Matrix n n ℂ)

Sources

• I. Schur, Uber charakteristische Wurzeln, Math. Ann. 66 (1909), 488-510, DOI 10.1007/BF01450045.

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.