multiplying a matrix and a vector in Euclidean space

Stream: Is there code for X?

[David Renshaw]

import Mathlib.Analysis.InnerProductSpace.PiL2

open scoped Matrix

def I : Matrix (Fin 3) (Fin 3) ℚ := !![1,0,0; 0,1,0; 0,0,1]

def v : EuclideanSpace ℚ (Fin 3) := ![3,4,5]
def w : EuclideanSpace ℚ (Fin 3) := ![6,7,8]

-- To my surprise, I get a type error on the following:
#check w + I *ᵥ v
--failed to synthesize
--  HAdd (EuclideanSpace ℚ (Fin 3)) (Fin 3 → ℚ) ?m.1201

-- The problem seems to be that matrix multiplication puts us in `Fin 3 → ℚ`
-- rather than `EuclideanSpace ℚ (Fin 3)`:
#check I *ᵥ v
-- I *ᵥ v : Fin 3 → ℚ

-- Even casting back does not seem to help:
#check ((I *ᵥ v) : EuclideanSpace ℚ (Fin 3))
-- I *ᵥ v : Fin 3 → ℚ

-- I can use `WithLp.equiv`, but that's ugly and noncomputable:
#check w + (WithLp.equiv _ _).symm (I *ᵥ v)
-- w + (WithLp.equiv 2 (Fin 3 → ℚ)).symm (I *ᵥ v) : EuclideanSpace ℚ (Fin 3)

[David Renshaw]

^ Is there a nice way to apply a matrix to a vector in Euclidean space and get back a vector in Euclidean space?

[David Renshaw]

(I'm aware that WithLp has known issues with defeq abuse that are being worked on: https://leanprover.zulipchat.com/#narrow/channel/345428-mathlib-reviewers/topic/.2324261.20WithLp.20refactoring/near/522889153 )

[David Renshaw]

It seems that I can use the id function to cast, but I can't use ( · : EuclideanSpace ℚ (Fin 3)):

import Mathlib.Analysis.InnerProductSpace.PiL2

open scoped Matrix

def I : Matrix (Fin 3) (Fin 3) ℚ := !![1,0,0; 0,1,0; 0,0,1]

def v : EuclideanSpace ℚ (Fin 3) := ![3,4,5]
def w : EuclideanSpace ℚ (Fin 3) := ![6,7,8]

-- This works:
#check w + (id (α := EuclideanSpace ℚ (Fin 3)) (I *ᵥ v))

-- This does not work:
#check w + ((I *ᵥ v) : EuclideanSpace ℚ (Fin 3))
-- failed to synthesize
--  HAdd (EuclideanSpace ℚ (Fin 3)) (Fin 3 → ℚ) ?m.2359

[David Renshaw]

Ah, maybe I'm supposed to be using docs#Matrix.toEuclideanLin. But then I need to change my field to ℝ.

[Eric Wieser]

Either that or pull the vectors back into non euclidean space

[David Renshaw]

The RCLike / IsROrC assumption got dropped from EuclideanSpace in mathlib4#11428. I wonder if it should be correspondingly relaxed for Matrix.toEuclideanLin.

[Eric Wieser]

It definitely should

[Eric Wieser]

PR welcome!

[Paul Lezeau]

(resurrecting this old thread): @Eric Wieser do you think it would be reasonable to add a SMul instance for this?

[Eric Wieser]

With what type?

[Paul Lezeau]

Something along the lines of

import Mathlib

variable {n : Type*} [Fintype n] [DecidableEq n]

noncomputable instance : SMul (Matrix n n ℝ) (EuclideanSpace ℝ n) where
  smul A v := Matrix.toEuclideanLin A v

-- Looks a little nicer than `Matrix.toEuclideanLin !![1, 0; 0, 1] !₂[1, 0]`
example : !![1, 0; 0, 1] • !₂[1, 0] = !₂[1, 0] := by
  ext i
  fin_cases i <;> simp

[Paul Lezeau]

(replacing $\mathbb{R}$ by a general field of course)

[Eric Wieser]

I was going to make a counter-argument, but ran into a bug instead:

import Mathlib

variable {n : Type*} [Fintype n] [DecidableEq n]

#synth Module (EuclideanSpace ℝ n →ₗ[ℝ] EuclideanSpace ℝ n) (EuclideanSpace ℝ n)  -- ok
#synth SMul (EuclideanSpace ℝ n →ₗ[ℝ] EuclideanSpace ℝ n) (EuclideanSpace ℝ n)  -- times out

[Eric Wieser]

Paul Lezeau said:

(replacing $\mathbb{R}$ by a general field of course)

Note that your example doesn't work any more with this change, since Lean can't infer the ring

[Paul Lezeau]

Eric Wieser said:

Note that your example doesn't work any more with this change, since Lean can't infer the ring

By this change, do you mean replacing Matrix n n F by (EuclideanSpace F n →ₗ[F] EuclideanSpace F n) ?
This seems to work for me

import Mathlib

variable {R : Type*} [Field R] [RCLike R] {n : Type*} [Fintype n] [DecidableEq n]

noncomputable instance : SMul (Matrix n n R) (EuclideanSpace R n) where
  smul A v := Matrix.toEuclideanLin A v

-- Looks a little nicer than `Matrix.toEuclideanLin !![1, 0; 0, 1] !₂[1, 0]`
example : !![(1 : R), 0; 0, 1] • !₂[(1 : R), 0] = !₂[1, 0] := by
  sorry

[Eric Wieser]

In that case you can write !![(1 : R), 0; 0, 1].toEuclideanLin !₂[1, 0] as a middle ground

[Eric Wieser]

(my comment was how you couldn't avoid the : R, which in your previous example was needed to make dot notation work)

[Paul Lezeau]

Right! But I think this will often be fine in the case where one is working with variables of type R/over R anyway (e.g an abstract matrix A : Matrix n n R)