2

I have some points $x_1,\dots,x_n$ in $\mathbb{R}^j$. I define the set $C(x_1,\dots,x_n)= \left\{\sum_{i=1}^{n} \lambda_i x_i : \lambda_1+\dots+ \lambda_n = 1, \lambda_i \ge 0 \right\}$. The closure of a set is given by all its cluster points. We call a set $S$ closed if $\overline{S}=S$. I now want to prove constructively, meaning without the use of the law of excluded middle, that the set $C(x_1,\dots,x_n)$ is closed. To this end let $a^{(m)} = (a_1^{(m)},\dots, a_n^{(m)})$ be a converging sequence such that $\sum_{i=1}^{n} a_i^{(m)} = 1$ and $a_i^{(m)} \ge 0$. Obviously we have for the limit $a = (a_1,\dots,a_n)$ of this sequence that $\sum_{i=1}^{n} a_i =1$ and $a_i \ge 0$. Since any converging sequence in $C(x_1,\dots,x_n)$ is of the form $a_1^{(m)}x_1 + \dots+ a_n^{(n)}x_n$ and its limit $a_1 x_1 + \dots + a_n x_n$ is still in $C(x_1,\dots,x_n)$, we get that the set is closed.

However, I have be told that constructively this set is NOT closed. But I don't see any flaws in my prove so I am a little confused.

Hanul Jeon
  • 27,376
  • You need to take a convergent sequence of points in $C(x_1,...,x_n)$ and show that the limit is in $C(x_1,..,x_n)$. You took a sequence of weight vectors and you assumed that sequence of weight vectors converges. It's not the same thing. How do you know that a convergent sequence of points in $C(x_1,...,x_n)$ corresponds to a convergent sequence of weight vectors? – quasi Aug 22 '18 at 18:39
  • @quasi But any sequence in the set is build this way, isn't it? If the sequence in the set is converging the weight vectors have to converge. And the "nods" $x_i$ are fixed anyway. –  Aug 22 '18 at 18:42
  • 1
    If the sequence of weight vectors converges, then the corresponding sequence of points will converge. That's clear. The converse is the issue. You didn't prove it. I suspect that if you try to prove the converse, it won't qualify as a constructive proof. – quasi Aug 22 '18 at 18:44
  • 2
    Your set $C(x_1, \ldots, x_n)$ is called the convex hull of the set of points ${x_1, \ldots, x_n}$. The convex hull of a finite set can be shown to be a polytope, i.e., an intersection of a finite number of closed half-spaces. This can be proved constructively using a quantifier elimination process for real linear arithmetic. As a polytope is easily seen to be closed using constructive methods, I think this leads to a constructive proof of your result. There may be an easier way. – Rob Arthan Aug 22 '18 at 20:11
  • @RobArthan Can you please elaborate how this works? Especially the part where one has to show that the convex hull is a polytope. –  Aug 23 '18 at 09:11
  • Apologies! My suggestion would only work if the $x_i$ were given explicitly (say as rational numbers). It is possible that you could analyse the quantifier elimination process for real arithmetic (not just linear arithmetic) in your particular case and get a proof of your result, but I haven't looked into that myself. The usual proof that convex hulls of finite sets are polytopes goes via the bipolar theorem and takes it as known that the convex hull is closed. (Aside: some authors define polytopes to be convex hulls of finite sets and call what I called polytopes polyhedra.) – Rob Arthan Aug 23 '18 at 19:49
  • Who told you that there isn't a constructive proof? And what was their evidence? – Rob Arthan Aug 23 '18 at 19:51
  • Could the issue be when $C$ has dimension $<n-1$, so that more than one $\lambda$ maps to the same point? It seems like some oracle power might be needed in that case to get a converging sequence of $\lambda$s. – realdonaldtrump Aug 25 '18 at 08:49

0 Answers0