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
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
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):
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