Schur complement

schur_complement.lean

/- By JA, with improvements by Floris van Doorn. -/
import data.matrix.notation tactic.ring

namespace finset

universes u v w
variables {α : Type u} {β : Type v} {γ : Type w} [comm_monoid β]

open_locale big_operators

@[to_additive]
lemma prod_sum_elim' [decidable_eq (α ⊕ γ)]
  (s : finset α) (t : finset γ) (f : α ⊕ γ → β) :
  ∏ x in s.map function.embedding.inl ∪ t.map function.embedding.inr, f x =
    (∏ x in s, f (sum.inl x)) * (∏ x in t, f (sum.inr x)) :=
begin
  convert prod_sum_elim s t (λ x, f (sum.inl x)) (λ x, f (sum.inr x)),
  ext i, cases i; refl
end

end finset

namespace matrix
open_locale matrix

variables {R : Type*} [comm_ring R]
variables {m n k : Type*} [fintype m] [fintype n] [fintype k] 
variables [decidable_eq m] [decidable_eq n] [decidable_eq k]
 
@[reducible] def sum_vec (x : n → R) (y : m → R) : n ⊕ m → R := sum.elim x y

localized "infix ` ⊕ᵥ `:65 := sum_vec" in matrix

def hcompose (A : matrix m n R) (B : matrix m k R) : matrix m (n ⊕ k) R :=
λ i j, sum.cases_on j (λ j, A i j) (λ j, B i j)

def vcompose (A : matrix m n R) (B : matrix k n R) : matrix (m ⊕ k) n R :=
λ i j, sum.cases_on i (λ i, A i j) (λ i, B i j)

theorem dot_product_sum_vec (x u : n → R) (y v : m → R) : 
  dot_product (x ⊕ᵥ y) (u ⊕ᵥ v) = dot_product x u + dot_product y v :=
by { simp [dot_product, univ_sum_type, finset.sum_sum_elim'], refl }

section
variables (A : matrix n n R) (B : matrix n m R) (C : matrix m n R) (D : matrix m m R)

theorem from_blocks_eq : from_blocks A B C D = hcompose (vcompose A C) (vcompose B D) :=
by { ext i j, cases i; cases j; refl }

theorem from_blocks_eq' : from_blocks A B C D = vcompose (hcompose A B) (hcompose C D) :=
by { ext i j, cases i; cases j; refl }

end

theorem hcompose_mul_sum_vec (A : matrix m n R) (B : matrix m k R) (x : n → R) (y : k → R) :
  mul_vec (hcompose A B) (x ⊕ᵥ y) = mul_vec A x + mul_vec B y :=
by { ext i, rw [hcompose, mul_vec], apply dot_product_sum_vec }

theorem sum_vec_mul_vcompose (x : m → R) (y : k → R) (A : matrix m n R) (B : matrix k n R) :
  vec_mul (x ⊕ᵥ y) (vcompose A B) = vec_mul x A + vec_mul y B :=
by { ext i, rw [vcompose, vec_mul], apply dot_product_sum_vec }

@[simp] lemma row_sum_mul_vcompose (x : m → R) (y : k → R) (A : matrix m n R) (B : matrix k n R) :
  row (x ⊕ᵥ y) ⬝ A.vcompose B = row x ⬝ A + row y ⬝ B :=
by simp_rw [←row_vec_mul, sum_vec_mul_vcompose, row_add]  

@[simp] lemma hcompose_mul_col_sum (x : m → R) (y : k → R) (A : matrix n m R) (B : matrix n k R) :
  A.hcompose B ⬝ col (x ⊕ᵥ y) = A ⬝ col x + B ⬝ col y :=
by simp_rw [←col_mul_vec, hcompose_mul_sum_vec, col_add]  

section invertibleA

variables (A : matrix n n R) [invertible A]

@[simp] protected lemma matrix.inv_mul : ⅟A ⬝ A = 1 :=
by rw [←mul_eq_mul, inv_of_mul_self]

@[simp] protected lemma matrix.mul_inv [invertible A] : A ⬝ ⅟A = 1 :=
by rw [←mul_eq_mul, mul_inv_of_self]

@[simp] lemma matrix.mul_left_cancel (C : matrix m n R) : C ⬝ A ⬝ ⅟A = C :=
by rw [matrix.mul_assoc, matrix.mul_inv, matrix.mul_one]

@[simp] lemma matrix.mul_left_cancel' (C : matrix m n R) : C ⬝ ⅟A ⬝ A = C :=
by rw [matrix.mul_assoc, matrix.inv_mul, matrix.mul_one]

instance invertible_transpose : invertible (Aᵀ) :=
⟨(⅟A)ᵀ, by rw [mul_eq_mul, ←transpose_mul, matrix.mul_inv, transpose_one], 
        by rw [mul_eq_mul, ←transpose_mul, matrix.inv_mul, transpose_one]⟩

@[simp] lemma transpose_inverse : (⅟A)ᵀ = ⅟(Aᵀ) := rfl

@[simp] lemma inverse_injective_iff {α : Type*} [monoid α] (a b : α) [invertible a] [invertible b] :
  ⅟a = ⅟b ↔ a = b :=
⟨λ h, invertible_unique _ _ h, λ h, invertible_unique a b h⟩

@[simp] lemma inverse_transpose_symm (Asymm : Aᵀ = A) : ⅟(Aᵀ) = ⅟A :=
by simp *

end invertibleA

section

variables (A : matrix n n R) (B : matrix n m R) (C : matrix m n R) (D : matrix m m R)
variables (x u : n → R) (y v : m → R)

@[simp] lemma vec_mul_from_blocks_mul_vec (C : matrix m n R) (u : n → R) (v : m → R) :
  row (x ⊕ᵥ y) ⬝ from_blocks A B C D ⬝ col (u ⊕ᵥ v) =
    row x ⬝ A ⬝ col u + row x ⬝ B ⬝ col v + row y ⬝ C ⬝ col u + row y ⬝ D ⬝ col v :=
by { simp [from_blocks_eq', matrix.add_mul, matrix.mul_assoc, matrix.mul_add, add_assoc] }

end

end matrix

open matrix
open_locale matrix

variables {R : Type*} [comm_ring R]
variables {m n k : Type*} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n]

variables (A : matrix n n R) (B : matrix n m R) (C : matrix m n R) (D : matrix m m R)
variables (x : n → R) (y : m → R)
variable  [invertible A]

lemma exercise_1a (Asymm : Aᵀ = A) : row (x ⊕ᵥ y) ⬝ from_blocks A B Bᵀ D ⬝ col (x ⊕ᵥ y) = 
  (col x + ⅟ A ⬝ B ⬝ col y)ᵀ ⬝ A ⬝ (col x + ⅟A ⬝ B ⬝ col y) + row y ⬝ (D - Bᵀ ⬝ ⅟A ⬝ B) ⬝ col y :=
begin
  simp [matrix.add_mul, matrix.mul_add, matrix.sub_mul, matrix.mul_sub, ←matrix.mul_assoc, *],
  abel
end