Hi, new math-comp analysis user here.

Is there a way to gain access to $\mathbb{R}^n$ as a `normedModType`

equipped with the Euclidean norm?

I tried `R * R`

and `'rV[R]_2`

where `R : realType`

, but in both cases the standard `` | x |`

turns out to be the maximum norm $||x||_\infty = \max \{|x_1|,|x_2|\}$.

Hi folks, @Jelle Wemmenhove was wondering who / how he could make progress on this issue, maybe @Cyril Cohen knows about the instances for `normedModType`

?

To my knowledge, no-one is working on it at the moment. Contributions are welcome. Technically speaking I would put an alias of `'rV`

for the Euclidean norm.

Thanks @Cyril Cohen , so if I understand correctly, the todo is roughly:

- define a type convertible with
`'rV[R]_n`

- create the instance for normedModType

So if that's the case, it seems that the main difficulty would be to find a name for the alias, right? Does anyone have a suggestion?

I was thinking that maybe `normedModType`

would need an extra parameter to index by the norm, so I was fearing some complexity.

e.g.

```
Definition euclidean (R : Type) (n : nat) := 'rV[R]_n.
Notation "'E[ R ]_ n" := (euclidean R n) (...) : type_scope.
```

Thanks @Cyril Cohen

I'm not sure `'E`

is the best notation, but we can trigger a discussion on the PR and easily substitute everywhere in case of change.

(Just a remark: the reason why the default norm is the infinite norm is that is works for every field, while the 2-norm requires at least a pythagorean field (sums of squares must be squares))

Thank you very much! It's clear what should be done, maybe it could turn into a contribution in the end! :)

Last updated: Jun 22 2024 at 16:02 UTC