In the development of gradient-flow theory (in Hilbert-space $H$), we soon stumble on the question whether the function $u \mapsto \varphi[u]:=\frac{1}{2}\|u\|^2+I[u]$ -where $I:H \to \mathbb{C}$ is convex , proper and lower semi-continuous- has a a finite infimum and a unique minimizer $u_{\min}\in H$. To answer this question affirmatively, Evans (p.524, allegedly borrowed from Brezis) invokes Mazur's theorem/Mazur's lemma via a lengthy argument. Is that line of thinking efficient? Can we in stead not immediately apply the Hahn-Banach theorem to $I$ to show that $\varphi$ is bounded below and $\varphi^{-1}(\text{bounded set}\subset \mathbb{C})=\text{bounded set}\subset H$. Next, if we define a sequence $(u_k)_k$ so that $\varphi[u_k] \to \inf I$ sufficiently fast, I think one easily obtains that $(u_k)_k$ is a Cauchy-sequence and therefore convergent (to $u_{\min}$).
For this alternative argument, we of course need the Hahn-Banach theorem and hence the axiom of choice. So perhaps Evans/Brezis prefer their line since it possibly avoids invoking the axiom of choice?
Q1: Are the Mazur theorem/lemma true independent of the axiom of choice?
Q2: Can I prove that $\varphi$ (defined above) has a finite infimum and a unique minimizer without the axiom of choice?
The proof of Mazur's lemma also relies on Hahn-Banach (separation) theorem.
In Hilbert spaces the proof of Hahn-Banach does not need the axiom of choice: separating hyperplanes can be constructed by means of geometric considerations (projections ).