standard basis

Stream: new members

[Hans Parshall]

I would like to show that the standard basis is orthonormal, and I get to a reasonable looking statement in terms of function.update:

import analysis.inner_product_space.basic
import analysis.inner_product_space.pi_L2
import analysis.normed_space.pi_Lp

variables {F m : Type*}
  [is_R_or_C F]
  [fintype m]
  [decidable_eq m]
  [inner_product_space F (m → F)]

lemma bm_on : orthonormal F (pi.basis_fun F m) :=
begin
  rw orthonormal,
  split,
  intro i,
  {
    rw pi.basis_fun,
    simp,
    sorry,
  },
  intros i j,
  intro neq,
  {
    rw pi.basis_fun,
    simp,
    sorry,
  },
end

I am having difficulty getting function.update to interact with inner. Any help is appreciated!

[Kevin Buzzard]

Doesn't variable [inner_product_space F (m → F)] mean "assume there is a completely arbitrary inner product space structure on m → F about which we know nothing"? If so then your lemma will not be true. I'm not 100% sure of this though, I don't know this part of the library.

[Hans Parshall]

This does seem like an issue. How do I specialize?

[Heather Macbeth]

You should use docs#euclidean_space !

[Hans Parshall]

How do I access the standard basis for euclidean_space ?

[Heather Macbeth]

Something like (ite (i = j) (1:𝕜) 0 : euclidean_space 𝕜 m), although I'd be curious to know what your use case is ... do you really need a basis for it?

[Hans Parshall]

The current use case is practicing Lean and navigating mathlib; I think that my original reason for wanting this basis is obsolete, but it still feels like an exercise that I should be able to accomplish.

[Hans Parshall]

I am still very new to this and appreciate your help!

[Yaël Dillies]

Precisely, you can use docs#pi.single

[Hans Parshall]

I think this is what pi.basis_fun does. How do I work with this in euclidean space?