[proofplan]
Subtract the prescribed boundary extension to reduce to homogeneous Dirichlet data. The new unknown satisfies a Poisson equation with Holder continuous right-hand side and zero boundary trace. We then apply the standard local Schauder estimates: the interior estimate on balls away from the boundary and the flat-boundary Schauder estimate after straightening the boundary. A finite cover of $\overline U$ and a [partition of unity](/page/Partition%20of%20Unity) assemble these local bounds into a global $C^{2,\alpha}$ estimate. Finally we add back the extension $G$ and absorb its lower-order norms into $\|G\|_{C^{2,\alpha}(\overline U)}$.
[/proofplan]
[step:Reduce to zero boundary data]
Define
\begin{align*}
v := u-G.
\end{align*}
Since $u|_{\partial U}=\gamma$ and $G|_{\partial U}=\gamma$, the function $v$ has zero continuous boundary trace on $\partial U$. Moreover, in $U$,
\begin{align*}
-\Delta v = -\Delta u+\Delta G = f+\Delta G.
\end{align*}
Set
\begin{align*}
h := f+\Delta G.
\end{align*}
Because $f\in C^{0,\alpha}(\overline U)$ and $G\in C^{2,\alpha}(\overline U)$, we have $h\in C^{0,\alpha}(\overline U)$ and
\begin{align*}
\|h\|_{C^{0,\alpha}(\overline U)}
\leq \|f\|_{C^{0,\alpha}(\overline U)}+C_0\|G\|_{C^{2,\alpha}(\overline U)}
\end{align*}
for a constant $C_0=C_0(n)>0$.
[guided]
The boundary datum is handled by subtracting a fixed extension. This is why the theorem assumes the existence of $G\in C^{2,\alpha}(\overline U)$ with $G=\gamma$ on $\partial U$. After setting $v=u-G$, the boundary condition becomes homogeneous:
\begin{align*}
v|_{\partial U}=0.
\end{align*}
The equation changes only by the known term $\Delta G$:
\begin{align*}
-\Delta v=f+\Delta G.
\end{align*}
The right-hand side remains Holder continuous because second derivatives of a $C^{2,\alpha}$ function are $C^{0,\alpha}$. Thus it is enough to prove the global Schauder estimate for the zero-boundary problem with right-hand side $h$.
[/guided]
[/step]
[step:State the local Schauder estimates used on the cover]
We use two standard local estimates. First, the [Schauder Interior Estimate](/theorems/4947), applied to the constant-coefficient operator $-\Delta$, says that whenever $\overline W\subset V\subset\subset U$,
\begin{align*}
\|v\|_{C^{2,\alpha}(\overline W)}
\leq C_{\mathrm{int}}\left(\|h\|_{C^{0,\alpha}(\overline V)}+\|v\|_{C^0(\overline V)}\right).
\end{align*}
Second, the flat-boundary Schauder estimate for the Dirichlet Laplacian says the following. If $Q^+=B(0,1)\cap\{x_n>0\}$, $Q_{1/2}^+=B(0,1/2)\cap\{x_n>0\}$, $w\in C^0(\overline{Q^+})\cap C^2(Q^+)$, $w=0$ on $B(0,1)\cap\{x_n=0\}$, and $-\Delta w=q$ in $Q^+$ with $q\in C^{0,\alpha}(\overline{Q^+})$, then
\begin{align*}
\|w\|_{C^{2,\alpha}(\overline{Q_{1/2}^+})}
\leq C_{\partial}\left(\|q\|_{C^{0,\alpha}(\overline{Q^+})}+\|w\|_{C^0(\overline{Q^+})}\right),
\end{align*}
where $C_{\partial}$ depends only on $n$ and $\alpha$. Under a $C^{2,\alpha}$ boundary-flattening diffeomorphism, the Laplacian becomes a uniformly [elliptic operator](/page/Elliptic%20Operator) with $C^{0,\alpha}$ coefficients, and the same estimate holds with a constant depending on the chart norms and ellipticity constants.
[/step]
[step:Apply the estimates on a finite cover]
Since $\overline U$ is compact and $\partial U$ is $C^{2,\alpha}$, the [Straightening the Boundary Theorem](/theorems/50) gives finitely many boundary charts together with finitely many interior balls whose smaller subpatches cover $\overline U$. Choose a smooth partition of unity $\{\zeta_j\}_{j=1}^N$ subordinate to these patches, with all chart norms and cutoff norms fixed once and for all by $U$.
On an interior patch, the preceding interior estimate gives
\begin{align*}
\|\zeta_j v\|_{C^{2,\alpha}}
\leq C_j\left(\|h\|_{C^{0,\alpha}(\overline U)}+\|v\|_{C^0(\overline U)}\right).
\end{align*}
On a boundary patch, straighten the boundary and apply the flat-boundary estimate to the localized pullback of $\zeta_j v$. The commutator terms created by differentiating $\zeta_j$ contain only derivatives of $v$ of order at most one. The standard interpolation step in Schauder theory absorbs these lower-order local terms into the left-hand side after passing from each chart patch to its fixed smaller subpatch, leaving
\begin{align*}
\|\zeta_j v\|_{C^{2,\alpha}}
\leq C_j\left(\|h\|_{C^{0,\alpha}(\overline U)}+\|v\|_{C^0(\overline U)}\right).
\end{align*}
The constants $C_j$ depend only on $n$, $\alpha$, the chosen chart, and the cutoff. Since the cover is finite and depends only on $U$, summing the finitely many estimates gives
\begin{align*}
\|v\|_{C^{2,\alpha}(\overline U)}
\leq C_1\left(\|h\|_{C^{0,\alpha}(\overline U)}+\|v\|_{C^0(\overline U)}\right),
\end{align*}
where $C_1$ depends only on $U$, $n$, and $\alpha$.
[/step]
[step:Return to the original unknown]
Since $v=u-G$,
\begin{align*}
\|v\|_{C^0(\overline U)}
\leq \|u\|_{C^0(\overline U)}+\|G\|_{C^0(\overline U)}
\leq \|u\|_{C^0(\overline U)}+\|G\|_{C^{2,\alpha}(\overline U)}.
\end{align*}
Combining this with the estimate for $h=f+\Delta G$ gives
\begin{align*}
\|v\|_{C^{2,\alpha}(\overline U)}
\leq C_2\left(\|u\|_{C^0(\overline U)}
+\|f\|_{C^{0,\alpha}(\overline U)}
+\|G\|_{C^{2,\alpha}(\overline U)}\right).
\end{align*}
Finally, $u=v+G$, so
\begin{align*}
\|u\|_{C^{2,\alpha}(\overline U)}
\leq \|v\|_{C^{2,\alpha}(\overline U)}+\|G\|_{C^{2,\alpha}(\overline U)}.
\end{align*}
After increasing the constant, this is exactly
\begin{align*}
\|u\|_{C^{2,\alpha}(\overline U)}
\leq C\left(\|u\|_{C^0(\overline U)}+\|f\|_{C^{0,\alpha}(\overline U)}+\|G\|_{C^{2,\alpha}(\overline U)}\right).
\end{align*}
In particular $u\in C^{2,\alpha}(\overline U)$.
[guided]
The final step only translates the homogeneous estimate back to the original boundary data. Every appearance of $G$ is controlled by its $C^{2,\alpha}$ norm, and the $C^0$ size of $v$ is bounded by the $C^0$ size of $u$ plus the $C^0$ size of $G$. Since the theorem allows the final constant to depend on $U$, $n$, and $\alpha$, all constants from the finite cover, flattening maps, cutoffs, and local estimates are absorbed into one constant $C$.
[/guided]
[/step]
