From a07a7ae98384cd6485d7825e161e528ba78ef3bc Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 24 Apr 2023 09:08:24 +0000 Subject: [PATCH] refactor(linear_algebra/matrix/nonsingular_inverse): move results about block matrices to `schur_complement` (#18850) This gets these out of the critical path for porting, and also balances the size of these files a little better. I've added myself second rather than last on the author list since the bulk of these moved lemmas are mine, and they are about equal in number of lines to the existing lemmas. The lemmas have been moved without modification, though the module docstring for `schur_complement` has been adapted accordingly. --- .../matrix/nonsingular_inverse.lean | 89 ------------ .../matrix/schur_complement.lean | 132 +++++++++++++++--- 2 files changed, 113 insertions(+), 108 deletions(-) diff --git a/src/linear_algebra/matrix/nonsingular_inverse.lean b/src/linear_algebra/matrix/nonsingular_inverse.lean index 1bb03fe96276e..c730f21c63493 100644 --- a/src/linear_algebra/matrix/nonsingular_inverse.lean +++ b/src/linear_algebra/matrix/nonsingular_inverse.lean @@ -615,39 +615,6 @@ inv_submatrix_equiv A e₁.symm e₂.symm end submatrix -/-! ### Block matrices -/ - -section block -variables [fintype l] -variables [decidable_eq l] -variables [fintype m] -variables [decidable_eq m] - -/-- LDU decomposition of a block matrix with an invertible top-left corner, using the -Schur complement. -/ -lemma from_blocks_eq_of_invertible₁₁ - (A : matrix m m α) (B : matrix m n α) (C : matrix l m α) (D : matrix l n α) [invertible A] : - from_blocks A B C D = - from_blocks 1 0 (C⬝⅟A) 1 ⬝ from_blocks A 0 0 (D - C⬝(⅟A)⬝B) ⬝ from_blocks 1 (⅟A⬝B) 0 1 := -by simp only [from_blocks_multiply, matrix.mul_zero, matrix.zero_mul, add_zero, zero_add, - matrix.one_mul, matrix.mul_one, matrix.inv_of_mul_self, matrix.mul_inv_of_self_assoc, - matrix.mul_inv_of_mul_self_cancel, matrix.mul_assoc, add_sub_cancel'_right] - -/-- LDU decomposition of a block matrix with an invertible bottom-right corner, using the -Schur complement. -/ -lemma from_blocks_eq_of_invertible₂₂ - (A : matrix l m α) (B : matrix l n α) (C : matrix n m α) (D : matrix n n α) [invertible D] : - from_blocks A B C D = - from_blocks 1 (B⬝⅟D) 0 1 ⬝ from_blocks (A - B⬝⅟D⬝C) 0 0 D ⬝ from_blocks 1 0 (⅟D ⬝ C) 1 := -(matrix.reindex (equiv.sum_comm _ _) (equiv.sum_comm _ _)).injective $ by - simpa [reindex_apply, sum_comm_symm, - ←submatrix_mul_equiv _ _ _ (equiv.sum_comm n m), - ←submatrix_mul_equiv _ _ _ (equiv.sum_comm n l), - sum_comm_apply, from_blocks_submatrix_sum_swap_sum_swap] - using from_blocks_eq_of_invertible₁₁ D C B A - -end block - /-! ### More results about determinants -/ section det @@ -663,62 +630,6 @@ lemma det_conj' {M : matrix m m α} (h : is_unit M) (N : matrix m m α) : det (M⁻¹ ⬝ N ⬝ M) = det N := by rw [←h.unit_spec, ←coe_units_inv, det_units_conj'] -/-- Determinant of a 2×2 block matrix, expanded around an invertible top left element in terms of -the Schur complement. -/ -lemma det_from_blocks₁₁ (A : matrix m m α) (B : matrix m n α) (C : matrix n m α) (D : matrix n n α) - [invertible A] : (matrix.from_blocks A B C D).det = det A * det (D - C ⬝ (⅟A) ⬝ B) := -by rw [from_blocks_eq_of_invertible₁₁, det_mul, det_mul, det_from_blocks_zero₂₁, - det_from_blocks_zero₂₁, det_from_blocks_zero₁₂, det_one, det_one, one_mul, one_mul, mul_one] - -@[simp] lemma det_from_blocks_one₁₁ (B : matrix m n α) (C : matrix n m α) (D : matrix n n α) : - (matrix.from_blocks 1 B C D).det = det (D - C ⬝ B) := -begin - haveI : invertible (1 : matrix m m α) := invertible_one, - rw [det_from_blocks₁₁, inv_of_one, matrix.mul_one, det_one, one_mul], -end - -/-- Determinant of a 2×2 block matrix, expanded around an invertible bottom right element in terms -of the Schur complement. -/ -lemma det_from_blocks₂₂ (A : matrix m m α) (B : matrix m n α) (C : matrix n m α) (D : matrix n n α) - [invertible D] : (matrix.from_blocks A B C D).det = det D * det (A - B ⬝ (⅟D) ⬝ C) := -begin - have : from_blocks A B C D = (from_blocks D C B A).submatrix (sum_comm _ _) (sum_comm _ _), - { ext i j, - cases i; cases j; refl }, - rw [this, det_submatrix_equiv_self, det_from_blocks₁₁], -end - -@[simp] lemma det_from_blocks_one₂₂ (A : matrix m m α) (B : matrix m n α) (C : matrix n m α) : - (matrix.from_blocks A B C 1).det = det (A - B ⬝ C) := -begin - haveI : invertible (1 : matrix n n α) := invertible_one, - rw [det_from_blocks₂₂, inv_of_one, matrix.mul_one, det_one, one_mul], -end - -/-- 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. -/ -lemma det_one_add_mul_comm (A : matrix m n α) (B : matrix n m α) : - det (1 + A ⬝ B) = det (1 + B ⬝ A) := -calc det (1 + A ⬝ B) - = det (from_blocks 1 (-A) B 1) : by rw [det_from_blocks_one₂₂, matrix.neg_mul, sub_neg_eq_add] -... = det (1 + B ⬝ A) : by rw [det_from_blocks_one₁₁, matrix.mul_neg, sub_neg_eq_add] - -/-- Alternate statement of the **Weinstein–Aronszajn identity** -/ -lemma det_mul_add_one_comm (A : matrix m n α) (B : matrix n m α) : - det (A ⬝ B + 1) = det (B ⬝ A + 1) := -by rw [add_comm, det_one_add_mul_comm, add_comm] - -lemma det_one_sub_mul_comm (A : matrix m n α) (B : matrix n m α) : - det (1 - A ⬝ B) = det (1 - B ⬝ A) := -by rw [sub_eq_add_neg, ←matrix.neg_mul, det_one_add_mul_comm, matrix.mul_neg, ←sub_eq_add_neg] - -/-- A special case of the **Matrix determinant lemma** for when `A = I`. - -TODO: show this more generally. -/ -lemma det_one_add_col_mul_row (u v : m → α) : det (1 + col u ⬝ row v) = 1 + v ⬝ᵥ u := -by rw [det_one_add_mul_comm, det_unique, pi.add_apply, pi.add_apply, matrix.one_apply_eq, - matrix.row_mul_col_apply] - end det end matrix diff --git a/src/linear_algebra/matrix/schur_complement.lean b/src/linear_algebra/matrix/schur_complement.lean index bda40a17b46a9..da1b1d46d3a3b 100644 --- a/src/linear_algebra/matrix/schur_complement.lean +++ b/src/linear_algebra/matrix/schur_complement.lean @@ -1,30 +1,130 @@ /- Copyright (c) 2022 Alexander Bentkamp. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Alexander Bentkamp, Jeremy Avigad, Johan Commelin +Authors: Alexander Bentkamp, Eric Wieser, Jeremy Avigad, Johan Commelin -/ import linear_algebra.matrix.nonsingular_inverse import linear_algebra.matrix.pos_def -/-! # Schur complement +/-! # 2×2 block matrices and the Schur complement -This file proves properties of the Schur complement `D - C A⁻¹ B` of a block matrix `[A B; C D]`. +This file proves properties of 2×2 block matrices `[A B; C D]` that relate to the Schur complement +`D - C⬝A⁻¹⬝B`. -The determinant of a block matrix in terms of the Schur complement is expressed in the lemmas -`matrix.det_from_blocks₁₁` and `matrix.det_from_blocks₂₂` in the file -`linear_algebra.matrix.nonsingular_inverse`. +## Main results -## Main result - - * `matrix.schur_complement_pos_semidef_iff` : If a matrix `A` is positive definite, then `[A B; Bᴴ - D]` is postive semidefinite if and only if `D - Bᴴ A⁻¹ B` is postive semidefinite. + * `matrix.det_from_blocks₁₁`, `matrix.det_from_blocks₂₂`: determinant of a block matrix in terms of + the Schur complement. + * `matrix.det_one_add_mul_comm`: the **Weinstein–Aronszajn identity**. + * `matrix.schur_complement_pos_semidef_iff` : If a matrix `A` is positive definite, then + `[A B; Bᴴ D]` is postive semidefinite if and only if `D - Bᴴ A⁻¹ B` is postive semidefinite. -/ +variables {l m n α : Type*} + namespace matrix +open_locale matrix + +section comm_ring +variables [fintype l] [fintype m] [fintype n] +variables [decidable_eq l] [decidable_eq m] [decidable_eq n] +variables [comm_ring α] + +/-- LDU decomposition of a block matrix with an invertible top-left corner, using the +Schur complement. -/ +lemma from_blocks_eq_of_invertible₁₁ + (A : matrix m m α) (B : matrix m n α) (C : matrix l m α) (D : matrix l n α) [invertible A] : + from_blocks A B C D = + from_blocks 1 0 (C⬝⅟A) 1 ⬝ from_blocks A 0 0 (D - C⬝(⅟A)⬝B) ⬝ from_blocks 1 (⅟A⬝B) 0 1 := +by simp only [from_blocks_multiply, matrix.mul_zero, matrix.zero_mul, add_zero, zero_add, + matrix.one_mul, matrix.mul_one, matrix.inv_of_mul_self, matrix.mul_inv_of_self_assoc, + matrix.mul_inv_of_mul_self_cancel, matrix.mul_assoc, add_sub_cancel'_right] + +/-- LDU decomposition of a block matrix with an invertible bottom-right corner, using the +Schur complement. -/ +lemma from_blocks_eq_of_invertible₂₂ + (A : matrix l m α) (B : matrix l n α) (C : matrix n m α) (D : matrix n n α) [invertible D] : + from_blocks A B C D = + from_blocks 1 (B⬝⅟D) 0 1 ⬝ from_blocks (A - B⬝⅟D⬝C) 0 0 D ⬝ from_blocks 1 0 (⅟D ⬝ C) 1 := +(matrix.reindex (equiv.sum_comm _ _) (equiv.sum_comm _ _)).injective $ by + simpa [reindex_apply, equiv.sum_comm_symm, + ←submatrix_mul_equiv _ _ _ (equiv.sum_comm n m), + ←submatrix_mul_equiv _ _ _ (equiv.sum_comm n l), + equiv.sum_comm_apply, from_blocks_submatrix_sum_swap_sum_swap] + using from_blocks_eq_of_invertible₁₁ D C B A + +/-! ### Lemmas about `matrix.det` -/ + +section det + +/-- Determinant of a 2×2 block matrix, expanded around an invertible top left element in terms of +the Schur complement. -/ +lemma det_from_blocks₁₁ (A : matrix m m α) (B : matrix m n α) (C : matrix n m α) (D : matrix n n α) + [invertible A] : (matrix.from_blocks A B C D).det = det A * det (D - C ⬝ (⅟A) ⬝ B) := +by rw [from_blocks_eq_of_invertible₁₁, det_mul, det_mul, det_from_blocks_zero₂₁, + det_from_blocks_zero₂₁, det_from_blocks_zero₁₂, det_one, det_one, one_mul, one_mul, mul_one] + +@[simp] lemma det_from_blocks_one₁₁ (B : matrix m n α) (C : matrix n m α) (D : matrix n n α) : + (matrix.from_blocks 1 B C D).det = det (D - C ⬝ B) := +begin + haveI : invertible (1 : matrix m m α) := invertible_one, + rw [det_from_blocks₁₁, inv_of_one, matrix.mul_one, det_one, one_mul], +end + +/-- Determinant of a 2×2 block matrix, expanded around an invertible bottom right element in terms +of the Schur complement. -/ +lemma det_from_blocks₂₂ (A : matrix m m α) (B : matrix m n α) (C : matrix n m α) (D : matrix n n α) + [invertible D] : (matrix.from_blocks A B C D).det = det D * det (A - B ⬝ (⅟D) ⬝ C) := +begin + have : from_blocks A B C D + = (from_blocks D C B A).submatrix (equiv.sum_comm _ _) (equiv.sum_comm _ _), + { ext i j, + cases i; cases j; refl }, + rw [this, det_submatrix_equiv_self, det_from_blocks₁₁], +end + +@[simp] lemma det_from_blocks_one₂₂ (A : matrix m m α) (B : matrix m n α) (C : matrix n m α) : + (matrix.from_blocks A B C 1).det = det (A - B ⬝ C) := +begin + haveI : invertible (1 : matrix n n α) := invertible_one, + rw [det_from_blocks₂₂, inv_of_one, matrix.mul_one, det_one, one_mul], +end + +/-- 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. -/ +lemma det_one_add_mul_comm (A : matrix m n α) (B : matrix n m α) : + det (1 + A ⬝ B) = det (1 + B ⬝ A) := +calc det (1 + A ⬝ B) + = det (from_blocks 1 (-A) B 1) : by rw [det_from_blocks_one₂₂, matrix.neg_mul, sub_neg_eq_add] +... = det (1 + B ⬝ A) : by rw [det_from_blocks_one₁₁, matrix.mul_neg, sub_neg_eq_add] + +/-- Alternate statement of the **Weinstein–Aronszajn identity** -/ +lemma det_mul_add_one_comm (A : matrix m n α) (B : matrix n m α) : + det (A ⬝ B + 1) = det (B ⬝ A + 1) := +by rw [add_comm, det_one_add_mul_comm, add_comm] + +lemma det_one_sub_mul_comm (A : matrix m n α) (B : matrix n m α) : + det (1 - A ⬝ B) = det (1 - B ⬝ A) := +by rw [sub_eq_add_neg, ←matrix.neg_mul, det_one_add_mul_comm, matrix.mul_neg, ←sub_eq_add_neg] + +/-- A special case of the **Matrix determinant lemma** for when `A = I`. + +TODO: show this more generally. -/ +lemma det_one_add_col_mul_row (u v : m → α) : det (1 + col u ⬝ row v) = 1 + v ⬝ᵥ u := +by rw [det_one_add_mul_comm, det_unique, pi.add_apply, pi.add_apply, matrix.one_apply_eq, + matrix.row_mul_col_apply] + +end det + +end comm_ring + +/-! ### Lemmas about `ℝ` and `ℂ`-/ + +section is_R_or_C open_locale matrix -variables {n : Type*} {m : Type*} {𝕜 : Type*} [is_R_or_C 𝕜] +variables {𝕜 : Type*} [is_R_or_C 𝕜] localized "infix ` ⊕ᵥ `:65 := sum.elim" in matrix @@ -54,14 +154,6 @@ begin abel end -end matrix - -namespace matrix - -open_locale matrix -variables {n : Type*} {m : Type*} - {𝕜 : Type*} [is_R_or_C 𝕜] - lemma is_hermitian.from_blocks₁₁ [fintype m] [decidable_eq m] {A : matrix m m 𝕜} (B : matrix m n 𝕜) (D : matrix n n 𝕜) (hA : A.is_hermitian) : @@ -121,4 +213,6 @@ begin convert pos_semidef.from_blocks₁₁ _ _ hD; apply_instance <|> simp end +end is_R_or_C + end matrix