Equation between Eq 167 and 168

[MohanadAhmed]

Rank One Update by Concatenation of inverse Equation

With $X$ an $(m+1)\times m$ matrix and $v$ a $(m+1)\times 1$ vector and $\alpha$ defined as: $$\alpha = v^Tv - v^TXAX^Tv$$ and $A$ $A=(X^TX)^{-1}$ we have:

$$(\bar{X}^T\bar{X})^{-1} = \frac{1}{\alpha}\begin{bmatrix} \alpha A +AX^TvvX^TA^T & -AX^Tv \\ -v^TXA^T & 1 \end{bmatrix}$$

In addition there are auxiliary lemmas:

• reindex_equiv_eq_iff_matrix_eq (e₁ e₂ : n ≃ m) (A B: matrix n n R) : two matrices A and B are equal if after re-indexing by an equivalent re-index set they are equal and vice versa.
• reindex_equiv_eq_if_matrix_eq and matrix_eq_if_reindex_equiv: give the forward and reverse directions of the lemmas above
• rank_one_update_transpose_mul_self: the rank one update by concatenation with a matrix when transposed and multiplied into itself can be expressed as a $2 \times 2$ block matrix.

This Pull Request starts from where PR #8 ends. The new changes in this PR are Equation between 167 and 168 and the lemmas mentioned above in two files mat_vec_append.lean and `reindex.lean' in the 'for_mathlib' folder.