Mathlib.Data.Matrix.Invertible

Matrix.invOf_mul_cancel_left theorem

(A : Matrix n n α) (B : Matrix n m α) [Invertible A] : ⅟ A * (A * B) = B

Full source

/-- A copy of `invOf_mul_cancel_left` for rectangular matrices. -/
protected theorem invOf_mul_cancel_left (A : Matrix n n α) (B : Matrix n m α) [Invertible A] :
    ⅟ A * (A * B) = B := by rw [← Matrix.mul_assoc, invOf_mul_self, Matrix.one_mul]

Left Cancellation Property for Matrix Multiplication with Inverse

Informal description

Let $A$ be an invertible $n \times n$ matrix over a type $\alpha$, and let $B$ be an $n \times m$ matrix over $\alpha$. Then the product of the inverse of $A$ with the product of $A$ and $B$ equals $B$, i.e., $A^{-1}(AB) = B$.

Matrix.mul_invOf_cancel_left theorem

(A : Matrix n n α) (B : Matrix n m α) [Invertible A] : A * (⅟ A * B) = B

Full source

/-- A copy of `mul_invOf_cancel_left` for rectangular matrices. -/
protected theorem mul_invOf_cancel_left (A : Matrix n n α) (B : Matrix n m α) [Invertible A] :
    A * (⅟ A * B) = B := by rw [← Matrix.mul_assoc, mul_invOf_self, Matrix.one_mul]

Left Cancellation Property for Matrix Multiplication with Inverse

Informal description

Let $A$ be an invertible $n \times n$ matrix over a type $\alpha$, and let $B$ be an $n \times m$ matrix over $\alpha$. Then the product $A \cdot (A^{-1} \cdot B)$ equals $B$, where $A^{-1}$ denotes the inverse of $A$.

Matrix.invOf_mul_cancel_right theorem

(A : Matrix m n α) (B : Matrix n n α) [Invertible B] : A * ⅟ B * B = A

Full source

/-- A copy of `invOf_mul_cancel_right` for rectangular matrices. -/
protected theorem invOf_mul_cancel_right (A : Matrix m n α) (B : Matrix n n α) [Invertible B] :
    A * ⅟ B * B = A := by rw [Matrix.mul_assoc, invOf_mul_self, Matrix.mul_one]

Right cancellation property for matrix multiplication with inverse: $A B^{-1} B = A$

Informal description

For any $m \times n$ matrix $A$ and any invertible $n \times n$ matrix $B$ over a ring $\alpha$, the product $A \cdot B^{-1} \cdot B$ equals $A$.

Matrix.mul_invOf_cancel_right theorem

(A : Matrix m n α) (B : Matrix n n α) [Invertible B] : A * B * ⅟ B = A

Full source

/-- A copy of `mul_invOf_cancel_right` for rectangular matrices. -/
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]

Right Cancellation Property for Matrix Multiplication with Inverse

Informal description

Let $A$ be an $m \times n$ matrix and $B$ be an invertible $n \times n$ matrix over a type $\alpha$. Then $A \cdot B \cdot B^{-1} = A$, where $B^{-1}$ denotes the inverse of $B$.

Matrix.invertibleConjTranspose instance

[Invertible A] : Invertible Aᴴ

Full source

/-- The conjugate transpose of an invertible matrix is invertible. -/
instance invertibleConjTranspose [Invertible A] : Invertible Aᴴ := Invertible.star _

Invertibility of the Conjugate Transpose of an Invertible Matrix

Informal description

For any invertible matrix $A$, its conjugate transpose $A^\mathsf{H}$ is also invertible.

Matrix.conjTranspose_invOf theorem

[Invertible A] [Invertible Aᴴ] : (⅟ A)ᴴ = ⅟ (Aᴴ)

Full source

lemma conjTranspose_invOf [Invertible A] [Invertible Aᴴ] : (⅟A)ᴴ = ⅟(Aᴴ) := star_invOf _

Conjugate Transpose of Matrix Inverse Equals Inverse of Conjugate Transpose

Informal description

For any matrix $A$ over a ring $\alpha$, if $A$ and its conjugate transpose $A^\mathsf{H}$ are both invertible, then the conjugate transpose of the inverse of $A$ equals the inverse of the conjugate transpose of $A$, i.e., $(A^{-1})^\mathsf{H} = (A^\mathsf{H})^{-1}$.

Matrix.invertibleOfInvertibleConjTranspose definition

[Invertible Aᴴ] : Invertible A

Full source

/-- A matrix is invertible if the conjugate transpose is invertible. -/
def invertibleOfInvertibleConjTranspose [Invertible Aᴴ] : Invertible A := by
  rw [← conjTranspose_conjTranspose A, ← star_eq_conjTranspose]
  infer_instance

Invertibility of a matrix from invertibility of its conjugate transpose

Informal description

If the conjugate transpose $ A^\mathsf{H} $ of a matrix $ A $ is invertible, then $ A $ itself is invertible.

Matrix.isUnit_conjTranspose theorem

: IsUnit Aᴴ ↔ IsUnit A

Full source

