Equation between Eq 167 and 168

src/matrix_cookbook/3_inverses.lean

@@ -1,12 +1,18 @@
 import linear_algebra.matrix.nonsingular_inverse
 import data.complex.basic
+import tactic.swap_var
+import linear_algebra.matrix.reindex
+import matrix_cookbook.for_mathlib.linear_algebra.matrix.adjugate
+import matrix_cookbook.for_mathlib.linear_algebra.matrix.nonsing_inverse
+import matrix_cookbook.lib.mat_vec_append
 
 /-! # Inverses -/
 
 namespace matrix_cookbook
 variables {m n p : Type*}
 variables [fintype m] [fintype n] [fintype p]
 variables [decidable_eq m] [decidable_eq n] [decidable_eq p]
+variables {R: Type*}[field R]
 variables (A B C : matrix n n ℂ)
 open matrix
 open_locale matrix big_operators
@@ -86,15 +92,133 @@ end
 
 /-! ### The Searle Set of Identities -/
 
-lemma eq_161 : (1 + A⁻¹)⁻¹ = A⬝(A + 1)⁻¹ := sorry
-lemma eq_162 : (A + Bᵀ⬝B)⁻¹⬝B = A⁻¹⬝B⬝(1 + Bᵀ⬝A⁻¹⬝B)⁻¹:= sorry
-lemma eq_163 : (A⁻¹ + B⁻¹)⁻¹ = A⬝(A + B)⁻¹⬝B ∧ (A⁻¹ + B⁻¹)⁻¹ = B⬝(A + B)⁻¹⬝A := sorry
-lemma eq_164 : A - A⬝(A + B)⁻¹⬝A = B - B⬝(A + B)⁻¹⬝B := sorry
-lemma eq_165 : A⁻¹ + B⁻¹ = A⁻¹⬝(A + B)⁻¹⬝B⁻¹ := sorry
-lemma eq_166 : (1 + A⬝B)⁻¹ = 1 - A⬝(1 + B⬝A)⁻¹⬝B := sorry
-lemma eq_167 : (1 + A⬝B)⁻¹⬝A = A⬝(1 + B⬝A)⁻¹ := sorry
+lemma eq_161 {hA: is_unit A.det} {hAaddOne: is_unit (A+1).det} :  (1 + A⁻¹)⁻¹ = A⬝(A + 1)⁻¹ :=
+begin
+  rw inv_eq_right_inv, 
+  rw [matrix.add_mul, matrix.one_mul, nonsing_inv_mul_cancel_left],
+  nth_rewrite 1 ← matrix.one_mul (A + 1)⁻¹,   
+  rw [← matrix.add_mul, mul_nonsing_inv],
+  assumption',
+end
+lemma eq_162 {B: matrix n m ℂ} {hAB: is_unit (1 + Bᵀ ⬝ A⁻¹ ⬝ B).det} : 
+  (A + B⬝Bᵀ)⁻¹⬝B = A⁻¹⬝B⬝(1 + Bᵀ⬝A⁻¹⬝B)⁻¹:= 
+begin
+  rw [eq_159, matrix.sub_mul, sub_eq_iff_eq_add],
+  repeat {rw matrix.mul_assoc (A⁻¹⬝B), },
+  rw ← matrix.mul_add (A⁻¹⬝B),
+  nth_rewrite 0 ← matrix.mul_one (1 + Bᵀ ⬝ A⁻¹ ⬝ B)⁻¹,
+  repeat {rw matrix.mul_assoc (1 + Bᵀ ⬝ A⁻¹ ⬝ B)⁻¹, },
+  rwa [← matrix.mul_add (1 + Bᵀ ⬝ A⁻¹ ⬝ B)⁻¹, nonsing_inv_mul, matrix.mul_one],
+end
+lemma eq_163 {hA: is_unit A.det} {hB: is_unit B.det} {hAB: is_unit (A + B).det}: 
+  (A⁻¹ + B⁻¹)⁻¹ = A⬝(A + B)⁻¹⬝B ∧ (A⁻¹ + B⁻¹)⁻¹ = B⬝(A + B)⁻¹⬝A :=
+begin
+  split,
+  work_on_goal 2 {swap_var [A B], rw add_comm, rw add_comm B,  },
+  all_goals 
+  { rw inv_eq_right_inv, 
+    rw [matrix.add_mul, matrix.mul_assoc, nonsing_inv_mul_cancel_left],
+    apply_fun (λ x, B⬝x), dsimp, 
+    rw [matrix.mul_add, mul_nonsing_inv_cancel_left, ← matrix.add_mul, add_comm,
+    mul_nonsing_inv_cancel_left,matrix.mul_one],},
+  assumption',
+  exact left_mul_inj_of_is_unit_det hB,
+  rw add_comm, exact hAB,
+  exact left_mul_inj_of_is_unit_det hA,
+end
+
+lemma eq_164_one_side (A B : matrix n n ℂ) (hA: is_unit A.det) (hB: is_unit B.det): 
+  A - A⬝(A + B)⁻¹⬝A = (B⁻¹ + A⁻¹)⁻¹ := 
+begin
+  haveI invB := invertible_of_is_unit_det B hB,
+  nth_rewrite 0 ← matrix.mul_one B,
+  rw [eq_159, matrix.one_mul, matrix.mul_one, matrix.mul_sub, mul_nonsing_inv A hA, 
+    matrix.sub_mul, matrix.one_mul, sub_sub_cancel,  matrix.mul_assoc _ _ A, 
+    nonsing_inv_mul_cancel_right A _ hA, matrix.mul_assoc, mul_nonsing_inv_cancel_left A _ hA],
+  nth_rewrite 0 ← inv_inv_of_invertible B,
+  rw [← matrix.mul_inv_rev, matrix.add_mul, matrix.one_mul, mul_nonsing_inv_cancel_right B _ hB],
+end
+
+lemma eq_164 {hA: is_unit A.det} {hB: is_unit B.det}: 
+  A - A⬝(A + B)⁻¹⬝A = B - B⬝(A + B)⁻¹⬝B :=
+begin
+  rw [eq_164_one_side A B hA hB, add_comm A, eq_164_one_side B A hB hA, add_comm],
+end
+
+lemma eq_165 {hA: is_unit A.det} {hB: is_unit B.det} : A⁻¹ + B⁻¹ = A⁻¹⬝(A + B)⬝B⁻¹ := 
+begin 
+  rw [matrix.mul_add, matrix.add_mul, mul_nonsing_inv_cancel_right B _ hB, 
+    nonsing_inv_mul A hA, matrix.one_mul, add_comm],
+end
+
+lemma eq_166 {A: matrix n m ℂ} {B: matrix m n ℂ}: 
+  (1 + A⬝B)⁻¹ = 1 - A⬝(1 + B⬝A)⁻¹⬝B :=
+begin
+  rw eq_159 1 A B, 
+  simp only [inv_one, matrix.one_mul, matrix.mul_one],
+end
+lemma eq_167 {hAB: is_unit (1 + B⬝A).det}: (1 + A⬝B)⁻¹⬝A = A⬝(1 + B⬝A)⁻¹ := 
+begin
+  rw [eq_159 1 A B, inv_one, matrix.one_mul, matrix.mul_one, matrix.mul_one,
+    matrix.sub_mul, matrix.one_mul, sub_eq_iff_eq_add],
+  nth_rewrite 0 ← matrix.mul_one (A ⬝ (1 + B ⬝ A)⁻¹),
+  rwa [matrix.mul_assoc (A ⬝ (1 + B ⬝ A)⁻¹) _ _, ← matrix.mul_add (A ⬝ (1 + B ⬝ A)⁻¹) _ _,
+    nonsing_inv_mul_cancel_right],
+end
 
 /-! ### Rank-1 update of inverse of inner product -/
