Stream: math-comp analysis

Topic: R^n with Euclidean norm


view this post on Zulip Jelle Wemmenhove (Dec 20 2022 at 16:11):

Hi, new math-comp analysis user here.

Is there a way to gain access to Rn\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=max{x1,x2}||x||_\infty = \max \{|x_1|,|x_2|\}.

view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 17 2023 at 19:13):

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

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.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 17 2023 at 19:18):

Thanks @Cyril Cohen

view this post on Zulip 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.

view this post on Zulip 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))

view this post on Zulip 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