feat(linear_algebra/matrix): The Weinstein–Aronszajn identity (#12767)

Notably this includes the proof of the determinant of a block matrix, which we didn't seem to have in the general case.

This also renames some of the lemmas about determinants of block matrices, and adds some missing API for `inv_of` on matrices.

There's some discussion at https://math.stackexchange.com/q/4105846/1896 about whether this name is appropriate, and whether it should be called "Sylvester's determinant theorem" instead.

src/linear_algebra/matrix/block.lean

@@ -67,7 +67,7 @@ lemma two_block_triangular_det (M : matrix m m R) (p : m → Prop) [decidable_pr
   M.det = (to_square_block_prop M p).det * (to_square_block_prop M (λ i, ¬p i)).det :=
 begin
   rw det_to_block M p,
-  convert upper_two_block_triangular_det (to_block M p p) (to_block M p (λ j, ¬p j))
+  convert det_from_blocks_zero₂₁ (to_block M p p) (to_block M p (λ j, ¬p j))
     (to_block M (λ j, ¬p j) (λ j, ¬p j)),
   ext,
   exact h ↑i i.2 ↑j j.2

src/linear_algebra/matrix/determinant.lean

@@ -571,10 +571,10 @@ begin
     exact hkx }
 end
 
-/-- The determinant of a 2x2 block matrix with the lower-left block equal to zero is the product of
+/-- The determinant of a 2×2 block matrix with the lower-left block equal to zero is the product of
 the determinants of the diagonal blocks. For the generalization to any number of blocks, see
 `matrix.det_of_upper_triangular`. -/
-@[simp] lemma upper_two_block_triangular_det
+@[simp] lemma det_from_blocks_zero₂₁
   (A : matrix m m R) (B : matrix m n R) (D : matrix n n R) :
   (matrix.from_blocks A B 0 D).det = A.det * D.det :=
 begin
@@ -628,31 +628,15 @@ begin
       rw [hx, from_blocks_apply₂₁], refl }}
 end
 
-/-- The determinant of a 2x2 block matrix with the upper-right block equal to zero is the product of
+/-- The determinant of a 2×2 block matrix with the upper-right block equal to zero is the product of
 the determinants of the diagonal blocks. For the generalization to any number of blocks, see
 `matrix.det_of_lower_triangular`. -/
-@[simp] lemma lower_two_block_triangular_det
+@[simp] lemma det_from_blocks_zero₁₂
   (A : matrix m m R) (C : matrix n m R) (D : matrix n n R) :
   (matrix.from_blocks A 0 C D).det = A.det * D.det :=
-by rw [←det_transpose, from_blocks_transpose, transpose_zero, upper_two_block_triangular_det,
+by rw [←det_transpose, from_blocks_transpose, transpose_zero, det_from_blocks_zero₂₁,
   det_transpose, det_transpose]
 
-/-- 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 → R) : det (1 + col u ⬝ row v) = 1 + v ⬝ᵥ u :=
-calc  det (1 + col u ⬝ row v)
-    = det (from_blocks 1 0 (row v) 1
-         ⬝ from_blocks (1 + col u ⬝ row v) (col u) 0 (1 : matrix unit unit R)
-         ⬝ from_blocks 1 0 (-row v) 1) :
-  by simp only [matrix.det_mul, upper_two_block_triangular_det, lower_two_block_triangular_det,
-                det_one, one_mul, mul_one]
-... = det (from_blocks 1 (col u) 0 (1 + row v ⬝ col u)) :
-  congr_arg _ $ by simp [from_blocks_multiply, matrix.mul_add, matrix.add_mul, ←matrix.mul_assoc,
-                         ←neg_add_rev, add_comm]
-... = det (1 + row v ⬝ col u) : by rw [upper_two_block_triangular_det, det_one, one_mul]
-... = 1 + v ⬝ᵥ u : by simp
-
 /-- Laplacian expansion of the determinant of an `n+1 × n+1` matrix along column 0. -/
 lemma det_succ_column_zero {n : ℕ} (A : matrix (fin n.succ) (fin n.succ) R) :
   det A = ∑ i : fin n.succ, (-1) ^ (i : ℕ) * A i 0 *

