feat(Data/Matrix/Mul): add diagonal and transpose lemmas for vector operations#34851
feat(Data/Matrix/Mul): add diagonal and transpose lemmas for vector operations#34851dennj wants to merge 2 commits intoleanprover-community:masterfrom
Conversation
github-actions
bot
added
the
new-contributor
PR summary 738faa5527Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
eric-wieser
left a comment
eric-wieser
left a comment
There was a problem hiding this comment.
I'm not yet convinced by these lemmas; they're pretty trivial consequences of existing lemmas, and without choosing a preferred side of Matrix.dotProduct_mulVec, it's not clear to me whether we should write the dot product or matrix product on the left.
|
I think these lemmas should just be inlined into whatever you're trying to prove. Like Eric said, they're pretty trivial from previous lemmas. Maybe |
…perations Add three lemmas for matrix-vector operations: - `vecMul_diagonal_dotProduct`: weighted inner product identity - `dotProduct_transpose_mulVec`: bilinear form symmetry - `mul_diagonal_mulVec`: column-weighted sum expansion
| (v ᵥ* diagonal w) x = v x * w x := | ||
| dotProduct_diagonal' v w x | ||
|
|
||
| theorem vecMul_diagonal_dotProduct [Fintype m] [DecidableEq m] |
There was a problem hiding this comment.
I still think this and mul_diagonal_mulVec shouldn't be lemmas/theorems.
| ext j | ||
| simp only [mulVec, dotProduct, mul_diagonal, col_apply, Pi.smul_apply, smul_eq_mul, | ||
| Finset.sum_apply, mul_comm, mul_left_comm] |
There was a problem hiding this comment.
I think they're simple enough to just inline into wherever you need it
| ext j | |
| simp only [mulVec, dotProduct, mul_diagonal, col_apply, Pi.smul_apply, smul_eq_mul, | |
| Finset.sum_apply, mul_comm, mul_left_comm] | |
| ext; simp [mulVec, dotProduct, mul_rotate (A _ _)] |
5 participants
This adds three lemmas for matrix-vector operations that serve as foundational support for future ML formalization:
vecMul_diagonal_dotProduct: weighted inner productx ᵥ* diagonal d ⬝ᵥ y = ∑ i, d i * x i * y idotProduct_transpose_mulVec: bilinear form symmetryx ⬝ᵥ Aᵀ *ᵥ y = y ⬝ᵥ A *ᵥ xmul_diagonal_mulVec: column-weighted sum(A * diagonal d) *ᵥ x = ∑ i, (d i * x i) • A.col iThese are basic linear algebra identities involving diagonal matrices and vector operations that appear frequently in machine learning contexts (weighted inner products, attention mechanisms, feature scaling, diagonal preconditioning).