Constructive version of Hilbert Projection Theorem

Question

I am looking at the Hilbert Projection Theorem, which states that every non-empty closed convex set in a Hilbert space admits a unique element that has the minimum norm in the set.

The proof involves taking the infimum of the norm on the set and constructing a seqeuence in the set with decreasing norm. However, this proof does not give us an explicit criterian or method to find a minimum element norm.

Finding this norm is easy in the cases when the closed convex set is a subspace or a sphere, but it may not be clear in other cases. For example if $H,G$ are Hilbert spaces and $A:H \rightarrow G$ is a bounded linear map, then for a closed convex set $C$ in $G$, $A^{-1}(C)$ may be a very strange set (depending on how $A$ is defined). In this case, are there any better results than the Hilbert Projection Theorem?

Answer 1

A constructive equivalent might be: Any located closed convex set has a unique element of minimal norm. This is roughly the version in chapter 7, problem 11 of Bishop and Bridges’s 1985 Constructive Analysis.

Here, locatedness is a standard constructive assumption, meaning that the distance to the set exists, or is calculable. Unpacking further, this means that for any $p$, there is a sequence $s_n$ of points in $S$ where the distances $d(p,s_n)$ converge to a number less than or equal to any $d(p,s)$. Then, as the Wikipedia article on the theorem shows, the $s_n$ are a Cauchy sequence and their limit is the desired point.