Uniformly convex Banach spaces are reflexive -- constructively (Q2856637)

Let \(X\)~be a real Banach space, or more generally a so-called complete quasinormed space with family of seminorms \((\|~\|_i)_{i\in I}\): for each~\(x\in X\), the set \(\{\|x\|_i:i\in I\}\) is bounded. In constructive mathematics, the existence of the supremum of this set is an hypothesis; if it holds, then the element \(x\) is called normable. The dual \(X^*\) of \(X\) is the space of linear functionals \(u\) on \(X\) with seminorms \(\|u\|_x=\|u(x)\|\) indexed by the unit ball \(B_X=\{x\in X:\forall i\in I(\|x\|_i\leq1)\}\). The bidual \(X^{**}\) is defined in the same way with seminorms indexed by \(f\in B_{X^*}\); every \(x\in X\) defines a linear functional \(\hat x\in X^{**}\) by \(\hat x(f)=f(x)\), and \(X\) is called reflexive if each normable element \(F\) of \(X^{**}\) has the form~\(F=\hat x\).NEWLINENEWLINEThe authors isolate the following hypothesis: \(X\) is pliant if for each \(x\in X\), each \(i\in I\) and each \(\varepsilon>0\), there exists \(f\in B_{X^*}\) such that \(\hat x(f)>\|x\|_i-\varepsilon\). This is true in classical mathematics; in constructive mathematics, it is not known whether it is true in general, but it is the case if \(X\) is separable (or ``quasi-separable'') or has Gâteaux differentiable norm. Let us recall that \(X\) is uniformly convex if for each \(\varepsilon>0\), there exists \(\delta\in(0,1)\) such that if \(x,y\in B_X\) and there exists \(i\in I\) such that \(\|x-y\|_i>\varepsilon\), then \(\|{1\over 2}(x+y)\|_i<1-\delta\) for all \(i\).NEWLINENEWLINEThe main theorem of this article is the Milman-Pettis theorem: if \(X\) is uniformly convex and pliant, then \(X\) is reflexive. The proof is a constructive modification of \textit{J. R. Ringrose}'s [J. Lond. Math. Soc. 34, 92 (1959; Zbl 0083.10302)] classical proof by contradiction.