Sherman–Morrison formula

Stream: Is there code for X?

[Yufei Liu]

has Serman-Morrison formula been formalised? if not, what is the closest theorem we have?

[Eric Wieser]

@MohanadAhmed may have thought about this

[MohanadAhmed]

Yes it was in an old PR I made on the matrix cookbook.

[MohanadAhmed]

You can find it here: (https://github.com/eric-wieser/lean-matrix-cookbook/pull/3/files#diff-111c27a44f916fed8abc2dc66500d634638917368614320e1508be1d77f3c636R97)

[MohanadAhmed]

For completeness here is the Lean 3 code that I wrote at that time:

lemma sherman_morrison (A : matrix m m ℂ) (B : matrix n n ℂ) (U : matrix m n ℂ) (V : matrix n m ℂ)
  {hA: is_unit A.det} {hB: is_unit B.det} {hQ: is_unit (B⁻¹ + V ⬝ A⁻¹ ⬝ U).det}:
  (A + U⬝B⬝V)⁻¹ = A⁻¹ - A⁻¹⬝U⬝(B⁻¹+V⬝A⁻¹⬝U)⁻¹⬝V ⬝ A⁻¹ :=
begin
  rw inv_eq_right_inv,
  rw [matrix.add_mul, matrix.mul_sub, mul_nonsing_inv],
  repeat {rw matrix.mul_assoc A⁻¹ _ _},
  set Q := (B⁻¹+V⬝A⁻¹⬝U),
  rw [mul_nonsing_inv_cancel_left, matrix.mul_sub, sub_add_sub_comm,
    matrix.mul_assoc _ Q⁻¹ _,  matrix.mul_assoc U (Q⁻¹⬝V) _],

  have : U ⬝ B ⬝ V ⬝ (A⁻¹ ⬝ (U ⬝ (Q⁻¹ ⬝ V ⬝ A⁻¹)))
    = (U ⬝ B ⬝ V ⬝ A⁻¹ ⬝ U) ⬝ (Q⁻¹ ⬝ V ⬝ A⁻¹),
  { rw ← matrix.mul_assoc _ A⁻¹ _,
    rw ← matrix.mul_assoc _ U _, },
  rw this,
  rw ← matrix.add_mul,
  nth_rewrite 1 ← matrix.mul_one U,
  rw [←  mul_nonsing_inv B, ← matrix.mul_assoc _ B _],
  repeat {rw matrix.mul_assoc (U⬝B) _ _},
  rw [← matrix.mul_add (U⬝B) _ _, matrix.mul_assoc (U⬝B), matrix.mul_assoc Q⁻¹,
    mul_nonsing_inv_cancel_left, add_sub_cancel],
  assumption',
end

[MohanadAhmed]

If you want to translate this to lean 4 don't forget nth_rw in Lean4 counts from 1 not from 0!

[Yufei Liu]

thanks! I will try translate this

[Yufei Liu]

btw, how's matrix cookbook's progress on translating from lean3 to lean4?

[Eric Wieser]

I was planning to use it to test out a history merging script when I write one for mathlib

[Eric Wieser]

But remember that pretty much all the cookbook results are already in mathlib; the project was only ever intended as an index

[Yufei Liu]

Eric Wieser said:

But remember that pretty much all the cookbook results are already in mathlib; the project was only ever intended as an index

i see, thank you

[MohanadAhmed]

Eric Wieser said:

But remember that pretty much all the cookbook results are already in mathlib; the project was only ever intended as an index

@Eric Wieser

I am not sure what you mean here, because the Matrix Cookbook is still far from being formalized. (As witnessed by the red progress bar eric has on the project)

Do you mean the results currently in lean-matrix-cookbook are all in Mathlib?

[Eric Wieser]

Do you mean the results currently in lean-matrix-cookbook are all in Mathlib?

Yes, I mean for the majority of the lemmas this is (almost) the case. Certainly a vast fraction of the pdf is not anywhere though!