Sobolev characterization by bounded difference quotients (source code)

= Sobolev characterization by bounded difference quotients
{title2=$f\in H^1(\mathbb R)\iff f\in L^2,\;\sup_{0<|h|<1}\|D_hf\|_2<\infty$}

For $f\in H^1(\mathbb R)$, its <difference quotient> equals $D_hf=\int_0^1f'(\cdot+\theta h)\,d\theta$ in <L2 space>. Thus $\|D_hf\|_2\leq\|f'\|_2$, and <translation of a function> gives $D_hf\to f'$ in <L2 space>. Conversely, bounded difference quotients have a weakly convergent subsequence as $h\to0$. Against a <test function>, $\int D_hf\,v\to-\int f v'$, so that weak limit is the <weak derivative> of $f$. It lies in <L2 space>, which is precisely the <first-order Sobolev space> condition.