Exact Inverse Relations: Equations 146, 150 ,156 through 160 with Support Lemmas #3

MohanadAhmed · 2023-05-17T14:25:27Z

Exact Inverse Relations: Eq 146, 150, 156 through Eq 160

This Pull Request adds proofs for equations 156 through 160. In addition equations 156 and 158 have "Hermitianized" versions, where the Hermitian operator is used instead of the transpose. These might be more appropriate (or what the reader understands when thinking of comlelx matrices).

The file mat_inv_lib.lean contains support identities. These are:

is_unit_of_pos_def: a positive definite matrix is also a unit determinant matrix (basically fancy way of saying determinant is nonzero).
invertible_of_pos_def: a positive definite matrix is invertible.
A_add_B_P_Bt_pos_if_A_pos_B_pos: Given $P,R$ positive definite the sum of $ R + BPB^H$ is positive definite.
right_mul_inj_of_invertible: multiplication from the right by invertible matrices is injective.
left_mul_inj_of_invertible: multiplication from the the left by invertible matrices is injective.
unit_matrix_sandwich: a matrix unit unit R i.e. a matrix with one element interposed in an outerproduct can be removed to the left to be scalar multiplication by that one element.
$$u,v \in \mathbb{C}^{m\times 1}, s \in \mathbb{C}^{1 \times 1} \to [s]_{1,1} (uv^t) = u \cdot s \cdot v^t$$

With $\cdot{}$, meaning matrix multiplication and $[A]_{ab}$ meaning element a,b from matrix $A$:

row_mul_mat_mul_col: a weighted inner product of row and vector columns with a weight matrix in the middle can be regraded as scalar or one element matrix.
$$u^T A v = u^T \cdot A \cdot v$$
one_add_row_mul_mat_col_inv
$$(1 + c^T A b)^{-1} = [(1 + u^T \cdot A \cdot v)^{-1}]_{1,1}$$

eric-wieser · 2023-05-17T14:33:54Z

src/matrix_cookbook/mat_inv_lib.lean

+lemma is_unit_of_pos_def {A : matrix m m ℂ} (hA: matrix.pos_def A): 
+  is_unit A.det := 
+begin
+  rw is_unit_iff_ne_zero,
+  apply ne.symm,
+  cases hA with hAH hpos,
+  rw is_hermitian.det_eq_prod_eigenvalues hAH,
+  norm_cast,
+  rw ← ne.def,
+  apply ne_of_lt,
+  apply finset.prod_pos,
+  intros i _,
+  rw hAH.eigenvalues_eq,
+  apply hpos _ (λ h, _),
+  have h_det : (hAH.eigenvector_matrix)ᵀ.det = 0,
+    from matrix.det_eq_zero_of_row_eq_zero i (λ j, congr_fun h j),
+  simpa only [h_det, not_is_unit_zero] using
+    is_unit_det_of_invertible hAH.eigenvector_matrixᵀ,
+end


I guess this is a complex version of matrix.pos_def.det_pos? Can you make a PR to mathlib that generalizes that lemma to is_R_or_C 𝕜?

It seems this one is a problem. We know because the matrix is positive definite that its determinant is a real number. But the way det is defined means for a $\mathbb{C}$ matrix the determinant is another complex number. Complex numbers have no less than operator as far as I know.

I think that is why the person who wrote matrix.pos_def.det_pos avoided it anyway. just to avoid the headache?

So I guess the question is given a matrix that is is_R_or_C how do you tell lean hey lean I know this determinant is going to be real number deal with it as such?

eric-wieser · 2023-05-17T14:37:00Z

src/matrix_cookbook/mat_inv_lib.lean

+open_locale matrix big_operators
+
+
+lemma is_unit_of_pos_def {A : matrix m m ℂ} (hA: matrix.pos_def A): 


Suggested change

lemma is_unit_of_pos_def {A : matrix m m ℂ} (hA: matrix.pos_def A):

lemma matrix.pos_def.complex_is_unit_det {A : matrix m m ℂ} (hA : matrix.pos_def A) :

eric-wieser · 2023-05-17T14:37:38Z

src/matrix_cookbook/mat_inv_lib.lean

+noncomputable lemma invertible_of_pos_def {A : matrix m m ℂ} {hA: matrix.pos_def A}:
+  invertible A := 
+begin  
+  apply invertible_of_is_unit_det,
+  apply is_unit_of_pos_def,
+  exact hA,
+end


I don't think this one is worth having, if you need it you can use invertible_of_is_unit_det hA.complex_is_unit_det

eric-wieser · 2023-05-17T14:40:07Z

