Explicit representation of EuclideanSpace.single

Stream: new members

[ZhiKai Pong]

is there a way to switch between the standard basis of EuclideanSpace and the vector representation? Something like

import Mathlib

example : EuclideanSpace.single 0 (1:ℝ) = ![1, 0, 0] := by
  sorry

At least it doesn't thrown an error and the 0 on the left hand side can adjust to the dimension, so I'm wondering whether this is possible.

[Aaron Liu]

import Mathlib

example : EuclideanSpace.single 0 (1 : ℝ) = !₂[1, 0, 0] := by
  ext i
  fin_cases i <;> rfl

[ZhiKai Pong]

!! thanks

[Eric Wieser]

Or

example : EuclideanSpace.single 0 (1 : ℝ) = !₂[1, 0, 0] :=
  FinVec.etaExpand_eq _ |>.symm

[ZhiKai Pong]

What's the equivalent notation for a matrix? I don't think !!₂ works

open EuclideanSpace in
example : Matrix.vecMulVec (single 0 (1:ℝ)) (single 1 (1:ℝ)) = !![0,1,0;0,0,0;0,0,0] := by
  ext i j
  fin_cases i
  fin_cases j
  <;> rfl

[Aaron Liu]

I don't think there is a corresponding type for matrices that would require an equivalent notation.

[ZhiKai Pong]

currently the rfl doesn't work

[Aaron Liu]

Multiplication on real numbers won't rfl, try simp maybe?

[Eric Wieser]

import Mathlib

example : Matrix.vecMulVec (Pi.single 0 (1:ℝ)) (Pi.single 1 (1:ℝ)) = !![0,1,0;0,0,0;0,0,0] := by
  trans !![1*0,1*1,1*0;0*0,0*1,0*0;0*0,0*1,0*0]
  · exact Matrix.etaExpand_eq _ |>.symm
  · simp

[ZhiKai Pong]

ok if I have to state the trans matrix explicitly that's kinda annoying... thank you

[Aaron Liu]

import Mathlib

open EuclideanSpace in
example : Matrix.vecMulVec (single 0 (1:ℝ)) (single 1 (1:ℝ)) = !![0,1,0;0,0,0;0,0,0] := by
  ext i j
  fin_cases i
  fin_cases j
  <;> simp

[ZhiKai Pong]

Aaron Liu said:

import Mathlib

open EuclideanSpace in
example : Matrix.vecMulVec (single 0 (1:ℝ)) (single 1 (1:ℝ)) = !![0,1,0;0,0,0;0,0,0] := by
  ext i j
  fin_cases i
  fin_cases j
  <;> simp

I've tried this but this still throws a bunch of unreadable unsolved goals on myside - does it work on your setup?

[Jireh Loreaux]

it works in the web editor, which is on the latest Mathlib (you can click the little arrow in the upper right corner of the code block). Maybe you need to update Mathlib?

[Eric Wieser]

Note that

open EuclideanSpace in
example : Matrix.vecMulVec (single 0 (1:ℝ)) (single 1 (1:ℝ))

is ill-typed; you want Pi.single not EuclideanSpace.single

[ZhiKai Pong]

Eric Wieser said:

Note that

open EuclideanSpace in
example : Matrix.vecMulVec (single 0 (1:ℝ)) (single 1 (1:ℝ))

is ill-typed; you want Pi.single not EuclideanSpace.single

(sorry replied to the wrong message)

do you mind explaining a bit further? I don't really understand the difference

[ZhiKai Pong]

Jireh Loreaux said:

it works in the web editor, which is on the latest Mathlib (you can click the little arrow in the upper right corner of the code block). Maybe you need to update Mathlib?

seems like in the web editor there are unsolved goals as well?
image.png

[Aaron Liu]

fixed it

import Mathlib

attribute [simp] Matrix.vecMulVec_apply

open Pi in
example : Matrix.vecMulVec (single 0 (1:ℝ)) (single 1 (1:ℝ)) = !![0,1,0;0,0,0;0,0,0] := by
  ext i j
  fin_cases i <;>
  fin_cases j <;> simp

[ZhiKai Pong]

I'm aware docs#OrthonormalBasis.orthonormal exists but I would like to try to understand the tools used for the reasoning. Is there anything wrong with how I'm setting this up and how should I proceed to prove this?

import Mathlib

noncomputable
def basis (μ : Fin 3) : EuclideanSpace ℝ (Fin 3) :=
  EuclideanSpace.single μ 1

example : basis μ1 ⬝ᵥ basis μ2 = if μ1 = μ2 then 1 else 0 := by
  split_ifs with h
  unfold basis
  simp --messy goal

[Eric Wieser]

docs#dotProduct shouldn't be used on EuclideanSpace

[Eric Wieser]

You should use inner instead

[ZhiKai Pong]

Thanks, I think this works now. I have to use repeat instead of <;> , is it because unfold doesn't count as a tactic?

import Mathlib

noncomputable

def basis (μ : Fin 3) : EuclideanSpace ℝ (Fin 3) :=

  EuclideanSpace.single μ 1

example : inner (basis μ1) (basis μ2) = if μ1 = μ2 then (1:ℝ) else (0:ℝ) := by

  split_ifs with h

  repeat  -- using <;> doesn't work
    simp
    unfold basis
    simpa

[Aaron Liu]

Can you demonstrate how <;> doesn't work?

[ZhiKai Pong]

Ah ok I had this

example : inner (basis μ1) (basis μ2) = if μ1 = μ2 then (1:ℝ)  else (0:ℝ) := by
  split_ifs with h
  <;> simp; unfold basis; simpa --doesn't work

If I do this then it's fine. If I want to do a one-liner what's the proper way to type that?

example : inner (basis μ1) (basis μ2) = if μ1 = μ2 then (1:ℝ)  else (0:ℝ) := by
  split_ifs with h
  <;>
  . simp
    unfold basis
    simpa

[Eric Wieser]

split_ifs with h <;> simp; unfold basis; simpa

means

(split_ifs with h <;> simp); unfold basis; simpa

but you want

split_ifs with h <;> (simp; unfold basis; simpa)

[Eric Wieser]

or perhaps

split_ifs with h <;> . simp; unfold basis; simpa

(untested)

[ZhiKai Pong]

makes sense, thanks! can confirm the final one works