Matrix.det_fromBlocks₂₂
theorem Matrix.det_fromBlocks₂₂ :
∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
[inst_3 : DecidableEq n] [inst_4 : CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α)
(D : Matrix n n α) [inst_5 : Invertible D], (A.fromBlocks B C D).det = D.det * (A - B * ⅟D * C).det
This theorem, `Matrix.det_fromBlocks₂₂`, describes the determinant of a 2x2 block matrix which is formulated in terms of the Schur complement. More precisely, given a commutative ring `α`, types `m` and `n` indexed by `Fintype`, and a matrix `D` in `α` that is invertible, for any matrices `A` in `Matrix m m α`, `B` in `Matrix m n α`, and `C` in `Matrix n m α`, the determinant of the block matrix formed from `A`, `B`, `C`, and `D` is equal to the determinant of `D` times the determinant of the difference between `A` and the product of `B`, the reciprocal of `D`, and `C`. The equality and finiteness of `m` and `n` are decided by `DecidableEq m` and `DecidableEq n` respectively.
More concisely: Given a commutative ring `α`, two finite types `m` and `n`, an invertible matrix `D` in `α`, and matrices `A`, `B`, and `C` of sizes `m x m`, `m x n`, and `n x m` respectively, the determinant of the block matrix `[ A B ] [ C^T D ]` is equal to the determinant of `D` times the determinant of `A - B * D^(-1) * C^T`.
|
Matrix.det_fromBlocks₁₁
theorem Matrix.det_fromBlocks₁₁ :
∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
[inst_3 : DecidableEq n] [inst_4 : CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α)
(D : Matrix n n α) [inst_5 : Invertible A], (A.fromBlocks B C D).det = A.det * (D - C * ⅟A * B).det
The theorem `Matrix.det_fromBlocks₁₁` states that for any given types `m`, `n` and `α`, where `α` forms a commutative ring, `m` and `n` have finite types and decidable equality, if we have a block matrix formed by matrices `A`, `B`, `C`, and `D` such that `A` is invertible, then the determinant of the block matrix is equal to the product of the determinant of `A` and the determinant of the Schur complement `D - C * ⅟A * B`.
In other words, this theorem offers a formula for calculating the determinant of a 2×2 block matrix, which has an invertible top left element, in terms of the Schur complement. This approach is often used in linear algebra when dealing with large matrices, where it simplifies the calculation of the determinant.
More concisely: Given matrices A, B, C, and D of compatible sizes with A invertible, the determinant of the block matrix [A | B; C | D] equals the product of the determinant of A and the determinant of D - C * A⁻¹ * B.
|
Matrix.det_mul_add_one_comm
theorem Matrix.det_mul_add_one_comm :
∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
[inst_3 : DecidableEq n] [inst_4 : CommRing α] (A : Matrix m n α) (B : Matrix n m α),
(A * B + 1).det = (B * A + 1).det
This is an alternate statement of the Weinstein–Aronszajn identity for matrices. Given two matrices, `A` of type `Matrix m n α` and `B` of type `Matrix n m α` where `α` denotes a commutative ring, `m` and `n` are types with finite number of elements and decidable equality, the determinant of the matrix resulting from multiplying `A` by `B` and adding the identity matrix is equal to the determinant of the matrix resulting from multiplying `B` by `A` and adding the identity matrix. This theorem asserts the commutativity of this specific matrix operation.
More concisely: For matrices A of size m x n and B of size n x m over a commutative ring α with finite number of elements and decidable equality, the determinant of (A * B + I) is equal to the determinant of (B * A + I), where I denotes the identity matrix.
|
Matrix.isUnit_fromBlocks_iff_of_invertible₂₂
theorem Matrix.isUnit_fromBlocks_iff_of_invertible₂₂ :
∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
[inst_3 : DecidableEq n] [inst_4 : CommRing α] {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α}
{D : Matrix n n α} [inst_5 : Invertible D], IsUnit (A.fromBlocks B C D) ↔ IsUnit (A - B * ⅟D * C)
This theorem states that for any matrices `A`, `B`, `C`, and `D` over a commutative ring α, with `A` and `D` being square matrices indexed by finite types `m` and `n` respectively, and `B` and `C` being rectangular matrices, if the bottom-right block matrix `D` is invertible, then the entire block matrix formed by `A`, `B`, `C`, and `D` is invertible if and only if the Schur complement of `D` in the block matrix, given by `A - B * ⅟D * C`, is invertible. In other words, the invertibility of the whole block matrix is equivalent to the invertibility of the Schur complement when the bottom-right block is invertible.
More concisely: For matrices A, B, C, and D over a commutative ring, if square matrices A and D are of finite sizes m and n, respectively, and rectangular matrices B and C have compatible sizes, then the block matrix [A | B | C] [T| D] is invertible if and only if D is invertible and the Schur complement A - B * D^(-1) * C is invertible.
|
Matrix.inv_fromBlocks_zero₁₂_of_isUnit_iff
theorem Matrix.inv_fromBlocks_zero₁₂_of_isUnit_iff :
∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
[inst_3 : DecidableEq n] [inst_4 : CommRing α] (A : Matrix m m α) (C : Matrix n m α) (D : Matrix n n α),
(IsUnit A ↔ IsUnit D) → (A.fromBlocks 0 C D)⁻¹ = A⁻¹.fromBlocks 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
This theorem describes the inverse of a lower block-triangular matrix under certain conditions. Specifically, given any finite types `m` and `n`, and any commutative ring `α`, for matrices `A` of type `Matrix m m α`, `C` of type `Matrix n m α`, and `D` of type `Matrix n n α`, if either both `A` and `D` are units (i.e., they both have inverses) or neither of them is a unit, then the inverse of the block matrix formed from `A`, `C`, and `D` (with a zero block in the upper right) is equal to the block matrix formed from the inverses of `A` and `D`, with a particular expression involving `C`, `D`, and `A` in the lower left block and zero in the upper right block.
More concisely: Given matrices `A` of size `m x m`, `C` of size `n x m`, `D` of size `n x n`, all over a commutative ring `α`, if either both `A` and `D` are invertible or neither is, then the inverse of the block matrix `[ A | 0 ] [ C D ]` is equal to `[ A^{-1} | 0 ] [ D^{-1} -C*D^{-1}*A^{-1} ]`.
|
Matrix.det_add_col_mul_row
theorem Matrix.det_add_col_mul_row :
∀ {m : Type u_2} {α : Type u_4} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : CommRing α]
{A : Matrix m m α},
IsUnit A.det →
∀ (u v : m → α), (A + Matrix.col u * Matrix.row v).det = A.det * (1 + Matrix.row v * A⁻¹ * Matrix.col u).det
This theorem, referred to as the Matrix Determinant Lemma, states that for any given type `m` and a type `α` forming a commutative ring, given a square matrix `A` of type `α` with rows and columns indexed by `m`, and if the determinant of `A` has a multiplicative inverse (i.e., `A.det` is a unit), then for any two vectors `u` and `v` (functions from `m` to `α`), the determinant of the matrix obtained by adding `A` and the matrix formed by the product of column matrix `u` and row matrix `v` equals the product of `A.det` and the determinant of `1 + (row matrix `v` times the inverse of `A` times column matrix `u`).
This theorem essentially gives us a formula to calculate the determinant of the resulting matrix when a rank-one update (addition of the product of a column vector and a row vector) is performed on a square matrix whose determinant is a unit.
More concisely: If `A` is a square matrix over a commutative ring with determinant `det(A)` being a unit, then `det(A + u v^T) = det(A) * det(I + v A^-1 u^T)`, where `u` and `v` are column vectors, and `I` is the identity matrix.
|
Matrix.fromBlocks_eq_of_invertible₂₂
theorem Matrix.fromBlocks_eq_of_invertible₂₂ :
∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype l] [inst_1 : Fintype m]
[inst_2 : Fintype n] [inst_3 : DecidableEq l] [inst_4 : DecidableEq m] [inst_5 : DecidableEq n]
[inst_6 : CommRing α] (A : Matrix l m α) (B : Matrix l n α) (C : Matrix n m α) (D : Matrix n n α)
[inst_7 : Invertible D],
A.fromBlocks B C D =
Matrix.fromBlocks 1 (B * ⅟D) 0 1 * (A - B * ⅟D * C).fromBlocks 0 0 D * Matrix.fromBlocks 1 0 (⅟D * C) 1
This theorem states that for any types `l`, `m`, `n`, and `α` where `α` is a commutative ring and `l`, `m`, `n` are types with decidable equality and finite instances, given matrices `A` of type `Matrix l m α`, `B` of type `Matrix l n α`, `C` of type `Matrix n m α`, `D` of type `Matrix n n α` such that `D` is invertible, the matrix formed by these matrices arranged in a block matrix form is equal to the product of three matrices.
The first matrix is a block matrix with the diagonal blocks being identity matrices and upper right block being `B * ⅟D`. The second matrix is a block matrix with the diagonal blocks being `A - B * ⅟D * C` and `D`, and zeros elsewhere. The third matrix is a block matrix with the diagonal blocks being identity matrices and the lower left block being `⅟D * C`. Here, `⅟D` represents the inverse of `D`.
This theorem is essentially a statement of the LDU decomposition for block matrices where the last block on the diagonal (bottom-right corner) is invertible. The decomposition is done using the Schur complement.
More concisely: Given commutative ring `α`, matrices `A` of size `l x m`, `B` of size `l x n`, `C` of size `n x m`, and `D` of size `n x n` over `α` with `D` invertible, the block matrix formed by `[I | B * ⁅D⁅; (A - B * ⁅D⁅ * C) | D; ⁅D⁅ * C | I]` is equal to `[I | B * ⁅D⁅; zero | ⁅D⁅ * C] * [I | ⁅I⁅; -⁅D⁅⁻¹ * C | I] * [I | ⁅I⁅; -⁅C⁅⁻¹ * D | I]`.
|
Matrix.fromBlocks_eq_of_invertible₁₁
theorem Matrix.fromBlocks_eq_of_invertible₁₁ :
∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype l] [inst_1 : Fintype m]
[inst_2 : Fintype n] [inst_3 : DecidableEq l] [inst_4 : DecidableEq m] [inst_5 : DecidableEq n]
[inst_6 : CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix l m α) (D : Matrix l n α)
[inst_7 : Invertible A],
A.fromBlocks B C D =
Matrix.fromBlocks 1 0 (C * ⅟A) 1 * A.fromBlocks 0 0 (D - C * ⅟A * B) * Matrix.fromBlocks 1 (⅟A * B) 0 1
This theorem describes the LDU decomposition of a block matrix with an invertible top-left corner, using the Schur complement. Specifically, it states that for any types `l`, `m`, `n`, and `α` where `l`, `m`, and `n` have a finite number of elements and decidable equality, and `α` forms a commutative ring, given matrices `A`, `B`, `C`, and `D` with appropriate dimensions, if `A` is invertible, then the block matrix formed by `A`, `B`, `C`, and `D` equals the product of three matrices. The first matrix is a block matrix with 1's on the diagonal, `C * ⅟A` in the bottom-left block, and zeros elsewhere. The second matrix is a block matrix with `A` in the top-left block, `D - C * ⅟A * B` in the bottom-right block, and zeros elsewhere. The third matrix is a block matrix with 1's on the diagonal, `⅟A * B` in the top-right block, and zeros elsewhere.
More concisely: Given matrices `A` of size `l x l`, `B` of size `l x m`, `C` of size `m x n`, and `D` of size `n x n`, if `A` is invertible, then `[A ~| B; C ~| D] = [I_l ~| C * ⅟A ~| 0; A * ⅟(D - C * ⅟A * B) ~| I_n * ⅟A * B] * [I_l + B * ⅟(D - C * ⅟A * B) * B^T ~| 0; 0 ~| I_n]`, where `I_l` and `I_n` are identity matrices of sizes `l x l` and `n x n` respectively.
|
Matrix.det_add_mul
theorem Matrix.det_add_mul :
∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
[inst_3 : DecidableEq n] [inst_4 : CommRing α] {A : Matrix m m α} (U : Matrix m n α) (V : Matrix n m α),
IsUnit A.det → (A + U * V).det = A.det * (1 + V * A⁻¹ * U).det
This theorem is a generalization of the Matrix determinant lemma. It states that for any types `m`, `n`, and `α` where `m` and `n` are finite types with decidable equality, and `α` is a type with a commutative ring structure, given a matrix `A` of type `Matrix m m α`, and matrices `U` and `V` of type `Matrix m n α` and `Matrix n m α` respectively, if the determinant of `A` is a unit (i.e., has a multiplicative inverse), then the determinant of the sum of `A` and the product of `U` and `V` is equal to the product of the determinant of `A` and the determinant of `1` plus the product of `V`, the inverse of `A`, and `U`. In mathematical notation: if $\det(A)$ is a unit, then $\det(A + UV) = \det(A) \cdot \det(1 + VA^{-1}U)$.
More concisely: If `A` is a square matrix of size `m x m` over a commutative ring `α` with decidable equality and determinant `det(A)` is a unit, then `det(A + UV) = det(A) * det(1 + VA⁻¹U)`.
|
Matrix.isUnit_fromBlocks_zero₂₁
theorem Matrix.isUnit_fromBlocks_zero₂₁ :
∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
[inst_3 : DecidableEq n] [inst_4 : CommRing α] {A : Matrix m m α} {B : Matrix m n α} {D : Matrix n n α},
IsUnit (A.fromBlocks B 0 D) ↔ IsUnit A ∧ IsUnit D
This theorem states that for any types `m`, `n`, and `α` with `α` being a commutative ring, `m` and `n` being finite types with decidable equality, and given matrices `A` of type `Matrix m m α`, `B` of type `Matrix m n α`, and `D` of type `Matrix n n α`, the block matrix obtained from `A`, `B`, `0`, and `D` is unit (i.e., has an inverse) if and only if both `A` and `D` are units. Here, the block matrix is upper triangular, meaning that the blocks `B` and `0` are above and below the diagonal, respectively.
More concisely: Given matrices A of size m x m over a commutative ring α with decisable equality, B of size m x n, and D of size n x n, the block matrix [A | B; B^T | D] is unit if and only if both A and D are units.
|
Matrix.det_one_add_col_mul_row
theorem Matrix.det_one_add_col_mul_row :
∀ {m : Type u_2} {α : Type u_4} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : CommRing α] (u v : m → α),
(1 + Matrix.col u * Matrix.row v).det = 1 + Matrix.dotProduct v u
The theorem `Matrix.det_one_add_col_mul_row` is a specific instance of the Matrix determinant lemma, where the matrix `A` is the identity matrix. It states that for any types `m` and `α`, where `m` is a finite type with decidable equality and `α` is a commutative ring, given any two functions `u` and `v` from `m` to `α`, the determinant of the matrix resulting from adding 1 to the product of a column matrix from `u` and a row matrix from `v` is equal to 1 plus the dot product of `v` and `u`. In mathematical terms, this is equivalent to saying that det(I + uv^T) = 1 + v.u, where I is the identity matrix, v and u are vectors, and uv^T denotes the outer product of u and v.
More concisely: The determinant of the matrix obtained by adding the outer product of two vectors to the identity matrix is equal to 1 plus the dot product of the vectors.
|
Matrix.isUnit_fromBlocks_zero₁₂
theorem Matrix.isUnit_fromBlocks_zero₁₂ :
∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
[inst_3 : DecidableEq n] [inst_4 : CommRing α] {A : Matrix m m α} {C : Matrix n m α} {D : Matrix n n α},
IsUnit (A.fromBlocks 0 C D) ↔ IsUnit A ∧ IsUnit D
The theorem `Matrix.isUnit_fromBlocks_zero₁₂` states that a lower block-triangular matrix is invertible if and only if both elements of its diagonal are invertible. Here, the matrix is defined over a commutative ring, the rows and columns are indexed by some finite types `m` and `n`, and the matrix is broken down into blocks `A`, `C`, and `D`. `A` is the top left block, `D` is the bottom right block, and `0` and `C` are the top right and bottom left blocks, respectively. In this case, the top right block is a zero matrix.
More concisely: A lower block-triangular matrix over a commutative ring with size `m x n`, where the top right block is a zero matrix, is invertible if and only if the diagonal elements `A[i,i]` and `D[j,j]` for `i in 1 to min m n` and `j in min (m - i + 1) to n` are invertible.
|
Matrix.inv_fromBlocks_zero₂₁_of_isUnit_iff
theorem Matrix.inv_fromBlocks_zero₂₁_of_isUnit_iff :
∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
[inst_3 : DecidableEq n] [inst_4 : CommRing α] (A : Matrix m m α) (B : Matrix m n α) (D : Matrix n n α),
(IsUnit A ↔ IsUnit D) → (A.fromBlocks B 0 D)⁻¹ = A⁻¹.fromBlocks (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹
The theorem `Matrix.inv_fromBlocks_zero₂₁_of_isUnit_iff` states that for any types `m`, `n`, and `α`, given a finite `m` (`Fintype m`), a finite `n` (`Fintype n`), decidable equality on `m` (`DecidableEq m`) and `n` (`DecidableEq n`), and a commutative ring `α` (`CommRing α`), for any matrices `A` of type `Matrix m m α`, `B` of type `Matrix m n α`, and `D` of type `Matrix n n α`, if `A` is a unit if and only if `D` is a unit (`IsUnit A ↔ IsUnit D`), then the inverse of the upper block-triangular matrix formed by `A`, `B`, and `D` with `B` in the upper right block and `D` in the bottom right block, is equal to the upper block-triangular matrix formed by the inverse of `A`, the negated product of the inverses of `A`, `B`, and `D`, and the inverse of `D`, with the negated product in the upper right block.
More concisely: If matrices `A` of size `m x m`, `B` of size `m x n`, and `D` of size `n x n` over a commutative ring `α` have equal inverses (`IsUnit A ↔ IsUnit D`) then the inverse of the upper block-triangular matrix formed by `A`, `B`, and `D` is equal to the upper block-triangular matrix formed by the inverse of `A`, the negated product of the inverses of `A`, `B`, and `D`, and the inverse of `D`, with the negated product in the upper right block.
|
Matrix.det_one_add_mul_comm
theorem Matrix.det_one_add_mul_comm :
∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
[inst_3 : DecidableEq n] [inst_4 : CommRing α] (A : Matrix m n α) (B : Matrix n m α),
(1 + A * B).det = (1 + B * A).det
The Weinstein–Aronszajn identity states that for any two matrices `A` and `B`, where `A` is of shape `m`x`n` and `B` is of shape `n`x`m`, and the entries of the matrices are from a commutative ring, the determinant of the sum of the identity matrix of shape `m`x`m` and the product of `A` and `B` is equal to the determinant of the sum of the identity matrix of shape `n`x`n` and the product of `B` and `A`. The equality holds regardless of the order of multiplication in the sum. The identity matrix on the left-hand side is of shape `m`x`m` while the identity matrix on the right-hand side is of shape `n`x`n`.
More concisely: The determinant of the sum of the identity matrix of shape `m`x`m` and the product of matrices `A` of shape `m`x`n` and `B` of shape `n`x`m`, where the entries come from a commutative ring, equals the determinant of the sum of the identity matrix of shape `n`x`n` and the product of matrices `B` and `A`.
|
Matrix.isUnit_fromBlocks_iff_of_invertible₁₁
theorem Matrix.isUnit_fromBlocks_iff_of_invertible₁₁ :
∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
[inst_3 : DecidableEq n] [inst_4 : CommRing α] {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α}
{D : Matrix n n α} [inst_5 : Invertible A], IsUnit (A.fromBlocks B C D) ↔ IsUnit (D - C * ⅟A * B)
This theorem establishes a condition for the invertibility of a block matrix in terms of the Schur complement of the matrix. More specifically, it states that for any given types `m`, `n`, and `α`, given that `m` and `n` have finite types and decidable equality, and `α` forms a commutative ring, then for any given block matrix composed of matrices `A`, `B`, `C`, and `D`, if the top-left matrix `A` is invertible, then the entire block matrix is invertible if and only if the Schur complement, `D - C * ⅟A * B`, is also invertible.
Note: Here, `A.fromBlocks B C D` is the block matrix defined in Lean 4 whose blocks are the matrices `A`, `B`, `C`, and `D`. The Schur complement of a block matrix is a derived matrix obtained by subtracting the product of the 'off-diagonal' blocks from the bottom-right block, after scaling one of the off-diagonal blocks by the inverse of the top-left block.
More concisely: Given matrices A, B, C, and D of compatible sizes over a commutative ring α with finite types and decidable equality, if A is invertible then the block matrix [A | B; C | D] is invertible if and only if the Schur complement D - C * A⁻¹ * B is invertible.
|