# Zulip Chat Archive

## Stream: maths

### Topic: R^n and convex analysis

#### Jeremy Avigad (Jul 21 2019 at 16:28):

Is there a definition of `ℝ^n`

as a vector space in the library? I didn't see one, but I'll apologize in advance if I did not look hard enough.

There are lots of possible representations: `vector ℝ n`

, `fin n → ℝ`

, more generally `σ → ℝ`

with `σ`

a `fintype`

, a recursively-defined iterated product, etc. Ultimately, I want it for convex analysis, which means that I need something that will work with matrices but can can also be instantiated as a normed space. (And I guess we will eventually have to grapple that there are various equivalent norms -- either the l1 or l2 norm will work.) That seems to speak for using `σ → ℝ`

with `σ`

a `fintype`

.

Has anyone already done something along these lines? If not, what should I do?

#### Chris Hughes (Jul 21 2019 at 16:34):

If you're making heavy use of matrices, one option is an n by 1 matrix. That's what I've been using. I'm even using 1 by 1 matrices.

#### Jeremy Avigad (Jul 21 2019 at 16:47):

Thanks. Given `f : σ → ℝ`

, we can use `matrix.col f`

and `matrix.row f`

to get an n by 1 matrix and a 1 by n matrix, respectively. And there are already casts, I think, from `fin n → ℝ`

to and from `vector ℝ n`

. I think the type `σ → ℝ`

is already a vector space. *And* the norms on `σ → ℝ`

are special cases of the L1 and L2 norms in measure theory (now that we have integration!). So all that also speaks to using `σ → ℝ`

as the main representation: it is convenient to get to the others.

#### Jan-David Salchow (Jul 21 2019 at 18:39):

@Kevin Buzzard, this is the same issue as with localisation, right? What would the predicate be?

#### Kevin Buzzard (Jul 21 2019 at 18:59):

Well there's the standard universal property, which will involve quantifying over universes, and then at least one concrete one which have this property, of the form "this list of size n is a basis"

Last updated: May 06 2021 at 18:20 UTC