## Stream: math-comp analysis

### Topic: R^n with Euclidean norm

#### Jelle Wemmenhove (Dec 20 2022 at 16:11):

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|\}$.

#### Emilio Jesús Gallego Arias (Jan 17 2023 at 18:48):

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

#### Cyril Cohen (Jan 17 2023 at 19:08):

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.

#### Emilio Jesús Gallego Arias (Jan 17 2023 at 19:13):

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.

#### Cyril Cohen (Jan 17 2023 at 19:17):

e.g.

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


#### Emilio Jesús Gallego Arias (Jan 17 2023 at 19:18):

Thanks @Cyril Cohen

#### Cyril Cohen (Jan 17 2023 at 19:20):

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.

#### Cyril Cohen (Jan 17 2023 at 19:24):

(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))

#### Jelle Wemmenhove (Jan 18 2023 at 13:03):

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