feat(Data.Matrix.Invertible): the binomial inverse theorem (#31507)

Proves the “binomial inverse theorem”, a variant of the Woodbury identity.

This is one of the 1000+ list.

Author: AntoineChambert-Loir

Mathlib/Data/Matrix/Invertible.lean

@@ -48,6 +48,34 @@ protected theorem invOf_mul_cancel_right (A : Matrix m n α) (B : Matrix n n α)
 protected theorem mul_invOf_cancel_right (A : Matrix m n α) (B : Matrix n n α) [Invertible B] :
     A * B * ⅟B = A := by rw [Matrix.mul_assoc, mul_invOf_self, Matrix.mul_one]
 
+/-- A copy oy of `invOf_mul_eq_iff_eq_mul_left` for rectangular matrices. -/
+protected theorem invOf_mul_eq_iff_eq_mul_left
+    {A B : Matrix n m α} {C : Matrix n n α} [Invertible C] :
+    ⅟C * A = B ↔ A = C * B := by
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+  · rw [← h, Matrix.mul_invOf_cancel_left]
+  · rw [h, Matrix.invOf_mul_cancel_left]
+
+/-- A copy oy of `mul_left_eq_iff_eq_invOf_mul` for rectangular matrices. -/
+protected theorem mul_left_eq_iff_eq_invOf_mul
+    {A B : Matrix n m α} {C : Matrix n n α} [Invertible C] :
+    C * A = B ↔ A = ⅟C * B := by
+  rw [eq_comm, ← Matrix.invOf_mul_eq_iff_eq_mul_left, eq_comm]
+
+/-- A copy oy of `mul_invOf_eq_iff_eq_mul_right` for rectangular matrices. -/
+protected theorem mul_invOf_eq_iff_eq_mul_right
+    {A B : Matrix m n α} {C : Matrix n n α} [Invertible C] :
+    A * ⅟C = B ↔ A = B * C := by
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+  · rw [← h, Matrix.invOf_mul_cancel_right]
+  · rw [h, Matrix.mul_invOf_cancel_right]
+
+/-- A copy oy of `mul_right_eq_iff_eq_mul_invOf` for rectangular matrices. -/
+protected theorem mul_right_eq_iff_eq_mul_invOf
+    {A B : Matrix m n α} {C : Matrix n n α} [Invertible C] :
+    A * C = B ↔ A = B * ⅟C := by
+  rw [eq_comm, ← Matrix.mul_invOf_eq_iff_eq_mul_right, eq_comm]
+
 section ConjTranspose
 variable [StarRing α] (A : Matrix n n α)
 
@@ -159,14 +187,59 @@ def invertibleAddMulMul : Invertible (A + U * C * V) where
   invOf_mul_self := add_mul_mul_invOf_mul_eq_one' _ _ _ _
   mul_invOf_self := add_mul_mul_invOf_mul_eq_one _ _ _ _
 
-/-- The **Woodbury Identity** (`⅟` version). -/
+/-- The **Woodbury Identity** (`⅟` version).
+
+See `Matrix.invOf_add_mul_mul'` for the Binomial Inverse Theorem. -/
 theorem invOf_add_mul_mul [Invertible (A + U * C * V)] :
     ⅟(A + U * C * V) = ⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A := by
   letI := invertibleAddMulMul A U C V
   convert (rfl : ⅟(A + U * C * V) = _)
 
 end Woodbury
 
+section BinomialInverseTheorem
+
+variable [Fintype m] [DecidableEq m] [Ring α]
+    (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α)
+    [Invertible A] [Invertible (C + C * V * ⅟A * U * C)]
+
+lemma add_mul_mul_mul_invOf_eq_one :
+    (A + U * C * V) * (⅟A - ⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A) = 1 := by
+  simp only [Matrix.mul_sub, Matrix.add_mul, mul_invOf_self']
+  rw [add_sub_assoc, add_eq_left, sub_eq_zero]
+  simp only [← Matrix.mul_assoc, mul_invOf_self', Matrix.one_mul]
+  simp only [← Matrix.add_mul]
+  congr
+  rw [← Matrix.mul_right_eq_iff_eq_mul_invOf]
+  simp only [Matrix.add_mul, Matrix.mul_add, Matrix.mul_assoc]
+
+lemma add_mul_mul_mul_invOf_eq_one' :
+    (⅟A - ⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A) * (A + U * C * V) = 1 := by
+  simp only [Matrix.mul_add, Matrix.sub_mul, invOf_mul_self']
+  rw [sub_add, sub_eq_self, sub_eq_zero]
+  simp only [Matrix.mul_assoc, ← Matrix.mul_sub]
+  congr
+  rw [eq_sub_iff_add_eq, ← Matrix.mul_add]
+  rw [Matrix.invOf_mul_eq_iff_eq_mul_left]
+  simp only [Matrix.add_mul, invOf_mul_self', Matrix.mul_one, add_right_inj]
+  simp only [Matrix.mul_assoc]
+
+/-- If matrices `A` and `C + C * V * A⁻¹ * U * C` are invertible, then so is `A + U * C * V`. -/
+def invertibleAddMulMul' : Invertible (A + U * C * V) where
+  invOf := ⅟A - ⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A
+  invOf_mul_self := add_mul_mul_mul_invOf_eq_one' A U C V
+  mul_invOf_self := add_mul_mul_mul_invOf_eq_one A U C V
+
+/-- The **Binomial Inverse Theorem** (`⅟` version).
+
+See `Matrix.invOf_add_mul_mul` for the Woodbury identity. -/
+theorem invOf_add_mul_mul' [Invertible (A + U * C * V)] :
+    ⅟(A + U * C * V) = ⅟A - ⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A := by
+  letI := invertibleAddMulMul' A U C V
+  convert (rfl : ⅟(A + U * C * V) = _)
+
+end BinomialInverseTheorem
+
 end Ring
 
 end Matrix

Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

@@ -260,12 +260,12 @@ theorem inv_mul_cancel_right_of_invertible (B : Matrix m n α) [Invertible A] :
 theorem inv_mul_cancel_left_of_invertible (B : Matrix n m α) [Invertible A] : A⁻¹ * (A * B) = B :=
   nonsing_inv_mul_cancel_left A B (isUnit_det_of_invertible A)
 
-theorem inv_mul_eq_iff_eq_mul_of_invertible (A B C : Matrix n n α) [Invertible A] :
+theorem inv_mul_eq_iff_eq_mul_of_invertible (A : Matrix n n α) [Invertible A] (B C : Matrix n m α) :
     A⁻¹ * B = C ↔ B = A * C :=
   ⟨fun h => by rw [← h, mul_inv_cancel_left_of_invertible],
    fun h => by rw [h, inv_mul_cancel_left_of_invertible]⟩
 
-theorem mul_inv_eq_iff_eq_mul_of_invertible (A B C : Matrix n n α) [Invertible A] :
+theorem mul_inv_eq_iff_eq_mul_of_invertible (A : Matrix n n α) [Invertible A] (B C : Matrix m n α) :
     B * A⁻¹ = C ↔ B = C * A :=
   ⟨fun h => by rw [← h, inv_mul_cancel_right_of_invertible],
    fun h => by rw [h, mul_inv_cancel_right_of_invertible]⟩
@@ -588,7 +588,9 @@ section Woodbury
 variable [Fintype m] [DecidableEq m]
 variable (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α)
 
-/-- The **Woodbury Identity** (`⁻¹` version). -/
+/-- The **Woodbury Identity** (`⁻¹` version).
+
+See ``add_mul_mul_inv_eq_sub'` for the binomial inverse theorem. -/
 theorem add_mul_mul_inv_eq_sub (hA : IsUnit A) (hC : IsUnit C) (hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)) :
     (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹ := by
   obtain ⟨_⟩ := hA.nonempty_invertible
@@ -599,6 +601,16 @@ theorem add_mul_mul_inv_eq_sub (hA : IsUnit A) (hC : IsUnit C) (hAC : IsUnit (C
   simp only [← invOf_eq_nonsing_inv]
   apply invOf_add_mul_mul
 
+/-- The **binomial inverse theorem** (variant of the Woodbury identity). -/
+theorem add_mul_mul_inv_eq_sub' (hA : IsUnit A) (h : IsUnit (C + C * V * A⁻¹ * U * C)) :
+    (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * C * (C + C * V * A⁻¹ * U * C)⁻¹ * C * V * A⁻¹ := by
+  obtain ⟨_⟩ := hA.nonempty_invertible
+  obtain ⟨ih⟩ := h.nonempty_invertible
+  simp only [← invOf_eq_nonsing_inv] at ih
+  letI := invertibleAddMulMul' A U C V
+  simp only [← invOf_eq_nonsing_inv]
+  apply invOf_add_mul_mul'
+
 end Woodbury
 
 @[simp]

docs/1000.yaml

@@ -1704,6 +1704,9 @@ Q1547975:
 
 Q1551745:
   title: Binomial inverse theorem
+  decl: Matrix.invOf_add_mul_mul'
+  authors: Antoine Chambert-Loir
+  date: 2025-11-11
 
 Q1555342:
   title: Reeh–Schlieder theorem