2×2 block matrices and the Schur complement #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file proves properties of 2×2 block matrices [A B; C D] that relate to the Schur complement
D - C⬝A⁻¹⬝B.
Some of the results here generalize to 2×2 matrices in a category, rather than just a ring. A few
results in this direction can be found in the the file cateogry_theory.preadditive.biproducts,
especially the declarations category_theory.biprod.gaussian and category_theory.biprod.iso_elim.
Compare with matrix.invertible_of_from_blocks₁₁_invertible.
Main results #
matrix.det_from_blocks₁₁,matrix.det_from_blocks₂₂: determinant of a block matrix in terms of the Schur complement.matrix.inv_of_from_blocks_zero₂₁_eq,matrix.inv_of_from_blocks_zero₁₂_eq: the inverse of a block triangular matrix.matrix.is_unit_from_blocks_zero₂₁,matrix.is_unit_from_blocks_zero₁₂: invertibility of a block triangular matrix.matrix.det_one_add_mul_comm: the Weinstein–Aronszajn identity.matrix.schur_complement_pos_semidef_iff: If a matrixAis positive definite, then[A B; Bᴴ D]is postive semidefinite if and only ifD - Bᴴ A⁻¹ Bis postive semidefinite.
theorem
matrix.from_blocks_eq_of_invertible₁₁
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype l]
[fintype m]
[fintype n]
[decidable_eq l]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
(A : matrix m m α)
(B : matrix m n α)
(C : matrix l m α)
(D : matrix l n α)
[invertible A] :
matrix.from_blocks A B C D = ((matrix.from_blocks 1 0 (C.mul (⅟ A)) 1).mul (matrix.from_blocks A 0 0 (D - (C.mul (⅟ A)).mul B))).mul (matrix.from_blocks 1 ((⅟ A).mul B) 0 1)
LDU decomposition of a block matrix with an invertible top-left corner, using the Schur complement.
theorem
matrix.from_blocks_eq_of_invertible₂₂
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype l]
[fintype m]
[fintype n]
[decidable_eq l]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
(A : matrix l m α)
(B : matrix l n α)
(C : matrix n m α)
(D : matrix n n α)
[invertible D] :
matrix.from_blocks A B C D = ((matrix.from_blocks 1 (B.mul (⅟ D)) 0 1).mul (matrix.from_blocks (A - (B.mul (⅟ D)).mul C) 0 0 D)).mul (matrix.from_blocks 1 0 ((⅟ D).mul C) 1)
LDU decomposition of a block matrix with an invertible bottom-right corner, using the Schur complement.
Block triangular matrices #
def
matrix.from_blocks_zero₂₁_invertible
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
(A : matrix m m α)
(B : matrix m n α)
(D : matrix n n α)
[invertible A]
[invertible D] :
invertible (matrix.from_blocks A B 0 D)
An upper-block-triangular matrix is invertible if its diagonal is.
Equations
- A.from_blocks_zero₂₁_invertible B D = (matrix.from_blocks A B 0 D).invertible_of_left_inverse (matrix.from_blocks (⅟ A) (-((⅟ A).mul B).mul (⅟ D)) 0 (⅟ D)) _
def
matrix.from_blocks_zero₁₂_invertible
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
(A : matrix m m α)
(C : matrix n m α)
(D : matrix n n α)
[invertible A]
[invertible D] :
invertible (matrix.from_blocks A 0 C D)
A lower-block-triangular matrix is invertible if its diagonal is.
Equations
- A.from_blocks_zero₁₂_invertible C D = (matrix.from_blocks A 0 C D).invertible_of_left_inverse (matrix.from_blocks (⅟ A) 0 (-((⅟ D).mul C).mul (⅟ A)) (⅟ D)) _
theorem
matrix.inv_of_from_blocks_zero₂₁_eq
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
(A : matrix m m α)
(B : matrix m n α)
(D : matrix n n α)
[invertible A]
[invertible D]
[invertible (matrix.from_blocks A B 0 D)] :
theorem
matrix.inv_of_from_blocks_zero₁₂_eq
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
(A : matrix m m α)
(C : matrix n m α)
(D : matrix n n α)
[invertible A]
[invertible D]
[invertible (matrix.from_blocks A 0 C D)] :
def
matrix.invertible_of_from_blocks_zero₂₁_invertible
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
(A : matrix m m α)
(B : matrix m n α)
(D : matrix n n α)
[invertible (matrix.from_blocks A B 0 D)] :
invertible A × invertible D
Both diagonal entries of an invertible upper-block-triangular matrix are invertible (by reading off the diagonal entries of the inverse).
Equations
- A.invertible_of_from_blocks_zero₂₁_invertible B D = (A.invertible_of_left_inverse (⅟ (matrix.from_blocks A B 0 D)).to_blocks₁₁ _, D.invertible_of_right_inverse (⅟ (matrix.from_blocks A B 0 D)).to_blocks₂₂ _)
def
matrix.invertible_of_from_blocks_zero₁₂_invertible
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
(A : matrix m m α)
(C : matrix n m α)
(D : matrix n n α)
[invertible (matrix.from_blocks A 0 C D)] :
invertible A × invertible D
Both diagonal entries of an invertible lower-block-triangular matrix are invertible (by reading off the diagonal entries of the inverse).
Equations
- A.invertible_of_from_blocks_zero₁₂_invertible C D = (A.invertible_of_right_inverse (⅟ (matrix.from_blocks A 0 C D)).to_blocks₁₁ _, D.invertible_of_left_inverse (⅟ (matrix.from_blocks A 0 C D)).to_blocks₂₂ _)
def
matrix.from_blocks_zero₂₁_invertible_equiv
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
(A : matrix m m α)
(B : matrix m n α)
(D : matrix n n α) :
invertible (matrix.from_blocks A B 0 D) ≃ invertible A × invertible D
invertible_of_from_blocks_zero₂₁_invertible and from_blocks_zero₂₁_invertible form
an equivalence.
Equations
- A.from_blocks_zero₂₁_invertible_equiv B D = {to_fun := λ (_x : invertible (matrix.from_blocks A B 0 D)), A.invertible_of_from_blocks_zero₂₁_invertible B D, inv_fun := λ (i : invertible A × invertible D), let _inst : invertible A := i.fst, _inst_1 : invertible D := i.snd in A.from_blocks_zero₂₁_invertible B D, left_inv := _, right_inv := _}
def
matrix.from_blocks_zero₁₂_invertible_equiv
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
(A : matrix m m α)
(C : matrix n m α)
(D : matrix n n α) :
invertible (matrix.from_blocks A 0 C D) ≃ invertible A × invertible D
invertible_of_from_blocks_zero₁₂_invertible and from_blocks_zero₁₂_invertible form
an equivalence.
Equations
- A.from_blocks_zero₁₂_invertible_equiv C D = {to_fun := λ (_x : invertible (matrix.from_blocks A 0 C D)), A.invertible_of_from_blocks_zero₁₂_invertible C D, inv_fun := λ (i : invertible A × invertible D), let _inst : invertible A := i.fst, _inst_1 : invertible D := i.snd in A.from_blocks_zero₁₂_invertible C D, left_inv := _, right_inv := _}
@[simp]
theorem
matrix.is_unit_from_blocks_zero₂₁
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
{A : matrix m m α}
{B : matrix m n α}
{D : matrix n n α} :
An upper block-triangular matrix is invertible iff both elements of its diagonal are.
This is a propositional form of matrix.from_blocks_zero₂₁_invertible_equiv.
@[simp]
theorem
matrix.is_unit_from_blocks_zero₁₂
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
{A : matrix m m α}
{C : matrix n m α}
{D : matrix n n α} :
A lower block-triangular matrix is invertible iff both elements of its diagonal are.
This is a propositional form of matrix.from_blocks_zero₁₂_invertible_equiv forms an iff.
theorem
matrix.inv_from_blocks_zero₂₁_of_is_unit_iff
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
(A : matrix m m α)
(B : matrix m n α)
(D : matrix n n α)
(hAD : is_unit A ↔ is_unit D) :
An expression for the inverse of an upper block-triangular matrix, when either both elements of diagonal are invertible, or both are not.
theorem
matrix.inv_from_blocks_zero₁₂_of_is_unit_iff
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
(A : matrix m m α)
(C : matrix n m α)
(D : matrix n n α)
(hAD : is_unit A ↔ is_unit D) :
An expression for the inverse of a lower block-triangular matrix, when either both elements of diagonal are invertible, or both are not.
2×2 block matrices #
General 2×2 block matrices #
def
matrix.from_blocks₂₂_invertible
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
(A : matrix m m α)
(B : matrix m n α)
(C : matrix n m α)
(D : matrix n n α)
[invertible D]
[invertible (A - (B.mul (⅟ D)).mul C)] :
invertible (matrix.from_blocks A B C D)
A block matrix is invertible if the bottom right corner and the corresponding schur complement is.
Equations
- A.from_blocks₂₂_invertible B C D = (let _inst : invertible 1 := invertible_one, _inst_1 : invertible 1 := invertible_one in ((1.from_blocks_zero₂₁_invertible (B.mul (⅟ D)) 1).matrix_mul ((A - (B.mul (⅟ D)).mul C).from_blocks_zero₂₁_invertible 0 D)).matrix_mul (1.from_blocks_zero₁₂_invertible ((⅟ D).mul C) 1)).copy' (matrix.from_blocks A B C D) (matrix.from_blocks (⅟ (A - (B.mul (⅟ D)).mul C)) (-((⅟ (A - (B.mul (⅟ D)).mul C)).mul B).mul (⅟ D)) (-((⅟ D).mul C).mul (⅟ (A - (B.mul (⅟ D)).mul C))) (⅟ D + ((((⅟ D).mul C).mul (⅟ (A - (B.mul (⅟ D)).mul C))).mul B).mul (⅟ D))) _ _
def
matrix.from_blocks₁₁_invertible
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
(A : matrix m m α)
(B : matrix m n α)
(C : matrix n m α)
(D : matrix n n α)
[invertible A]
[invertible (D - (C.mul (⅟ A)).mul B)] :
invertible (matrix.from_blocks A B C D)
A block matrix is invertible if the top left corner and the corresponding schur complement is.
Equations
- A.from_blocks₁₁_invertible B C D = let _inst : invertible (matrix.from_blocks D C B A) := D.from_blocks₂₂_invertible C B A, iDCBA : invertible ((matrix.from_blocks D C B A).submatrix ⇑(equiv.sum_comm m n) ⇑(equiv.sum_comm m n)) := (matrix.from_blocks D C B A).submatrix_equiv_invertible (equiv.sum_comm m n) (equiv.sum_comm m n) in iDCBA.copy' (matrix.from_blocks A B C D) (matrix.from_blocks (⅟ A + ((((⅟ A).mul B).mul (⅟ (D - (C.mul (⅟ A)).mul B))).mul C).mul (⅟ A)) (-((⅟ A).mul B).mul (⅟ (D - (C.mul (⅟ A)).mul B))) (-((⅟ (D - (C.mul (⅟ A)).mul B)).mul C).mul (⅟ A)) (⅟ (D - (C.mul (⅟ A)).mul B))) _ _
theorem
matrix.inv_of_from_blocks₂₂_eq
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
(A : matrix m m α)
(B : matrix m n α)
(C : matrix n m α)
(D : matrix n n α)
[invertible D]
[invertible (A - (B.mul (⅟ D)).mul C)]
[invertible (matrix.from_blocks A B C D)] :
theorem
matrix.inv_of_from_blocks₁₁_eq
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
(A : matrix m m α)
(B : matrix m n α)
(C : matrix n m α)
(D : matrix n n α)
[invertible A]
[invertible (D - (C.mul (⅟ A)).mul B)]
[invertible (matrix.from_blocks A B C D)] :
def
matrix.invertible_of_from_blocks₂₂_invertible
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
(A : matrix m m α)
(B : matrix m n α)
(C : matrix n m α)
(D : matrix n n α)
[invertible D]
[invertible (matrix.from_blocks A B C D)] :
invertible (A - (B.mul (⅟ D)).mul C)
If a block matrix is invertible and so is its bottom left element, then so is the corresponding Schur complement.
Equations
- A.invertible_of_from_blocks₂₂_invertible B C D = ((A - (B.mul (⅟ D)).mul C).invertible_of_from_blocks_zero₁₂_invertible 0 D).fst
def
matrix.invertible_of_from_blocks₁₁_invertible
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
(A : matrix m m α)
(B : matrix m n α)
(C : matrix n m α)
(D : matrix n n α)
[invertible A]
[invertible (matrix.from_blocks A B C D)] :
invertible (D - (C.mul (⅟ A)).mul B)
If a block matrix is invertible and so is its bottom left element, then so is the corresponding Schur complement.
Equations
- A.invertible_of_from_blocks₁₁_invertible B C D = let iABCD' : invertible ((matrix.from_blocks A B C D).submatrix ⇑(equiv.sum_comm n m) ⇑(equiv.sum_comm n m)) := (matrix.from_blocks A B C D).submatrix_equiv_invertible (equiv.sum_comm n m) (equiv.sum_comm n m), iDCBA : invertible (matrix.from_blocks D C B A) := iABCD'.copy (matrix.from_blocks D C B A) _ in D.invertible_of_from_blocks₂₂_invertible C B A
def
matrix.invertible_equiv_from_blocks₂₂_invertible
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
(A : matrix m m α)
(B : matrix m n α)
(C : matrix n m α)
(D : matrix n n α)
[invertible D] :
invertible (matrix.from_blocks A B C D) ≃ invertible (A - (B.mul (⅟ D)).mul C)
matrix.invertible_of_from_blocks₂₂_invertible and matrix.from_blocks₂₂_invertible as an
equivalence.
Equations
- A.invertible_equiv_from_blocks₂₂_invertible B C D = {to_fun := λ (iABCD : invertible (matrix.from_blocks A B C D)), A.invertible_of_from_blocks₂₂_invertible B C D, inv_fun := λ (i_schur : invertible (A - (B.mul (⅟ D)).mul C)), A.from_blocks₂₂_invertible B C D, left_inv := _, right_inv := _}
def
matrix.invertible_equiv_from_blocks₁₁_invertible
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
(A : matrix m m α)
(B : matrix m n α)
(C : matrix n m α)
(D : matrix n n α)
[invertible A] :
invertible (matrix.from_blocks A B C D) ≃ invertible (D - (C.mul (⅟ A)).mul B)
matrix.invertible_of_from_blocks₁₁_invertible and matrix.from_blocks₁₁_invertible as an
equivalence.
Equations
- A.invertible_equiv_from_blocks₁₁_invertible B C D = {to_fun := λ (iABCD : invertible (matrix.from_blocks A B C D)), A.invertible_of_from_blocks₁₁_invertible B C D, inv_fun := λ (i_schur : invertible (D - (C.mul (⅟ A)).mul B)), A.from_blocks₁₁_invertible B C D, left_inv := _, right_inv := _}
theorem
matrix.is_unit_from_blocks_iff_of_invertible₂₂
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
{A : matrix m m α}
{B : matrix m n α}
{C : matrix n m α}
{D : matrix n n α}
[invertible D] :
If the bottom-left element of a block matrix is invertible, then the whole matrix is invertible iff the corresponding schur complement is.
theorem
matrix.is_unit_from_blocks_iff_of_invertible₁₁
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
{A : matrix m m α}
{B : matrix m n α}
{C : matrix n m α}
{D : matrix n n α}
[invertible A] :
If the top-right element of a block matrix is invertible, then the whole matrix is invertible iff the corresponding schur complement is.
Lemmas about matrix.det #
theorem
matrix.det_from_blocks₁₁
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
(A : matrix m m α)
(B : matrix m n α)
(C : matrix n m α)
(D : matrix n n α)
[invertible A] :
Determinant of a 2×2 block matrix, expanded around an invertible top left element in terms of the Schur complement.
@[simp]
theorem
matrix.det_from_blocks_one₁₁
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
(B : matrix m n α)
(C : matrix n m α)
(D : matrix n n α) :
theorem
matrix.det_from_blocks₂₂
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
(A : matrix m m α)
(B : matrix m n α)
(C : matrix n m α)
(D : matrix n n α)
[invertible D] :
Determinant of a 2×2 block matrix, expanded around an invertible bottom right element in terms of the Schur complement.
@[simp]
theorem
matrix.det_from_blocks_one₂₂
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
(A : matrix m m α)
(B : matrix m n α)
(C : matrix n m α) :
theorem
matrix.det_one_add_mul_comm
{m : Type u_2}
{n : Type u_3}
{α : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
[comm_ring α]
(A : matrix m n α)
(B : matrix n m α) :
The Weinstein–Aronszajn identity. Note the 1 on the LHS is of shape m×m, while the 1 on
the RHS is of shape n×n.
theorem
matrix.det_one_add_col_mul_row
{m : Type u_2}
{α : Type u_4}
[fintype m]
[decidable_eq m]
[comm_ring α]
(u v : m → α) :
(1 + (matrix.col u).mul (matrix.row v)).det = 1 + matrix.dot_product v u
A special case of the Matrix determinant lemma for when A = I.
TODO: show this more generally.
Lemmas about ℝ and ℂ #
theorem
matrix.schur_complement_eq₁₁
{m : Type u_2}
{n : Type u_3}
{𝕜 : Type u_5}
[is_R_or_C 𝕜]
[fintype m]
[decidable_eq m]
[fintype n]
{A : matrix m m 𝕜}
(B : matrix m n 𝕜)
(D : matrix n n 𝕜)
(x : m → 𝕜)
(y : n → 𝕜)
[invertible A]
(hA : A.is_hermitian) :
matrix.dot_product (matrix.vec_mul (has_star.star (sum.elim x y)) (matrix.from_blocks A B B.conj_transpose D)) (sum.elim x y) = matrix.dot_product (matrix.vec_mul (has_star.star (x + (A⁻¹.mul B).mul_vec y)) A) (x + (A⁻¹.mul B).mul_vec y) + matrix.dot_product (matrix.vec_mul (has_star.star y) (D - (B.conj_transpose.mul A⁻¹).mul B)) y
theorem
matrix.schur_complement_eq₂₂
{m : Type u_2}
{n : Type u_3}
{𝕜 : Type u_5}
[is_R_or_C 𝕜]
[fintype m]
[fintype n]
[decidable_eq n]
(A : matrix m m 𝕜)
(B : matrix m n 𝕜)
{D : matrix n n 𝕜}
(x : m → 𝕜)
(y : n → 𝕜)
[invertible D]
(hD : D.is_hermitian) :
matrix.dot_product (matrix.vec_mul (has_star.star (sum.elim x y)) (matrix.from_blocks A B B.conj_transpose D)) (sum.elim x y) = matrix.dot_product (matrix.vec_mul (has_star.star ((D⁻¹.mul B.conj_transpose).mul_vec x + y)) D) ((D⁻¹.mul B.conj_transpose).mul_vec x + y) + matrix.dot_product (matrix.vec_mul (has_star.star x) (A - (B.mul D⁻¹).mul B.conj_transpose)) x
theorem
matrix.is_hermitian.from_blocks₁₁
{m : Type u_2}
{n : Type u_3}
{𝕜 : Type u_5}
[is_R_or_C 𝕜]
[fintype m]
[decidable_eq m]
{A : matrix m m 𝕜}
(B : matrix m n 𝕜)
(D : matrix n n 𝕜)
(hA : A.is_hermitian) :
(matrix.from_blocks A B B.conj_transpose D).is_hermitian ↔ (D - (B.conj_transpose.mul A⁻¹).mul B).is_hermitian
theorem
matrix.is_hermitian.from_blocks₂₂
{m : Type u_2}
{n : Type u_3}
{𝕜 : Type u_5}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
(A : matrix m m 𝕜)
(B : matrix m n 𝕜)
{D : matrix n n 𝕜}
(hD : D.is_hermitian) :
(matrix.from_blocks A B B.conj_transpose D).is_hermitian ↔ (A - (B.mul D⁻¹).mul B.conj_transpose).is_hermitian
theorem
matrix.pos_semidef.from_blocks₁₁
{m : Type u_2}
{n : Type u_3}
{𝕜 : Type u_5}
[is_R_or_C 𝕜]
[fintype m]
[decidable_eq m]
[fintype n]
{A : matrix m m 𝕜}
(B : matrix m n 𝕜)
(D : matrix n n 𝕜)
(hA : A.pos_def)
[invertible A] :
(matrix.from_blocks A B B.conj_transpose D).pos_semidef ↔ (D - (B.conj_transpose.mul A⁻¹).mul B).pos_semidef
theorem
matrix.pos_semidef.from_blocks₂₂
{m : Type u_2}
{n : Type u_3}
{𝕜 : Type u_5}
[is_R_or_C 𝕜]
[fintype m]
[fintype n]
[decidable_eq n]
(A : matrix m m 𝕜)
(B : matrix m n 𝕜)
{D : matrix n n 𝕜}
(hD : D.pos_def)
[invertible D] :
(matrix.from_blocks A B B.conj_transpose D).pos_semidef ↔ (A - (B.mul D⁻¹).mul B.conj_transpose).pos_semidef