[proofplan]
We show $u \in C^k(\bar{U})$ for every $k \ge 0$ by combining the [Higher Boundary Elliptic Regularity](/theorems/97) theorem with the [Sobolev Embedding Theorem](/theorems/903). For each target differentiability $k$, we choose an integer $m$ large enough that $H^{m+2}(U) \hookrightarrow C^k(\bar{U})$ (which requires $m + 2 > n/2 + k$). Since all data are $C^\infty$, the Higher Boundary Regularity theorem gives $u \in H^{m+2}(U)$, and the Sobolev embedding then gives $u \in C^k(\bar{U})$.
[/proofplan]
[step:Recall the Sobolev embedding into $C^k(\bar{U})$]
By the [Sobolev Embedding Theorem](/theorems/903), if $U \subset \mathbb{R}^n$ is a bounded open set with $C^1$ boundary and $s > n/2 + k$ for non-negative integers $s, k$, then:
\begin{align*}
H^s(U) \hookrightarrow C^k(\bar{U}).
\end{align*}
Every function in $H^s(U)$ admits a representative with continuous derivatives up to order $k$ on $\bar{U}$.
[/step]
[step:For each $k$, choose $m$ and apply the Higher Boundary Regularity theorem]
Fix an arbitrary non-negative integer $k$. Choose any integer $m$ satisfying:
\begin{align*}
m > \frac{n}{2} + k - 2,
\end{align*}
so that $m + 2 > n/2 + k$.
We verify the hypotheses of the [Higher Boundary Elliptic Regularity](/theorems/97) theorem for this $m$:
- $\partial U \in C^\infty$ implies $\partial U \in C^{m+2}$.
- $a_{ij}, b_i, c \in C^\infty(\bar{U})$ implies $a_{ij}, b_i, c \in C^{m+1}(\bar{U})$.
- $f \in C^\infty(\bar{U})$ implies $f \in H^m(U)$.
All hypotheses are satisfied. The theorem gives $u \in H^{m+2}(U)$.
[/step]
[step:Conclude $u \in C^\infty(\bar{U})$]
By the Sobolev embedding with $s = m + 2 > n/2 + k$:
\begin{align*}
u \in H^{m+2}(U) \hookrightarrow C^k(\bar{U}).
\end{align*}
Since $k \ge 0$ was arbitrary:
\begin{align*}
u \in \bigcap_{k=0}^\infty C^k(\bar{U}) = C^\infty(\bar{U}).
\end{align*}
[/step]