src/linear_algebra/matrix/nonsingular_inverse.lean

@@ -49,22 +49,43 @@ matrix inverse, cramer, cramer's rule, adjugate
 -/
 
 namespace matrix
-universes u v
-variables {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α]
+universes u u' v
+variables {m : Type u} {n : Type u'} {α : Type v}
 open_locale matrix big_operators
 open equiv equiv.perm finset
 
-variables (A : matrix n n α) (B : matrix n n α)
-
 /-! ### Matrices are `invertible` iff their determinants are -/
 
 section invertible
+variables [fintype n] [decidable_eq n] [comm_ring α]
 
 /-- A copy of `inv_of_mul_self` using `⬝` not `*`. -/
-protected lemma inv_of_mul_self [invertible A] : ⅟A ⬝ A = 1 := inv_of_mul_self A
+protected lemma inv_of_mul_self (A : matrix n n α) [invertible A] : ⅟A ⬝ A = 1 := inv_of_mul_self A
 
 /-- A copy of `mul_inv_of_self` using `⬝` not `*`. -/
-protected lemma mul_inv_of_self [invertible A] : A ⬝ ⅟A = 1 := mul_inv_of_self A
+protected lemma mul_inv_of_self (A : matrix n n α) [invertible A] : A ⬝ ⅟A = 1 := mul_inv_of_self A
+
+/-- A copy of `inv_of_mul_self_assoc` using `⬝` not `*`. -/
+protected lemma inv_of_mul_self_assoc (A : matrix n n α) (B : matrix n m α) [invertible A] :
+  ⅟A ⬝ (A ⬝ B) = B :=
+by rw [←matrix.mul_assoc, matrix.inv_of_mul_self, matrix.one_mul]
+
+/-- A copy of `mul_inv_of_self_assoc` using `⬝` not `*`. -/
+protected lemma mul_inv_of_self_assoc (A : matrix n n α) (B : matrix n m α) [invertible A] :
+  A ⬝ (⅟A ⬝ B) = B :=
+by rw [←matrix.mul_assoc, matrix.mul_inv_of_self, matrix.one_mul]
+
+/-- A copy of `mul_inv_of_mul_self_cancel` using `⬝` not `*`. -/
+protected lemma mul_inv_of_mul_self_cancel (A : matrix m n α) (B : matrix n n α)
+  [invertible B] : A ⬝ ⅟B ⬝ B = A :=
+by rw [matrix.mul_assoc, matrix.inv_of_mul_self, matrix.mul_one]
+
+/-- A copy of `mul_mul_inv_of_self_cancel` using `⬝` not `*`. -/
+protected lemma mul_mul_inv_of_self_cancel (A : matrix m n α) (B : matrix n n α)
+  [invertible B] : A ⬝ B ⬝ ⅟B = A :=
+by rw [matrix.mul_assoc, matrix.mul_inv_of_self, matrix.mul_one]
+
+variables (A : matrix n n α) (B : matrix n n α)
 
 /-- If `A.det` has a constructive inverse, produce one for `A`. -/
 def invertible_of_det_invertible [invertible A.det] : invertible A :=
@@ -163,7 +184,8 @@ lemma det_ne_zero_of_right_inverse [nontrivial α] (h : A ⬝ B = 1) : A.det ≠
 
 end invertible
 
-open_locale classical
+variables [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α]
+variables (A : matrix n n α) (B : matrix n n α)
 
 lemma is_unit_det_transpose (h : is_unit A.det) : is_unit Aᵀ.det :=
 by { rw det_transpose, exact h, }
@@ -384,4 +406,69 @@ end
 by rw [← (A⁻¹).transpose_transpose, vec_mul_transpose, transpose_nonsing_inv, ← det_transpose,
     Aᵀ.det_smul_inv_mul_vec_eq_cramer _ (is_unit_det_transpose A h)]
 
+/-! ### More results about determinants -/
+
+/-- 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) :=
+begin
+  have : 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,
+  { 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] },
+  rw [this, 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],
+end
+
+@[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).minor (sum_comm _ _) (sum_comm _ _),
+  { ext i j,
+    cases i; cases j; refl },
+  rw [this, det_minor_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 matrix