Generalization of `⬝ᵥ` and `*ᵥ`

Stream: mathlib4

[Martin Dvořák]

In a recent review, we were asked (anonymously) whether our generalized version of ⬝ᵥ and *ᵥ defined here could be integrated into Mathlib.

What is your opinion?

[Yaël Dillies]

What does it do? What does it generalise?

[Martin Dvořák]

I tried to write it as readably as possible:

variable {I J : Type*} [Fintype I] [Fintype J] {α γ : Type*} [AddCommMonoid α] [SMul γ α]
def dotWeig (v : I → α) (w : I → γ) : α := ∑ i : I, w i • v i    -- generalizes `⬝ᵥ`
def Matrix.mulWeig (M : Matrix I J α) (w : J → γ) (i : I) : α := M i ᵥ⬝ w    -- `*ᵥ`

[Yaël Dillies]

What are the corresponding Lean declarations?

[Martin Dvořák]

docs#dotProduct
docs#Matrix.mulVec

[Yaël Dillies]

Ah, so the generalisation is that you replace * with • inside the definition of dotProduct? Sounds reasonable yes, although I suspect making that generalisation might make elaboration more brittle

[Martin Dvořák]

There is a long-winded explanation in Section 2.3.1 here on page 8, but I doubt anybody wants to read it. The code should speak for itself.

[Yaël Dillies]

Well of course, you could generalise to the point where you can use docs#Finset.sum directly :slight_smile: