R^n and convex analysis

Stream: maths

[Jeremy Avigad]

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]

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]

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]

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

[Kevin Buzzard]

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"