[Merged by Bors] - feat: column and row partitioned matrices#6052
Closed
MohanadAhmed wants to merge 14 commits intomasterfrom
Closed
[Merged by Bors] - feat: column and row partitioned matrices#6052MohanadAhmed wants to merge 14 commits intomasterfrom
MohanadAhmed wants to merge 14 commits intomasterfrom
Conversation
Vierkantor
reviewed
Jul 31, 2023
Contributor
Vierkantor
left a comment
There was a problem hiding this comment.
Sorry for taking a while to get around to your review. Overall I like the structure of your work, there are just a few things that we need to fill in and clean up.
I propose some extra lemmas that will noticeably change your proofs, so I will look at the style of proofs next time.
| exact ⟨(fun h => ⟨fun i j => (h i).1 j, fun _ _ => (h _).2 _⟩), | ||
| (fun h => (fun _ => ⟨(h.1 _), (h.2 _)⟩))⟩ | ||
|
|
||
| lemma fromRows_toRows (A : Matrix (M₁ ⊕ M₂) N R) : A = fromRows A.toRows₁ A.toRows₂ := by |
Contributor
There was a problem hiding this comment.
I would move this to be right after fromColumns_toColumns, so that each column result is followed by the corresponding result on rows.
Comment on lines
+34
to
+35
| /-- Concatenate together two matrices A₁[M₁ × N] and A₂[M₂ × N] with the same columns (N) to get a | ||
| bigger matrix indexed by [(M₁ ⊕ M₂) × N] -/ |
Contributor
There was a problem hiding this comment.
I'm not familiar with the A₁[M₁ × N] notation, maybe you have a reference for it?
Collaborator
Author
There was a problem hiding this comment.
I just meant the matrix is of rows
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Vierkantor
approved these changes
Aug 2, 2023
Contributor
Vierkantor
left a comment
There was a problem hiding this comment.
I went through and cleaned up the proofs. If you're happy with the changes, then this looks ready to me.
Thanks!
bors d+
|
✌️ MohanadAhmed can now approve this pull request. To approve and merge a pull request, simply reply with |
- Rfl proofs of simp lemmas. - ext combined with simp for partitioned matrix equalities - pass arguments into simp when they are not simp lemmas i.e. mul_apply Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Collaborator
Author
bors r+ |
bors bot
pushed a commit
that referenced
this pull request
Aug 2, 2023
This file provides the basic definitions of matrices composed from columns and rows. The concatenation of two matrices with the same row indices can be expressed as `A = fromColumns A₁ A₂` the concatenation of two matrices with the same column indices can be expressed as `B = fromRows B₁ B₂`. We then provide a few lemmas that deal with the products of these with each other and with block matrices. Two particular lemmas `fromColumns_mul_fromRows_eq_one_comm` and `equiv_compl_fromColumns_mul_fromRows_eq_one_comm` deal with the case of matrix multiplication that gives one as a result. This gives a crude (but usable) replacement for the `Invertible` type which can only be applied to square matrices (with the same index type for rows and columns).
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
kim-em
pushed a commit
that referenced
this pull request
Aug 3, 2023
This file provides the basic definitions of matrices composed from columns and rows. The concatenation of two matrices with the same row indices can be expressed as `A = fromColumns A₁ A₂` the concatenation of two matrices with the same column indices can be expressed as `B = fromRows B₁ B₂`. We then provide a few lemmas that deal with the products of these with each other and with block matrices. Two particular lemmas `fromColumns_mul_fromRows_eq_one_comm` and `equiv_compl_fromColumns_mul_fromRows_eq_one_comm` deal with the case of matrix multiplication that gives one as a result. This gives a crude (but usable) replacement for the `Invertible` type which can only be applied to square matrices (with the same index type for rows and columns).
kim-em
pushed a commit
that referenced
this pull request
Aug 3, 2023
This file provides the basic definitions of matrices composed from columns and rows. The concatenation of two matrices with the same row indices can be expressed as `A = fromColumns A₁ A₂` the concatenation of two matrices with the same column indices can be expressed as `B = fromRows B₁ B₂`. We then provide a few lemmas that deal with the products of these with each other and with block matrices. Two particular lemmas `fromColumns_mul_fromRows_eq_one_comm` and `equiv_compl_fromColumns_mul_fromRows_eq_one_comm` deal with the case of matrix multiplication that gives one as a result. This gives a crude (but usable) replacement for the `Invertible` type which can only be applied to square matrices (with the same index type for rows and columns).
kim-em
pushed a commit
that referenced
this pull request
Aug 14, 2023
This file provides the basic definitions of matrices composed from columns and rows. The concatenation of two matrices with the same row indices can be expressed as `A = fromColumns A₁ A₂` the concatenation of two matrices with the same column indices can be expressed as `B = fromRows B₁ B₂`. We then provide a few lemmas that deal with the products of these with each other and with block matrices. Two particular lemmas `fromColumns_mul_fromRows_eq_one_comm` and `equiv_compl_fromColumns_mul_fromRows_eq_one_comm` deal with the case of matrix multiplication that gives one as a result. This gives a crude (but usable) replacement for the `Invertible` type which can only be applied to square matrices (with the same index type for rows and columns).
72 tasks
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
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.
This file provides the basic definitions of matrices composed from columns and rows. The concatenation of two matrices with the same row indices can be expressed as
A = fromColumns A₁ A₂the concatenation of two matrices with the same column indices can be expressed asB = fromRows B₁ B₂.We then provide a few lemmas that deal with the products of these with each other and with block matrices. Two particular lemmas
fromColumns_mul_fromRows_eq_one_commandequiv_compl_fromColumns_mul_fromRows_eq_one_commdeal with the case of matrix multiplication that gives one as a result. This gives a crude (but usable) replacement for theInvertibletype which can only be applied to square matrices (with the same index type for rows and columns).