[proofplan] We prove the algebra property for integer $s = k > n/2$ using the Leibniz rule and the [Sobolev embedding into $L^\infty$](/theorems/226). For each multi-index $\alpha$ with $|\alpha| \le k$, the Leibniz rule expands $\partial^\alpha(fg)$ into a sum of products $(\partial^\beta f)(\partial^{\alpha-\beta}g)$. In each such product, at least one factor has fewer than $k/2$ derivatives, hence embeds into $L^\infty$; the other factor is controlled in $L^2$ by the $H^k$ norm. Summing over all multi-indices yields the bilinear estimate. [/proofplan] [step:Obtain $L^\infty$ control from the Sobolev embedding] Since $k > n/2$, the [Sobolev embedding](/theorems/226) gives $H^k(\mathbb{R}^n) \hookrightarrow L^\infty(\mathbb{R}^n)$: there exists a constant $C_{n,k} > 0$ such that \begin{align*} \|f\|_{L^\infty} &\le C_{n,k}\,\|f\|_{H^k}, \qquad \|g\|_{L^\infty} \le C_{n,k}\,\|g\|_{H^k} \end{align*} for all $f, g \in H^k(\mathbb{R}^n)$. [/step] [step:Apply the Leibniz rule to $\partial^\alpha(fg)$] For each multi-index $\alpha$ with $|\alpha| \le k$, the Leibniz rule gives \begin{align*} \partial^\alpha(fg) &= \sum_{\beta \le \alpha} \binom{\alpha}{\beta}\,(\partial^\beta f)\,(\partial^{\alpha-\beta}g). \end{align*} Taking $L^2$ norms and applying the triangle inequality: \begin{align*} \|\partial^\alpha(fg)\|_{L^2} &\le \sum_{\beta \le \alpha} \binom{\alpha}{\beta}\,\|(\partial^\beta f)\,(\partial^{\alpha-\beta}g)\|_{L^2}. \end{align*} [/step] [step:Bound each Leibniz term by pairing $L^2$ and $L^\infty$ factors] Fix $\beta \le \alpha$ with $|\alpha| \le k$. Since $|\beta| + |\alpha - \beta| = |\alpha| \le k$, at least one of $|\beta|$ or $|\alpha - \beta|$ is at most $\lfloor k/2 \rfloor$. WLOG suppose $|\alpha - \beta| \le k/2$. The factor $\partial^\beta f$: since $|\beta| \le k$, we have $\partial^\beta f \in H^{k-|\beta|}(\mathbb{R}^n) \subseteq L^2(\mathbb{R}^n)$, and $\|\partial^\beta f\|_{L^2} \le \|f\|_{H^k}$. The factor $\partial^{\alpha-\beta}g$: since $|\alpha - \beta| \le k/2$, the function $\partial^{\alpha-\beta}g \in H^{k-|\alpha-\beta|}(\mathbb{R}^n)$ with $k - |\alpha - \beta| \ge k - k/2 = k/2 > n/2$ (using $k > n/2$). By the [Sobolev embedding](/theorems/226), $\|\partial^{\alpha-\beta}g\|_{L^\infty} \le C\,\|\partial^{\alpha-\beta}g\|_{H^{k-|\alpha-\beta|}} \le C\,\|g\|_{H^k}$. Combining via Hölder with exponents $2$ and $\infty$: \begin{align*} \|(\partial^\beta f)\,(\partial^{\alpha-\beta}g)\|_{L^2} &\le \|\partial^{\alpha-\beta}g\|_{L^\infty}\,\|\partial^\beta f\|_{L^2} \le C\,\|g\|_{H^k}\,\|f\|_{H^k}. \end{align*} [guided] Why does at least one factor embed into $L^\infty$? The key observation is that in any Leibniz term $(\partial^\beta f)(\partial^{\alpha-\beta}g)$, the total number of derivatives is $|\alpha| \le k$, so the derivatives are shared between $f$ and $g$. At least one factor receives at most $k/2$ derivatives, leaving the remaining $k - k/2 = k/2$ derivatives of Sobolev regularity. Since $k/2 > n/4$... but more precisely, the Sobolev regularity of $\partial^{\alpha-\beta}g$ is $k - |\alpha-\beta| \ge k/2 > n/2$, which exceeds the embedding threshold $n/2$. So the [Sobolev embedding](/theorems/226) applies to this factor, placing it in $L^\infty$. The other factor is bounded in $L^2$ by the $H^k$ norm. Multiplying an $L^\infty$ function by an $L^2$ function and applying Hölder gives an $L^2$ bound: \begin{align*} \|(\partial^\beta f)(\partial^{\alpha-\beta}g)\|_{L^2} &\le \|\partial^{\alpha-\beta}g\|_{L^\infty}\,\|\partial^\beta f\|_{L^2} \le C\,\|g\|_{H^k}\,\|f\|_{H^k}. \end{align*} [/guided] [/step] [step:Sum over multi-indices to obtain the algebra estimate] Squaring the Leibniz expansion and summing over all $|\alpha| \le k$: \begin{align*} \|fg\|_{H^k}^2 &= \sum_{|\alpha| \le k} \|\partial^\alpha(fg)\|_{L^2}^2 \le \sum_{|\alpha| \le k} \left(\sum_{\beta \le \alpha} \binom{\alpha}{\beta}\,C\,\|f\|_{H^k}\,\|g\|_{H^k}\right)^2 \le C_{n,k}^2\,\|f\|_{H^k}^2\,\|g\|_{H^k}^2, \end{align*} where $C_{n,k}$ absorbs the finite number of multi-index pairs and binomial coefficients. Taking square roots gives $\|fg\|_{H^k} \le C_{n,k}\,\|f\|_{H^k}\,\|g\|_{H^k}$. [/step]