R^n

Stream: new members

[Anatole Dedecker]

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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Anatole Dedecker]

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

[Anatole Dedecker]

But yeah I told him about hidden isomorphisms and all

[Kevin Buzzard]

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]

So this shows that your definition is a better implementation

[Adam Topaz]

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]

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

[Moritz Doll]

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

[tsuki hao]

[Quoting…]

Thank you! I'll try it！

[Flo (Florent Schaffhauser)]

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

[Eric Wieser]

It's very unlikely that you want that type

[Flo (Florent Schaffhauser)]

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]

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]

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