vector dotproduct with summation

Stream: general

[victoria]

I'm stuck on showing the following simple example: vector dot product a sum of vectors = sum of vector dot product.

import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Matrix.Reflection
import Mathlib.Data.Matrix.RowCol
import Mathlib.Algebra.BigOperators.Finprod
import Mathlib.Algebra.BigOperators.Basic
open BigOperators
open Finset
open Matrix

example (v : Fin n → ℝ) (w : Fin m → (Fin n → ℝ)) : v ⬝ᵥ ∑ i, w i = ∑ i, v ⬝ᵥ w i := by
  sorry

[victoria]

update code

import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Matrix.Reflection
import Mathlib.Data.Matrix.RowCol
import Mathlib.Algebra.BigOperators.Finprod
import Mathlib.Algebra.BigOperators.Basic
open BigOperators
open Finset
open Matrix


variable(m : ℕ ) (n : ℕ )
example (v : Fin n → ℝ) (w : Fin m → (Fin n → ℝ)) : v ⬝ᵥ ∑ i, w i = ∑ i, v ⬝ᵥ w i := by
  sorry

[Eric Wieser]

(note that set_option autoImplicit falsewould have given you a clearer error for the first code)

[Eric Wieser]

@loogle Matrix.dot_product, Finset.sum

[loogle]

:exclamation: unknown identifier 'Matrix.dot_product'
Did you mean "Matrix.dot_product", Finset.sum?

[Eric Wieser]

@loogle  Matrix.dotProduct, Finset.sum

[loogle]

:search: Matrix.dotProduct_one, Matrix.one_dotProduct, and 5 more

[Martin Dvořák]

variable {m n : ℕ}
example (v : Fin n → ℚ) (A : Fin m → (Fin n → ℚ)) : v ⬝ᵥ ∑ i, A i = ∑ i, v ⬝ᵥ A i := by
  convert_to v ⬝ᵥ (1 ᵥ* A) = (A *ᵥ v) ⬝ᵥ 1
  · unfold Matrix.vecMul Matrix.dotProduct
    aesop
  · congr
    simp [Matrix.mulVec]
    ext
    simp [Matrix.dotProduct, mul_comm]
  rw [Matrix.dotProduct_comm _ 1, Matrix.dotProduct_mulVec, Matrix.dotProduct_comm]

[Eric Wieser]

example (v : Fin n → ℝ) (w : Fin m → (Fin n → ℝ)) : v ⬝ᵥ ∑ i, w i = ∑ i, v ⬝ᵥ w i :=
  map_sum
    { toFun := dotProduct v
      map_add' := dotProduct_add v
      map_zero' := dotProduct_zero v : _ →+ _ } _ _

[Eric Wieser]

loogle said:

:search: Matrix.dotProduct_one, Matrix.one_dotProduct, and 5 more

This lemma is evidently missing; want to contribute (a more general version of) it to mathlib?

[Richard Copley]

import Mathlib.Tactic

open BigOperators Matrix

variable {m α β : Type*} [Fintype m] [NonUnitalNonAssocSemiring α]

nonrec def Matrix.dotProduct_addHom (v : m → α) : (m → α) →+ α where
  toFun := dotProduct v
  map_add' := dotProduct_add v
  map_zero' := dotProduct_zero v

theorem Matrix.dotProduct_sum (v : m → α) (w : β → m → α) (s : Finset β) :
    v ⬝ᵥ ∑ i in s, w i = ∑ i in s, v ⬝ᵥ w i :=
  map_sum (dotProduct_addHom v) _ _

variable (m : ℕ) (n : ℕ)
example (v : Fin n → ℝ) (w : Fin m → Fin n → ℝ) : v ⬝ᵥ ∑ i, w i = ∑ i, v ⬝ᵥ w i := by
  rw? says rw [dotProduct_sum]
      -- "no goals"