@[simp] lemma isUnit_conjTranspose : IsUnitIsUnit Aᴴ ↔ IsUnit A := isUnit_star

Invertibility of Conjugate Transpose $\leftrightarrow$ Invertibility of Matrix

Informal description

For any matrix $A$, the conjugate transpose $A^\mathsf{H}$ is invertible if and only if $A$ is invertible.

Matrix.invertibleTranspose instance

[Invertible A] : Invertible Aᵀ

Full source

/-- The transpose of an invertible matrix is invertible. -/
instance invertibleTranspose [Invertible A] : Invertible Aᵀ where
  invOf := (⅟A)ᵀ
  invOf_mul_self := by rw [← transpose_mul, mul_invOf_self, transpose_one]
  mul_invOf_self := by rw [← transpose_mul, invOf_mul_self, transpose_one]

Invertibility of Matrix Transpose

Informal description

For any invertible matrix $A$, its transpose $A^\top$ is also invertible.

Matrix.transpose_invOf theorem

[Invertible A] [Invertible Aᵀ] : (⅟ A)ᵀ = ⅟ (Aᵀ)

Full source

lemma transpose_invOf [Invertible A] [Invertible Aᵀ] : (⅟A)ᵀ = ⅟(Aᵀ) := by
  letI := invertibleTranspose A
  convert (rfl : _ = ⅟(Aᵀ))

Transpose of Inverse Equals Inverse of Transpose for Invertible Matrices

Informal description

For any invertible matrix $A$ with invertible transpose $A^\top$, the transpose of the inverse of $A$ equals the inverse of the transpose of $A$, i.e., $(A^{-1})^\top = (A^\top)^{-1}$.

Matrix.invertibleOfInvertibleTranspose definition

[Invertible Aᵀ] : Invertible A

Full source

/-- `Aᵀ` is invertible when `A` is. -/
def invertibleOfInvertibleTranspose [Invertible Aᵀ] : Invertible A where
  invOf := (⅟(Aᵀ))ᵀ
  invOf_mul_self := by rw [← transpose_one, ← mul_invOf_self Aᵀ, transpose_mul, transpose_transpose]
  mul_invOf_self := by rw [← transpose_one, ← invOf_mul_self Aᵀ, transpose_mul, transpose_transpose]

Invertibility of a matrix from invertibility of its transpose

Informal description

If the transpose $ A^\top $ of a matrix $ A $ is invertible, then $ A $ is also invertible. The inverse of $ A $ is given by the transpose of the inverse of $ A^\top $.

Matrix.transposeInvertibleEquivInvertible definition

: Invertible Aᵀ ≃ Invertible A

Full source

/-- Together `Matrix.invertibleTranspose` and `Matrix.invertibleOfInvertibleTranspose` form an
equivalence, although both sides of the equiv are subsingleton anyway. -/
@[simps]
def transposeInvertibleEquivInvertible : InvertibleInvertible Aᵀ ≃ Invertible A where
  toFun := @invertibleOfInvertibleTranspose _ _ _ _ _ _
  invFun := @invertibleTranspose _ _ _ _ _ _
  left_inv _ := Subsingleton.elim _ _
  right_inv _ := Subsingleton.elim _ _

Equivalence between invertibility of a matrix and its transpose

Informal description

The equivalence between the invertibility of a matrix $ A $ and the invertibility of its transpose $ A^\top $. Specifically, the function `invertibleOfInvertibleTranspose` maps an invertible transpose to an invertible matrix, and the function `invertibleTranspose` maps an invertible matrix to an invertible transpose. Both sides of the equivalence are unique up to subsingleton elimination.

Matrix.isUnit_transpose theorem

: IsUnit Aᵀ ↔ IsUnit A

Full source

@[simp] lemma isUnit_transpose : IsUnitIsUnit Aᵀ ↔ IsUnit A := by
  simp only [← nonempty_invertible_iff_isUnit,
    (transposeInvertibleEquivInvertible A).nonempty_congr]

Invertibility of Matrix and its Transpose: $A^\top$ invertible $\leftrightarrow$ $A$ invertible

Informal description

For any matrix $A$, the transpose $A^\top$ is a unit matrix (i.e., invertible) if and only if $A$ itself is a unit matrix.

Matrix.add_mul_mul_invOf_mul_eq_one theorem

: (A + U * C * V) * (⅟ A - ⅟ A * U * ⅟ (⅟ C + V * ⅟ A * U) * V * ⅟ A) = 1

Full source

lemma add_mul_mul_invOf_mul_eq_one :
    (A + U*C*V)*(⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A) = 1 := by
  calc
    (A + U*C*V)*(⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A)
    _ = A*⅟A - A*⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A + U*C*V*⅟A - U*C*V*⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A := by
      simp_rw [add_sub_assoc, add_mul, mul_sub, Matrix.mul_assoc]
    _ = (1 + U*C*V*⅟A) - (U*⅟(⅟C + V*⅟A*U)*V*⅟A + U*C*V*⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A) := by
      rw [mul_invOf_self, Matrix.one_mul]
      abel
    _ = 1 + U*C*V*⅟A - (U + U*C*V*⅟A*U)*⅟(⅟C + V*⅟A*U)*V*⅟A := by
      rw [sub_right_inj, Matrix.add_mul, Matrix.add_mul, Matrix.add_mul]
    _ = 1 + U*C*V*⅟A - U*C*(⅟C + V*⅟A*U)*⅟(⅟C + V*⅟A*U)*V*⅟A := by
      congr
      simp only [Matrix.mul_add, Matrix.mul_invOf_cancel_right, ← Matrix.mul_assoc]
    _ = 1 := by
      rw [Matrix.mul_invOf_cancel_right]
      abel

Matrix Identity: $(A + UCV)(A^{-1} - A^{-1}U(C^{-1} + VA^{-1}U)^{-1}VA^{-1}) = I$

Informal description

Let $A$, $C$, $U$, and $V$ be matrices of appropriate dimensions over a type $\alpha$, with $A$ and $C$ invertible. Then the following matrix identity holds: $$(A + U C V) \cdot \left(A^{-1} - A^{-1} U \cdot (C^{-1} + V A^{-1} U)^{-1} \cdot V A^{-1}\right) = I,$$ where $I$ denotes the identity matrix and $A^{-1}$ denotes the inverse of $A$.

Matrix.add_mul_mul_invOf_mul_eq_one' theorem

: (⅟ A - ⅟ A * U * ⅟ (⅟ C + V * ⅟ A * U) * V * ⅟ A) * (A + U * C * V) = 1

Full source

/-- Like `add_mul_mul_invOf_mul_eq_one`, but with multiplication reversed. -/
lemma add_mul_mul_invOf_mul_eq_one' :
    (⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A)*(A + U*C*V) = 1 := by
  calc
    (⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A)*(A + U*C*V)
    _ = ⅟A*A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A*A + ⅟A*U*C*V - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A*U*C*V := by
      simp_rw [add_sub_assoc, _root_.mul_add, _root_.sub_mul, Matrix.mul_assoc]
    _ = (1 + ⅟A*U*C*V) - (⅟A*U*⅟(⅟C + V*⅟A*U)*V + ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A*U*C*V) := by
      rw [invOf_mul_self, Matrix.invOf_mul_cancel_right]
      abel
    _ = 1 + ⅟A*U*C*V - ⅟A*U*⅟(⅟C + V*⅟A*U)*(V + V*⅟A*U*C*V) := by
      rw [sub_right_inj, Matrix.mul_add]
      simp_rw [Matrix.mul_assoc]
    _ = 1 + ⅟A*U*C*V - ⅟A*U*⅟(⅟C + V*⅟A*U)*(⅟C + V*⅟A*U)*C*V := by
      congr 1
      simp only [Matrix.mul_add, Matrix.add_mul, ← Matrix.mul_assoc,
        Matrix.invOf_mul_cancel_right]
    _ = 1 := by
      rw [Matrix.invOf_mul_cancel_right]
      abel

Left inverse identity for perturbed invertible matrices: $(A^{-1} - A^{-1} U (C^{-1} + V A^{-1} U)^{-1} V A^{-1})(A + U C V) = 1$

Informal description

For invertible matrices $A$, $C$, and matrices $U$, $V$ of appropriate dimensions, the following identity holds: $$(A^{-1} - A^{-1} U (C^{-1} + V A^{-1} U)^{-1} V A^{-1}) (A + U C V) = 1$$

Matrix.invertibleAddMulMul definition

: Invertible (A + U * C * V)

Full source

/-- If matrices `A`, `C`, and `C⁻¹ + V * A⁻¹ * U` are invertible, then so is `A + U * C * V`. -/
def invertibleAddMulMul : Invertible (A + U * C * V) where
  invOf := ⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A
  invOf_mul_self := add_mul_mul_invOf_mul_eq_one' _ _ _ _
  mul_invOf_self := add_mul_mul_invOf_mul_eq_one _ _ _ _

Invertibility of perturbed matrix $A + U C V$

Informal description

Given invertible matrices $A$ and $C$, and matrices $U$, $V$ of appropriate dimensions, the matrix $A + U C V$ is invertible, with its inverse given by: $$(A + U C V)^{-1} = A^{-1} - A^{-1} U (C^{-1} + V A^{-1} U)^{-1} V A^{-1}.$$

Matrix.invOf_add_mul_mul theorem

[Invertible (A + U * C * V)] : ⅟ (A + U * C * V) = ⅟ A - ⅟ A * U * ⅟ (⅟ C + V * ⅟ A * U) * V * ⅟ A

Full source

/-- The **Woodbury Identity** (`⅟` version). -/
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) = _)

Woodbury Identity for Invertible Matrices: $(A + U C V)^{-1} = A^{-1} - A^{-1} U (C^{-1} + V A^{-1} U)^{-1} V A^{-1}$

Informal description

For invertible matrices $A$ and $C$, and matrices $U$, $V$ of appropriate dimensions, if $A + U C V$ is invertible, then its inverse is given by: $$(A + U C V)^{-1} = A^{-1} - A^{-1} U (C^{-1} + V A^{-1} U)^{-1} V A^{-1}.$$

Main results