$H^{\frac12}$ norm and preimage via the trace operator In this article, at one point, a chain of (in)equalities much like the following is found:
$$\|u\|_{H^1(D_1)}=\|f\|_{H^1(\partial D_1)}\leq C\|f\|_{H^{\frac12}(\partial D_1)},$$
where $u\in H^1(D_1)$ is the harmonic extension of $f\in H^1(\partial D_1)$ and $D_1$ is the unit disk in $\mathbb R^2$. Now, using Proposition 2.2 on p. 8 here in a local way, I can convince myself that the inequality holds. However, the equality is unjustified. Now, being $u$ harmonic, the Dirichlet principle tells us that:
$$\|u\|_{H^1(D_1)}=\inf_{\substack{v\in H^1(D_1) \\ v|_{\partial D_1}=f}}\|v\|_{H^1(D_1)},$$
and this Math SE post suggests $\|u\|_{H^{\frac12}(\partial D_1)}$ equals the latter expression, which would allow us to conclude the chain works. However, I cannot seem to find a proof of this equality. So how is it proved?
PS I am happy with a reference as long as it is available online. Google books are, however, best avoided, since I have the impression that at least half the times the page(s) needed are not in the preview.

Expand $f$ into a Fourier series, $f(e^{it})=\sum_{n\in \mathbb{Z}} c_n e^{in t}$. The harmonic extension is 
$$
u(re^{it})= \sum_{n\in \mathbb{Z}} r^{|n|} c_n e^{in t}
$$
The gradient squared is $u_r^2 + u_t^2/r^2$, which ends up being
$$
|\nabla u(re^{it})|^2 = 
\left|\sum_{n\ne 0} |n| r^{|n|-1} c_n e^{in t}\right|^2 + 
\left|\sum_{n\ne 0} r^{|n|-1} c_n (in)e^{in t}\right|^2
$$
Integrating over $t$ and using Parseval, we get 
$$
4\pi  \sum_{n\ne 0}n^2r^{2(|n|-1)} |c_n|^2 
$$
and then integrating  $\int_0^1 \cdots r\,dr$, 
$$
4\pi  \sum_{n\ne 0}n^2 \frac{1}{2|n|}|c_n|^2 = 2\pi  \sum_{n\ne 0}|n||c_n|^2
$$
This is the $H^{1/2}$ seminorm on the circle, shown to be equal to the $H^1$ seminorm of the harmonic extension. (In both cases, constants get 0).
