A lemma in functional analysis about distance I want to prove the following result, I know it is correct:
If $X$ is a Banach Space, $G \subset X$ is a closed linear subspace, $f \in X^*$ is a linear functional, then we have:
\begin{equation*}
\text{dist}(f,G^\perp) = \sup_{\|x\| \leq 1, x \in G}\left<f,x \right>
\end{equation*}
How should we do this? Is $G$ necessarily a closed subspace?
 A: This is a nice exercise on quotient spaces and duality. We will need these results:

*

*$\operatorname{dist}(f,G^\perp) = ||[f]||_{X^*/G^\perp}$.

*$X^*/G^\perp$ is isometric to $G^*$.

The first is a standard result (sometimes even taken as a definition of norm on a quotient space).
For the second one, consider the restriction mapping $R:X^* \rightarrow G^*$, $R(x^*) = x^* \restriction G$. Then $\operatorname{Ker} R = G^\perp$. Hence, we can define $\tilde{R}: X^*/G^\perp \rightarrow G^*$, the factorization of $R$, by $\tilde{R}([x^*]) = R(x^*)$. Now we just need to check that $\tilde{R}$ is an onto isometry, which is quite straightforward, we just need the Hahn-Banach theorem to prove it is onto.
Now, we have
$$\operatorname{dist}(f,G^\perp) = ||[f]||_{X^*/G^\perp} = ||\tilde{R}([f])||_{G^*} = ||f \restriction G||_{G^*} = \sup_{\|x\| \leq 1, x \in G}\left<f,x \right>.$$
A: It is clear that $$\text{dist}(f,G^\perp)=\inf_{g\in G^\perp}\sup_{\lVert x \rVert \leq 1}\lvert f(x)-g(x)\rvert\geq \inf_{g\in G^\perp}\sup_{x\in G, \lVert x \rVert \leq 1}\lvert f(x)-g(x)\rvert=\sup_{x\in G, \lVert x \rVert \leq 1}\lvert f(x)\rvert.$$
On the other hand consider $f\rvert_{G}$. By Hahn-Banach extension theorem, there exist an extension of $f$, $\tilde{f}$, such that $\lVert \tilde{f} \rVert=\sup_{x\in G, \lVert x \rVert \leq 1 } \lvert f(x) \rvert$. Notice now that $f-\tilde{f}\in G^\perp$. Thus we also have $$\text{dist}(f,G^\perp)=\inf_{g\in G^\perp}\sup_{\lVert x \rVert \leq 1}\lvert f(x)-g(x)\rvert\leq \sup_{\lVert x \rVert \leq 1}\lvert f(x)-f(x)+\tilde{f}(x)\rvert=\sup_{x\in G, \lVert x \rVert \leq 1} \lvert f(x) \rvert.$$
Which proves the claim.
