Constructivity of two problems on a standard simplex?

Question

Maximizing a hyperplane $\sum_i a_ix_i$ where $a_i\in\mathbb R$ and each $a_i$ are fixed and non-negative and $x_i$ are variables over a standard simplex $\sum_i x_i\leq 1$ with $0\leq x_i$ always produces a vertex point on the simplex and maximization corresponds to $\max_i a_i$.

1. In infinite dimensions is such a proof considered constructive or does it hold only in classical logic? It seems that we would have to show that at maximizing point there is an $i\in\mathbb N$ such that $x_i=1$ holds and for that perhaps is it possible we cannot do this without invoking LLPO?

Suppose we are looking for a $0/1$ vector in integers (not reals as in 1.) on the standard simplex and we know the optimal vector has either sum of even coordinates summing to $1$ or odd coordinates summing to $1$ then in finite dimensions it is a process of enumerating vertices.

2. In infinite dimensions is such a proof considered constructive or does it hold only in classical logic? It seems that we would have to show that at optimizing point there is an $i\in\mathbb N$ such that $x_i=1$ holds and for that perhaps is it possible we cannot do this without invoking LLPO?

In general is the proofs of optimization over infinite dimensions considered constructive?

3a. How about when each $a_i$ are fixed and positive?

3b. How about when each $a_i$ are fixed and distinct and non-negative thus guaranteeing an unique vertex point?

3c. How about when each $a_i$ are fixed and distinct and positive thus guaranteeing an unique vertex point?

Answer 1

You make an erroneous assumption in your question, as already in dimension 1 you need LLPO to know that the maximum is actually attained at some point.

We work constructively.

Theorem: LLPO is equivalent to the statement that every affine map $[0,1] \to \mathbb{R}$ attains its maximum

Proof. The general form of an affine map on $[0,1]$ is $f_{a,b}(x) = a \cdot (1 - x) + b \cdot x$. Suppose then that for every such $f_{a,b}$ there exists $x_0 \in [0,1]$ such that $f_{a,b}(x) \leq f_{a,b}(x_0)$ for all $x \in [0,1]$.

Let us first show that LLPO implies attainment of maximum. Given any $f_{a,b}$, by LLPO either $a \leq b$ or $b \leq a$:

• If $a \leq b$ then the maximum of $f_{a,b}$ is attained at $x_0 = 1$.
• If $b \leq a$ then the maximum of $f_{a,b}$ is attained at $x_0 = 0$.

The converse is more interesting. First note that the following holds: if $f_{a,b}(0) \leq f_{a,b}(t)$ for some $t > 0$ then $f_{a,b}(0) \leq f_{a,b}(1)$. Similarly, if $f_{a,b}(t) \geq f_{a,b}(1)$ for some $t < 1$ then $f_{a,b}(0) \geq f_{a,b}(1)$.

Consider any two reals $a, b \in \mathbb{R}$. We shall decide $a \leq b \lor b \leq a$, which implies LLPO. By assumption, the map $f_{a,b}$ attains its maximum at some $x_0 \in [0,1]$. Either $x_0 < 2/3$ or $x_0 > 1/3$:

• If $x_0 > 1/3$ then from $f(0) \leq f(x_0)$ it follows that $a = f(0) \leq f(1) = b$.
• If $x_0 < 2/3$ then from $f(x_0) \geq f(1)$ it follows that $a = f(0) \geq f(1) = b$. $\Box$

Of course, since affine maps are very simple, the maximal value of $f_{a,b}$ exists, but the above argument shows it takes LLPO to know where it is attained.