+variable X : matrix (m ⊕ unit) m R
+variable v : matrix (m ⊕ unit) unit R
+
+lemma eq_between_167_and_168 [invertible (Xᵀ⬝X)] 
+  {hα: (vᵀ ⬝ v - vᵀ ⬝ X ⬝ (Xᵀ ⬝ X)⁻¹ ⬝ Xᵀ ⬝ v) 0 0 ≠ 0}: 
+let 
+  X' := (append_mat_vec X v), 
+  A := (Xᵀ⬝X)⁻¹,
+  α := ((vᵀ⬝v) - (vᵀ⬝X⬝A⬝Xᵀ⬝v)) 0 0,
+  S11 := α•A + (A⬝Xᵀ⬝v⬝vᵀ⬝X⬝Aᵀ),    S12 := -A⬝Xᵀ⬝v,
+  S21 := -vᵀ⬝X⬝Aᵀ,                  S22 := (1: matrix unit unit R),
+  S :=  (1/α)•from_blocks S11 S12 S21 S22
+in 
+  (X'ᵀ⬝ X')⁻¹ = S := begin
+  intros X' A α S11 S12 S21 S22 S,
+  change X' with (append_mat_vec X v),
+
+  rw rank_one_update_transpose_mul_self,
+  apply inv_eq_right_inv,
+  rw [matrix.mul_smul, from_blocks_multiply, from_blocks_smul, ← from_blocks_one],
+  congr,
+
+  { have hA := is_unit_det_of_invertible (Xᵀ⬝X),
+    simp_rw [matrix.mul_add, matrix.mul_smul, mul_inv_of_invertible, smul_add, ← smul_assoc, smul_eq_mul, 
+      one_div_mul_cancel hα, one_smul], 
+    change S21 with -vᵀ ⬝ X ⬝ Aᵀ, 
+    simp_rw [matrix.neg_mul, matrix.mul_neg, smul_neg, tactic.ring.add_neg_eq_sub, 
+      sub_eq_iff_eq_add, add_right_inj, matrix.mul_assoc A, 
+      mul_nonsing_inv_cancel_left _ _ hA, ← matrix.mul_assoc], },
+  { rw smul_eq_zero, 
+    right,
+    change S12 with -A ⬝ Xᵀ ⬝ v,
+    rw [matrix.neg_mul, matrix.neg_mul, matrix.mul_neg, matrix.mul_assoc A,
+      mul_nonsing_inv_cancel_left, matrix.mul_one, add_left_neg],
+      apply is_unit_det_of_invertible,},
+  { rw smul_eq_zero,
+    right,
+    change S21 with -vᵀ ⬝ X ⬝ Aᵀ,
+    simp_rw [matrix.mul_add, matrix.mul_smul, matrix.neg_mul, matrix.mul_neg],
+    change α  with  (vᵀ ⬝ v - vᵀ ⬝ X ⬝ A ⬝ Xᵀ ⬝ v) () (),
+    simp_rw [pi.sub_apply, sub_smul, fin_one_mul_eq_smul, ← sub_eq_add_neg,
+      transpose_nonsing_inv, transpose_mul, transpose_transpose, ← matrix.mul_assoc,
+    add_sub_assoc, sub_add_sub_cancel, sub_self], },
+  { have f1 : ∀ (r: unit), r = 0, {intro r, simp only [eq_iff_true_of_subsingleton],},
+    rw [one_div, inv_smul_eq_iff₀ hα, matrix.mul_one],
+    change S12 with -A ⬝ Xᵀ ⬝ v,
+    change α  with  (vᵀ ⬝ v - vᵀ ⬝ X ⬝ A ⬝ Xᵀ ⬝ v) 0 0,
+    simp_rw [matrix.neg_mul, matrix.mul_neg],
+    funext a b,
+    simp_rw [f1 a, f1 b, pi.smul_apply, one_apply_eq, algebra.id.smul_eq_mul, mul_one, 
+      neg_add_eq_sub, ← matrix.mul_assoc],},
+end
 
 /-! ### Rank-1 update of Moore-Penrose Inverse -/
 

