Stream: new members

Topic: R^n

Anatole Dedecker (Aug 12 2020 at 23:38):

Ok so this is a dumb question as I am discovering mathlib's linear algebra library, but I can't find anything about ℝ^n being a vector_space :sweat_smile:

Jalex Stark (Aug 13 2020 at 01:59):

i actually don't know whether this answers your question, but have you watched anne baanen's video on linear algebra from lftcm2020?

Floris van Doorn (Aug 13 2020 at 02:24):

If you write fin n -> ℝ (or even better \i -> ℝ, possibly with [fintype \i]) then by apply_instance should find the instance docs#pi.semimodule . At least, I hope, since vector_space is defined to be semimodule.

Anatole Dedecker (Aug 13 2020 at 09:15):

Yes I thought about using fin n -> \R, which definitely work, but I didn't know if it was the appropriate way to talk about R^n (I was expecting some kind of Cartesian product). Also thanks @Jalex Stark I'll watch this.

Anatole Dedecker (Aug 13 2020 at 09:21):

Fun fact, I told a friend of mine who didn't know Lean about defining R^n as fin n -> \R (which I translated as ⟦1,n⟧ → ℝ), and I think he started to doubt my sanity

Kevin Buzzard (Aug 13 2020 at 09:28):

It doesn't matter what the implementation is to a user, and this implementation is easier to use than the inductive definition (which is the only other one I can imagine).

Anatole Dedecker (Aug 13 2020 at 09:30):

Indeed, but he just told me "that's not what R^n is (i.e a cartesian product)"

Kevin Buzzard (Aug 13 2020 at 09:46):

Then he needs to and learn about implementation v specification. Does he believe that 3 is {0,1,2}?

Kevin Buzzard (Aug 13 2020 at 09:47):

Because if he's using ZFC and he unwraps all the packaging, he might find out that this is what it is, except if he's looking at the real number 3, which of course is an uncountable set of Cauchy sequences.

Kevin Buzzard (Aug 13 2020 at 09:48):

A cartesian product only works for two sets. How can you use cartesian products for n sets?

Anatole Dedecker (Aug 13 2020 at 09:55):

He meant a recursive cartesian product, like $\mathbb{R}^n$ is $\mathbb{R}^{n-1} \times \mathbb{R}$

Anatole Dedecker (Aug 13 2020 at 09:56):

But yeah I told him about hidden isomorphisms and all

Kevin Buzzard (Aug 13 2020 at 12:13):

So he wants to prove e.g. that R^n is a group by induction on n? And in your definition you just get it immediately, right?

Kevin Buzzard (Aug 13 2020 at 12:13):

So this shows that your definition is a better implementation

Adam Topaz (Aug 13 2020 at 13:55):

I think the point in this case is that you need to think about $\mathbb{R}^S$ for some arbitrary set $S$, and $\mathbb{R}^n$ is the special case where $S$ is the canonical set of size n.

tsuki hao (Aug 08 2023 at 06:17):

May I ask how could R^n be defined in lean?

Moritz Doll (Aug 08 2023 at 06:42):

We have docs#EuclideanSpace but depending on the goal we prefer to state theorems in terms of arbitrary finite dimensional vector spaces.

tsuki hao (Aug 08 2023 at 07:04):

[Quoting…]

Thank you! I'll try it！

Flo (Florent Schaffhauser) (Aug 09 2023 at 08:26):

There is also the type Vector ℝ n, whose terms are lists of real numbers, that have length n. docs#Vector

Eric Wieser (Aug 09 2023 at 08:38):

It's very unlikely that you want that type

Flo (Florent Schaffhauser) (Aug 09 2023 at 10:15):

OK, so democratically I am wrong :-) But I cannot really see why it is unlikely that one might want that type.

Of course I do not know what the OP had in mind, whether they wanted R^n with its canonical structure of Euclidean space, or just n-tuples of real numbers. Would you agree in that case that this is the type to look at? Or would you recommend something like Fin n → \R instead?.

But it sounded to me that the next question that may come to mind might be how to define C^n then Q^n, then (Z/pZ)^n etc. So docs#EuclideanSpace might not be the ideal starting point.

I am just trying to understand why you think it is unlikely that the Vector \R n type might be helpful :sweat_smile:

Eric Wieser (Aug 09 2023 at 10:21):

Flo (Florent Schaffhauser) said:

Of course I do not know what the OP had in mind, whether they wanted R^n with its canonical structure of Euclidean space, or just n-tuples of real numbers. Would you agree in that case that this is the type to look at?

Even then, probably no. Chances are even if you don't want the metric space structure of docs#EuclideanSpace, you still want basic elementwise addition of tuples, which you do not get with docs#Vector.

Or would you recommend something like Fin n → \R instead?.

Yes, this is reasonable; you just have to avoid the trap that norm ![3, 4] = 4 not 5!

But it sounded to me that the next question that may come to mind might be how to define C^n then Q^n, then (Z/pZ)^n etc. So docs#EuclideanSpace might not be the ideal starting point.

docs#EuclideanSpace already works for $\mathbb{C}^n$. Probably this is an argument that EuclideanSpace should be generalized to allow $\mathbb{Q}$ too... (Edit: it doesn't permit a real-vector-space structure, so you can't normalize vectors)

Moritz Doll (Aug 09 2023 at 14:29):

PiLp should work for Fin n \to F as long as F has a metric or a norm.

Last updated: Dec 20 2023 at 11:08 UTC