Sharp radial Dirichlet energy inequality (source code)

= Sharp radial Dirichlet energy inequality
{title2=$\int_0^1[rg'(r)^2+g(r)^2/r]\,dr\geq1$}

For $g(1)=1$ and finite displayed energy, the angular mode $g(r)\cos\theta$ has <Dirichlet energy> equal to $\pi$ times that integral. The <harmonic function> $r\cos\theta$ minimizes the energy with the same boundary data by the <Dirichlet principle>, giving the bound. Finite energy forces $g(r)\to0$ as $r\to0$: Cauchy–Schwarz bounds changes of $g^2$ by twice the product of the two energy tails, so $g^2$ has a limit, and a nonzero limit would make $\int g^2/r$ divergent. Consequently completing the square gives the exact identity $\int_0^1[rg'^2+g^2/r]=1+\int_0^1r(g'-g/r)^2$. Equality occurs exactly for $g(r)=r$. This identity also covers finite-energy functions whose polar expression is not classically smooth at the centre.