How to create and perform math operations on vectors

Stream: new members

[David⚛️]

import Mathlib

open BigOperators
open Finset

-- Define a 3D vector space over the real numbers
def n : Nat := 3
def K := ℝ
def E := Fin n → K

-- Create two example vectors
def v : E := ![1, 2, 3]
def w : E := ![4, 5, 6]

-- Vector addition
def vector_add (v w : E) : E := fun i => v i + w i
def vsum := vector_add v w
#eval vsum

-- Vector subtraction
def vector_sub (v w : E) : E := fun i => v i - w i
def diff := vector_sub v w
#eval diff

How do I create a vector and perform a series of math operations on the vectors?

[Bjørn Kjos-Hanssen]

What you wrote works if you avoid the K and E and just say directly what you mean:

import Mathlib

open BigOperators
open Finset

-- Define a 3D vector space over the real numbers
def n : Nat := 3

-- Create two example vectors
def v : Fin n → ℝ := ![1, 2, 3]
def w : Fin n → ℝ := ![4, 5, 6]

-- Vector addition
def vector_add (v w : Fin n → ℝ) : Fin n → ℝ := fun i => v i + w i
def vsum := vector_add v w
#eval vsum

-- Vector subtraction
def vector_sub (v w : Fin n → ℝ) : Fin n → ℝ := fun i => v i - w i
def diff := vector_sub v w
#eval diff

If you really want to use E and K, one way is to use instances.

[David⚛️]

Bjørn Kjos-Hanssen ☀️ said:

What you wrote works if you avoid the K and E and just say directly what you mean:

import Mathlib

open BigOperators
open Finset

-- Define a 3D vector space over the real numbers
def n : Nat := 3

-- Create two example vectors
def v : Fin n → ℝ := ![1, 2, 3]
def w : Fin n → ℝ := ![4, 5, 6]

-- Vector addition
def vector_add (v w : Fin n → ℝ) : Fin n → ℝ := fun i => v i + w i
def vsum := vector_add v w
#eval vsum

-- Vector subtraction
def vector_sub (v w : Fin n → ℝ) : Fin n → ℝ := fun i => v i - w i
def diff := vector_sub v w
#eval diff

If you really want to use E and K, one way is to use instances.

This works fine :+1: I'm having difficulty dividing vectors. I'll appreciate any help.

[Kevin Buzzard]

You can also use abbrev E rather than def E and then things should work fine. But you'll never be able to #eval a real number, these are not floats, these are noncomputable objects (mathematical reals, so not finite precision objects).

[David⚛️]

import Mathlib

open BigOperators
open Finset

-- Define a 3D vector space over the real numbers
def n : Nat := 3

def vec_add (v w : Fin n → Float) : Fin n → Float := fun i => v i + w i
#eval vec_add (vec_add (![2,3,4]) (![3,4,5])) (![4,5,6])
#eval vec_add (![2,3,4]) (vec_add (![3,4,5]) (![4,5,6]))

This might sound a bit naive but is there a way I can write proof showing the distributive and associative properties of vectors?

[Eric Wieser]

Note that vec_add v w already exists: you can write it as v + w

[Eric Wieser]

David⚛️ said:

This might sound a bit naive but is there a way I can write proof showing the distributive and associative properties of vectors?

Not for Fin n -> Float; addition of floats is neither distributive nor associative!

[David⚛️]

Eric Wieser said:

David⚛️ said:

This might sound a bit naive but is there a way I can write proof showing the distributive and associative properties of vectors?

Not for Fin n -> Float; addition of floats is neither distributive nor associative!

Can we write an associative and distributive proof for Fin n -> Real

[Eric Wieser]

Yes, add_assoc u v w will work because mathlib already knows about associativity of this kind of vector