LDL.diag_eq_lowerInv_conj
theorem LDL.diag_eq_lowerInv_conj :
∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : LinearOrder n]
[inst_2 : IsWellOrder n fun x x_1 => x < x_1] [inst_3 : LocallyFiniteOrderBot n] {S : Matrix n n 𝕜}
[inst_4 : Fintype n] (hS : S.PosDef), LDL.diag hS = LDL.lowerInv hS * S * (LDL.lowerInv hS).conjTranspose
This theorem states that for any positive definite matrix `S` over a ring `𝕜` with a characteristic of real or complex numbers, indexed by a well-ordered type `n`, the diagonal matrix `D` in the LDL decomposition of `S` can be obtained by conjugating `S` with the inverse of the lower triangular matrix `L` in the decomposition. The conjugation is done as `L⁻¹ * S * (L⁻¹)ᵀ`, where `L⁻¹` is the inverse of `L`, and `(L⁻¹)ᵀ` is its complex conjugate transpose. In other words, the diagonal of the LDL decomposition is equal to this conjugated product.
More concisely: For any positive definite matrix `S` over a ring with real or complex numbers and indexed by a well-ordered type `n`, the diagonal matrix in its LDL decomposition is equal to the conjugated product of `S` and the inverse of its lower triangular matrix `L`, i.e., `(L⁻¹ * S * (L⁻¹)ᵀ)`.
|
LDL.lower_conj_diag
theorem LDL.lower_conj_diag :
∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : LinearOrder n]
[inst_2 : IsWellOrder n fun x x_1 => x < x_1] [inst_3 : LocallyFiniteOrderBot n] {S : Matrix n n 𝕜}
[inst_4 : Fintype n] (hS : S.PosDef), LDL.lower hS * LDL.diag hS * (LDL.lower hS).conjTranspose = S
The theorem **LDL Decomposition** states that any positive definite matrix `S` can be decomposed as `S = LDLᴴ`, where `L` is a lower-triangular matrix and `D` is a diagonal matrix. Specifically, for any given type `𝕜` which is a ring-like structure, a type `n` possessing linear order, well order, and a locally finite order bot, along with a matrix `S` of dimensions `n x n` with elements in `𝕜` and a finite type `n`, if `S` is positive definite, then the product of `L` (the lower triangular matrix from the LDL decomposition), `D` (the diagonal matrix from the LDL decomposition), and the conjugate transpose of `L`, is equal to `S`.
More concisely: Given a positive definite matrix `S` of dimensions `n x n` over a ring-like structure `𝕜` with `n` being a type possessing linear order, well order, and locally finite order bot, `S` can be decomposed as `LDLᴴ` where `L` is lower-triangular and `D` is diagonal, such that `S = LDLᴴ`.
|