feat(Data/Matrix/Mul): add diagonal and transpose lemmas for vector operations

[dennj]

This adds three lemmas for matrix-vector operations that serve as foundational support for future ML formalization:

• vecMul_diagonal_dotProduct: weighted inner product x ᵥ* diagonal d ⬝ᵥ y = ∑ i, d i * x i * y i
• dotProduct_transpose_mulVec: bilinear form symmetry x ⬝ᵥ Aᵀ *ᵥ y = y ⬝ᵥ A *ᵥ x
• mul_diagonal_mulVec: column-weighted sum (A * diagonal d) *ᵥ x = ∑ i, (d i * x i) • A.col i

These 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).

[github-actions]

PR summary 30e22ac079

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ dotProduct_transpose_mulVec
+ mul_diagonal_mulVec
+ vecMul_diagonal_dotProduct

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[eric-wieser]

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.

[eric-wieser]

I would expect

Suggested change

	/-- The dot product of `x ᵥ* diagonal d` with `y` equals `∑ i, d i * x i * y i`. -/
	theorem vecMul_diagonal_dotProduct [Fintype m] [DecidableEq m] [NonUnitalCommSemiring R]
	(d x y : m → R) : x ᵥ* diagonal d ⬝ᵥ y = ∑ i, d i * x i * y i := by
	simp only [dotProduct, vecMul_diagonal, mul_comm (x _) (d _), mul_assoc]
	theorem vecMul_diagonal_dotProduct [Fintype m] [DecidableEq m] [NonUnitalSemiring R]
	(d x y : m → R) : x ᵥ* diagonal d ⬝ᵥ y = ∑ i, x i * d i * y i := by
	simp only [dotProduct, vecMul_diagonal, mul_assoc]

which holds more generally; or even

Suggested change

	/-- The dot product of `x ᵥ* diagonal d` with `y` equals `∑ i, d i * x i * y i`. -/
	theorem vecMul_diagonal_dotProduct [Fintype m] [DecidableEq m] [NonUnitalCommSemiring R]
	(d x y : m → R) : x ᵥ* diagonal d ⬝ᵥ y = ∑ i, d i * x i * y i := by
	simp only [dotProduct, vecMul_diagonal, mul_comm (x _) (d _), mul_assoc]
	theorem vecMul_diagonal_dotProduct [Fintype m] [DecidableEq m]
	(d x y : m → α) : x ᵥ* diagonal d ⬝ᵥ y = ∑ i, (x i * d i) * y i := by
	simp only [dotProduct, vecMul_diagonal, mul_assoc]

[themathqueen]

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 dotProduct_transpose_mulVec is fine to keep though?

[eric-wieser]

As @themathqueen says, this lemmas is probably the most useful and worth keeping.

Since right now I don't think we declare a preferred spelling, I'd suggest additionally adding the statement that (x ᵥ* Aᵀ) ⬝ᵥ y = (y *ᵥ A) ⬝ᵥ x.