Equation between Eq 167 and 168 #9
Open
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
….lean Co-authored-by: Eric Wieser <[email protected]>
….lean Co-authored-by: Eric Wieser <[email protected]>
Contributor
Author
|
Seems mathlib upgrade broke two things:
|
eric-wieser
reviewed
May 28, 2023
Comment on lines
19
to
28
| lemma reindex_equiv_eq_if_matrix_eq (e₁ : m ≃ o) (e₂: n ≃ p) (A B: matrix m n R) : | ||
| (reindex e₁ e₂ A = reindex e₁ e₂ B) → A = B := | ||
| begin | ||
| intro h, | ||
| rw ← matrix.ext_iff at h, | ||
| funext r s, | ||
| specialize h (e₁ r) (e₂ s), | ||
| simp only [reindex_apply, submatrix_apply, equiv.symm_apply_apply] at h, | ||
| exact h, | ||
| end |
Owner
There was a problem hiding this comment.
This is (reindex e₁ e₂).injective
eric-wieser
reviewed
May 28, 2023
Comment on lines
39
to
41
| lemma reindex_equiv_eq_iff_matrix_eq (e₁ e₂ : n ≃ m) (A B: matrix n n R) : | ||
| (reindex e₁ e₂ A = reindex e₁ e₂ B) ↔ A = B := | ||
| ⟨ reindex_equiv_eq_if_matrix_eq _ _ _ _, matrix_eq_if_reindex_equiv _ _ _ _⟩ |
eric-wieser
reviewed
May 28, 2023
Owner
There was a problem hiding this comment.
Based on my comments below, I think this whole file can be discarded.
Owner
I'll do a version bump separately |
eric-wieser
added
the
lean3
Merged
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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$$ $A$ $A=(X^TX)^{-1}$ we have:
and
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_eqandmatrix_eq_if_reindex_equiv: give the forward and reverse directions of the lemmas aboverank_one_update_transpose_mul_self: the rank one update by concatenation with a matrix when transposed and multiplied into itself can be expressed as aThis 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.leanand `reindex.lean' in the 'for_mathlib' folder.