src/matrix_cookbook/mat_inv_lib.lean

+  (P : matrix m m ℂ) (R : matrix n n ℂ) (B : matrix n m ℂ)
+  -- [invertible P] [invertible R]
+  (hP: matrix.pos_def P) (hR: matrix.pos_def R) :
+  matrix.pos_def (B⬝P⬝Bᴴ + R) := 


There are two separate lemmas hiding here I think:

pos_def.add (hP: matrix.pos_def A) (hR: matrix.pos_def B) : matrix.pos_def (A + B)

pos_def.hermitian_conj (hP: matrix.pos_def P) : matrix.pos_def (B⬝P⬝Bᴴ)

…q156_eq160

eric-wieser · 2024-06-20T23:05:57Z

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

+lemma pos_def.add_semidef {A: matrix m m R} {B: matrix m m R}
+  (hA: matrix.pos_def A) (hB: matrix.pos_semidef B) : matrix.pos_def (A + B) :=
+begin


This one is now in leanprover-community/mathlib4#13750

…rses_eq156_eq160

eric-wieser · 2024-10-02T08:07:15Z

src/matrix_cookbook/3_inverses.lean

+lemma eq_158_hermitianized (P : matrix m m ℂ) (R : matrix n n ℂ) (B : matrix n m ℂ)
+  [invertible P] [invertible R]
+  {hP: matrix.pos_def P} {hR: matrix.pos_def R} : 
+  (P⁻¹ + Bᴴ⬝R⁻¹⬝B)⁻¹⬝Bᴴ⬝R⁻¹ = P⬝Bᴴ⬝(B⬝P⬝Bᴴ + R)⁻¹ := 
+begin
+  -- This is equation 80:
+  -- http://www.stat.columbia.edu/~liam/teaching/neurostat-spr12/papers/hmm/KF-welling-notes.pdf
+
+  have hP_unit := is_unit_iff_ne_zero.2 (pos_def.det_ne_zero hP),
+  have hR_unit := is_unit_iff_ne_zero.2 (pos_def.det_ne_zero hR),
+  have hP_inv_unit := is_unit_nonsing_inv_det P hP_unit,
+  have hR_inv_unit := is_unit_nonsing_inv_det R hR_unit,
+  have hComb_unit: is_unit (R + B ⬝ P ⬝ Bᴴ).det, 
+  { apply is_unit_iff_ne_zero.2, 
+    apply pos_def.det_ne_zero,
+    apply pos_def.add_semidef hR,
+    exact pos_def.hermitian_conj_is_semidef hP, },
+  have : is_unit (R⁻¹⁻¹ + Bᴴᴴ ⬝ P⁻¹⁻¹ ⬝ Bᴴ).det, 
+  { simp only [inv_inv_of_invertible, conj_transpose_conj_transpose],
+    apply hComb_unit, },
+
+  rw add_comm _ R,
+  nth_rewrite 1 ← conj_transpose_conj_transpose B,
+  rw eq_156_hermitianized P⁻¹ R⁻¹ Bᴴ,
+  simp only [inv_inv_of_invertible, conj_transpose_conj_transpose],
+  rw [matrix.sub_mul,  matrix.sub_mul, sub_eq_iff_eq_add], 
+  apply_fun (matrix.mul P⁻¹), 
+  rw matrix.mul_add,
+  repeat {rw ←  matrix.mul_assoc P⁻¹ _ _}, 
+  apply_fun (λ x, x⬝R),  
+  dsimp,
+  rw matrix.add_mul,
+  simp only [inv_mul_of_invertible, matrix.one_mul, 
+    inv_mul_cancel_right_of_invertible],
+  repeat {rw matrix.mul_assoc (Bᴴ⬝(R + B ⬝ P ⬝ Bᴴ)⁻¹)},
+  rw ← matrix.mul_add (Bᴴ⬝(R + B ⬝ P ⬝ Bᴴ)⁻¹), 
+  rw nonsing_inv_mul_cancel_right,
+
+  assumption',
+
+  apply right_mul_inj_of_invertible,
+  apply left_mul_inj_of_invertible,
+end


I ported this one as #16, using the mathlib-ed versions of many of your theorems; thanks for the proof outline, even though it took over a year to get merged!

Adapted from #3, using new results that have since been upstreamed to mathlib Co-authored-by: MohanadAhmed <[email protected]>

eq156 through eq160

6e56217

MohanadAhmed changed the title ~~eq156 through eq160~~ Exact Inverse Relations: Equations 156 through 160 with Support Lemmas May 17, 2023

eric-wieser reviewed May 17, 2023

View reviewed changes

MohanadAhmed added 2 commits May 19, 2023 11:04