src/matrix_cookbook/9_special_matrices.lean

@@ -302,4 +302,4 @@ lemma eq_484 : sorry := sorry
 lemma eq_485 {n : ℕ} (v : fin n → R) (i j : fin n) : vandermonde v i j = v i ^ (j : ℕ) := vandermonde_apply _ _ _
 lemma eq_486 {n : ℕ} (v : fin n → R) :det (vandermonde v) = ∏ i : fin n, ∏ j in finset.Ioi i, (v j - v i) := det_vandermonde _
 
-end matrix_cookbook
+end matrix_cookbook

src/matrix_cookbook/for_mathlib/linear_algebra/matrix/nonsing_inverse.lean

@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2023 Mohanad Ahmed. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mohanad Ahmed
+-/
+
+import linear_algebra.matrix.nonsingular_inverse
+
+/-! # Missing lemmas about injectivity of invertible matrix multipliciations -/
+
+variables {m: Type*}[fintype m][decidable_eq m]
+variables {n: Type*}[fintype n][decidable_eq n]
+variables {R: Type*}[comm_ring R]
+
+open matrix
+open_locale matrix big_operators
+
+lemma matrix.right_mul_inj_of_invertible (P : matrix m m R) [invertible P] :
+  function.injective (λ (x : matrix n m R), x ⬝ P) := 
+begin
+  -- This chain does not work since we get * while we need ⬝ 
+  -- have w:= is_unit.mul_left_injective (
+  --   (is_unit_iff_is_unit_det P).2 (is_unit_det_of_invertible P)
+  -- ),
+
+  let hdetP_unit := matrix.is_unit_det_of_invertible P,
+  rintros x a hax, 
+  replace hax := congr_arg (λ (x : matrix n m R), x ⬝ P⁻¹) hax,
+  dsimp at hax, 
+  simp only [mul_inv_cancel_right_of_invertible] at hax,
+  exact hax,
+end
+
+lemma matrix.left_mul_inj_of_invertible (P : matrix m m R) [invertible P] :
+  function.injective (λ (x : matrix m n R), P ⬝ x) := 
+begin
+  let hdetP_unit := matrix.is_unit_det_of_invertible P,
+  rintros x a hax, 
+  replace hax := congr_arg (λ (x : matrix m n R), P⁻¹ ⬝ x) hax,
+  simp only [inv_mul_cancel_left_of_invertible] at hax,
+  exact hax,
+end
+
+lemma matrix.left_mul_inj_of_is_unit_det {P : matrix m m R} (hdetP_unit: is_unit P.det) :
+  function.injective (λ (x : matrix m n R), P ⬝ x) := 
+begin
+  haveI invP := invertible_of_is_unit_det P hdetP_unit,
+  apply matrix.left_mul_inj_of_invertible,
+end
+
+lemma matrix.right_mul_inj_of_is_unit_det {P : matrix m m R} (hdetP_unit: is_unit P.det) :
+  function.injective (λ (x : matrix n m R), x ⬝ P) := 
+begin
+  haveI invP := invertible_of_is_unit_det P hdetP_unit,
+  apply matrix.right_mul_inj_of_invertible,
+end

