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?



Constructive version of Hilbert Projection Theorem
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](https://en.m.wikipedia.org/wiki/Hilbert_projection_theorem) on the theorem shows, the $s\_n$ are a Cauchy sequence and their limit is the desired point.