Merge remote-tracking branch 'eric-wieser/master' into pr3_inverses_e…

74a5733

…q156_eq160

Merge remote-tracking branch 'eric-wieser/master' into pr3_inverses_e…

3a66d80

…q156_eq160

MohanadAhmed marked this pull request as draft May 19, 2023 08:16

MohanadAhmed added 15 commits May 20, 2023 00:52

some work

6a97116

some licensce stuff to get the local linter of my back

7de27e3

Some more work

d9af65b

Linter linting

9c6e35b

catch some

026c08a

Clear by congr: sm () () * v k = sm m () * v k

a5fa5ab

Prove the unit matrix smul cases

4538a7c

THis was annoying weighted_inner_product_comm

bd827af

Some work

0518716

Some cleanup

4534ddd

Some more cleanup and shutting up the linter

eb5ec92

Not very fruitful attempts at golfing

4b73d95

Move mat_inv_lib into lib folder

b3755de

Equation 146 knoced out

7b9e56d

Eq_149 and Eq150

f9248a0

MohanadAhmed changed the title ~~Exact Inverse Relations: Equations 156 through 160 with Support Lemmas~~ Exact Inverse Relations: Equations 146, 50 156 through 160 with Support Lemmas May 23, 2023

MohanadAhmed changed the title ~~Exact Inverse Relations: Equations 146, 50 156 through 160 with Support Lemmas~~ Exact Inverse Relations: Equations 146, 150 ,156 through 160 with Support Lemmas May 23, 2023

eric-wieser force-pushed the master branch from 08679ec to d52470a Compare October 19, 2023 11:03

eric-wieser added the lean3 This PR needs converting to Lean 4 if it is not already merged label Jan 7, 2024

eric-wieser mentioned this pull request Jun 11, 2024

A start on the woodbury identity #13

Merged

eric-wieser reviewed Jun 20, 2024

View reviewed changes

Merge commit '95f789f2df22c36f399dfcc3341290ee3d29f8df' into pr3_inve…

7b0f41a

…rses_eq156_eq160

eric-wieser mentioned this pull request Oct 2, 2024

Equation 158 #16

Merged

eric-wieser reviewed Oct 2, 2024

View reviewed changes

eric-wieser added a commit that referenced this pull request Oct 2, 2024

Equation 158 (#16)

7520e81

Adapted from #3, using new results that have since been upstreamed to mathlib Co-authored-by: MohanadAhmed <[email protected]>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Exact Inverse Relations: Equations 146, 150 ,156 through 160 with Support Lemmas #3

Exact Inverse Relations: Equations 146, 150 ,156 through 160 with Support Lemmas #3

MohanadAhmed commented May 17, 2023 •

edited

Loading

eric-wieser May 17, 2023 •

edited

Loading

MohanadAhmed May 19, 2023

eric-wieser May 17, 2023 •

edited

Loading

eric-wieser May 17, 2023 •

edited

Loading

eric-wieser May 17, 2023

eric-wieser Jun 20, 2024

eric-wieser Oct 2, 2024

		open_locale matrix big_operators


		lemma is_unit_of_pos_def {A : matrix m m ℂ} (hA: matrix.pos_def A):

	lemma is_unit_of_pos_def {A : matrix m m ℂ} (hA: matrix.pos_def A):
	lemma matrix.pos_def.complex_is_unit_det {A : matrix m m ℂ} (hA : matrix.pos_def A) :

Exact Inverse Relations: Equations 146, 150 ,156 through 160 with Support Lemmas #3

Are you sure you want to change the base?

Exact Inverse Relations: Equations 146, 150 ,156 through 160 with Support Lemmas #3

Conversation

MohanadAhmed commented May 17, 2023 • edited Loading

Exact Inverse Relations: Eq 146, 150, 156 through Eq 160

eric-wieser May 17, 2023 • edited Loading

Choose a reason for hiding this comment

MohanadAhmed May 19, 2023

Choose a reason for hiding this comment

eric-wieser May 17, 2023 • edited Loading

Choose a reason for hiding this comment

eric-wieser May 17, 2023 • edited Loading

Choose a reason for hiding this comment

eric-wieser May 17, 2023

Choose a reason for hiding this comment

eric-wieser Jun 20, 2024

Choose a reason for hiding this comment

eric-wieser Oct 2, 2024

Choose a reason for hiding this comment

MohanadAhmed commented May 17, 2023 •

edited

Loading

eric-wieser May 17, 2023 •

edited

Loading

eric-wieser May 17, 2023 •

edited

Loading

eric-wieser May 17, 2023 •

edited

Loading