Bounded isolated-point removability for weak first derivatives (source code)

= Bounded isolated-point removability for weak first derivatives
{title2=$n\geq2$}

A bounded function which is $C^1$ away from one point in dimension $n\geq2$, and whose classical gradient is locally integrable across that point, has that gradient as its <weak derivative>. Cut a <test function> off within distance $\varepsilon$ of the point. The error from differentiating the cutoff is bounded by $C\|u\|_\infty\varepsilon^{n-1}$ and vanishes. The other terms converge by local integrability. In dimension one the <Heaviside step function> is a counterexample: its classical derivative off the point is zero, but its distributional derivative is a <Dirac delta>.