src/matrix_cookbook/lib/mat_vec_append.lean

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2023 Mohanad Ahmed. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mohanad Ahmed
+-/
+
+import linear_algebra.matrix.nonsingular_inverse
+import linear_algebra.matrix.reindex
+
+/-! # Support Definitions and Lemmas for Rank one Updates by concatenation-/
+namespace matrix_cookbook
+
+open matrix
+open_locale matrix big_operators
+
+variables {m n: Type*}[fintype m][fintype n][decidable_eq m][decidable_eq n]
+variables {R: Type*}[field R]
+
+variable X : matrix (m ⊕ unit) m R
+variable v : matrix (m ⊕ unit) unit R
+def append_mat_vec := of (λ i, sum.elim (X i) (v i))
+
+lemma rank_one_update_transpose_mul_self :
+  (append_mat_vec X v)ᵀ ⬝ append_mat_vec X v =
+    from_blocks (Xᵀ ⬝ X) (Xᵀ ⬝ v) (vᵀ ⬝ X) (vᵀ ⬝ v) :=
+begin
+  funext r s,
+  rw append_mat_vec,
+  cases s, cases r, work_on_goal 3 {cases r},
+  all_goals 
+  { simp only [mul_apply, transpose_apply, of_apply, sum.elim_inl, sum.elim_inr,
+    from_blocks_apply₁₁, from_blocks_apply₁₂, from_blocks_apply₂₁, from_blocks_apply₂₂, 
+    mul_apply, transpose_apply],},
+end
+
+lemma fin_one_mul_eq_smul {A: matrix unit m R} {q: matrix unit unit R}:
+  (q () ()) • A = q ⬝ A := 
+begin
+  funext r s,
+  simp only [pi.smul_apply, algebra.id.smul_eq_mul, mul_apply, 
+    fintype.univ_of_subsingleton, finset.sum_singleton],
+  congr,
+end
+
+end matrix_cookbook