Let $1 \le p < \infty$, $W^{1, p}(\mathbb H^{d})$ be the [[Sobolev Space|Sobolev space]], and $f \in W^{1, p}(\mathbb H^d)$ be a compactly supported function with [[Sobolev Trace Theorem|trace]] zero. > [!theorem] > > There exists $C_p \ge 0$ such that > $ > \int_{\real^{d - 1}} \abs{f(x', x_d)}^p dx' \le C_p x_d^{p - 1}\int_{[0, x_d]}\int_{\real^{d - 1}}\abs{Df(x', t)}^pdx'dt > $ > for almost every $x_d > 0$. > > *Proof*. Let $\seq{f_n} \subset UC_c^1(\mathbb H^d)$ such that $f_n \to f$ in $W^{1, p}(\mathbb H^d)$, and $Tf_n = f_n|_{\partial \mathbb H^d} \to 0$ in $L^p(\partial \mathbb H^d)$. For any $x \in \mathbb R^d$, split $x = (x', x_d)$ with $x' \in \real^{d - 1}$ and $x_d \in \real$. By the [[Mean Value Theorem|mean value theorem]], > $ > \abs{f_n(x', x_d)} \le \abs{f_n(x', 0)} + \int_{[0, x_d]}\abs{\partial^{x_d}f_n(x', t)}dt > $ > Let $q$ be the Hölder conjugate of $p$. By [[Young's Inequality]] and [[Hölder's Inequality]], > $ > \begin{align*} > \abs{f_n(x', x_d)}^p &\le C_p\braks{\abs{f_n(x', 0)}^p + \paren{\int_{[0, x_d]}\abs{\partial^{x_d}f_n(x', t)}dt}^p} \\ > &\le C_p\braks{\abs{f_n(x', 0)}^p + \norm{\one_{[0, x_d]}}_q^p \cdot \norm{\one_{[0, x_d]} \cdot \partial^{x_d}f_n(x', \cdot)}_p^p} > \end{align*} > $ > where $\norm{\one_{[0, x_d]}}_q^p = x_d^{1/q \cdot 1/p} = x_d^{p - 1}$, so > $ > \abs{f_n(x', x_d)}^p \le C_p \braks{\abs{f_n(x', 0)}^p + x_d^{p - 1}\int_{[0, x_d]}\abs{\partial^{x_d}f_n(x', t)}^pdt} > $ > Since $f_n \to f$ in $W^{1, p}$, > $ > \int_{\real}\int_{\real^{d - 1}}\abs{f_n(x', x_d) - f(x', x_d)}^pdx'dx_d \to 0 > $ > as $n \to \infty$, so $\int_{\real^{d - 1}} \abs{f_n(x', x_d) - f(x', x_d)}dx' \to 0$ in $L^1$, and admits a subsequence $\seq{n_k}$ such that $\int_{\real^{d - 1}}\abs{f_{n_k}(x', x_d)}dx' \to \int_{\real^{d - 1}}\abs{f(x', x_d)}dx'$ for almost every $x_d > 0$. On the other hand, $Tf_n \to 0$ in $L^p$, so sending $k \to \infty$ yields > $ > \int_{\real^{d - 1}} \abs{f(x', x_d)}^p dx' \le C_p x_d^{p - 1}\int_{[0, x_d]}\int_{\real^{d - 1}}\abs{Df(x', t)}^pdx'dt > $ > for almost every $x_d$. > [!theorem] > > Let $W^{1, p}_c(\mathbb H^d)$ be the space of functions in $W^{1, p}(\mathbb H^{1, p})$, compactly supported in the *interior* of $\mathbb H^d$. For any $\eps > 0$, there exists $g \in W_c^{1, p}(\mathbb H^d)$ such that $\norm{f - g}_{W^{1, p}}j < \eps$. > > In other words, $W_c^{1, p}(\mathbb H^d)$ is [[Dense|dense]] in the kernel of the trace operator. In particular, since $C_c^\infty((\mathbb H^d)^o)$ is dense in $W_c^{1, p}$, $\ker(T) \subset W^{1, p}_0(\mathbb H^d)$. > > *Proof*. Let $\zeta \in C_c^\infty(\mathbb H, [0, 1])$ be a [[Smooth Bump Function|smooth bump function]] such that $\zeta|_{[0, 1]} = 1$ and $\supp{\zeta} \subset [0, 2]$. Identify > $ > \zeta: \mathbb H^n \to \real \quad (x', x_d) \mapsto \zeta(x_d) > $ > Let $t > 0$, $\zeta_t(x) = \zeta(tx)$, $f_t = f \cdot (1 - \zeta_t)$, then $f_t \in W_c^{1, p}(\mathbb H^d)$ with > $ > \norm{f_t - f}_p \le \norm{\one_{\real^{d - 1} \times [0, 2/t]} \cdot f}_p \to 0 > $ > as $t \to \infty$. On the other hand, > $ > \begin{align*} > \partial^{x_d}f_t &= \partial^{x_d} f \cdot(1 - \zeta_t) - tf(\partial^{x_n}\zeta)_t \\ > \partial^{x'}f_t &= \partial^{x'} f\cdot (1 - \zeta_t) > \end{align*} > $ > where $(\partial^{x_n}\zeta)_t(x) = (\partial^{x_n}\zeta)(tx)$. Passing through equivalent norms, > $ > \norm{Df_t - Df}_p \le C\braks{\norm{\partial^{x_d}(f_t - f)}_p + \norm{\partial^{x'}(f_t - f)}_p} > $ > with > $ > \begin{align*} > \norm{\partial^{x'}(f_t - f)}_p &\le \norm{\one_{\bracs{x_d \in [0, 2/t]}} \cdot \partial^{x'}f}_p\\ > \norm{\partial^{x_n}(f_t - f)}_p &\le \norm{\zeta_t \partial^{x_d} f}_p + \norm{tf \partial^{x_n}\zeta}_p \\ > &\le \norm{\one_{\bracs{x_d \in [0, 2/t]}} \cdot \partial^{x_d}f}_p + \norm{\partial^{x_d}\zeta}_u \cdot \norm{\one_{\bracs{x_d \in [0, 2/t]}} \cdot tf}_p > \end{align*} > $ > where $\normn{\one_{\bracs{x_d \in [0, 2/t]}} \cdot \partial^{x'}f}_p \to 0$ as $t \to \infty$. On the other hand, by the previous theorem, > $ > \int_{\real^{d - 1}}\abs{f(x', x_d)}^p dx' \le C_p x_d^{p - 1}\int_{[0, x_d]}\int_{\real^{d - 1}}\abs{Df(x', s)}^pdx'ds > $ > Integrating on the last variable gives > $ > \begin{align*} > \norm{\one_{\bracs{x_d \in [0, 2/t]}} \cdot f}_p^p &\le C_p\int_{[0, 2/t]} x_d^{p - 1}\int_{[0, x_d]}\int_{\real^{d - 1}}\abs{Df(x', s)}^pdx'dsdx_d\\ > &\le C_p\int_{[0, 2/t]} x_d^{p - 1}\int_{[0, 2/t]}\int_{\real^{d - 1}}\abs{Df(x', s)}^pdx'dsdx_d\\ > &\le C_p\braks{\int_{[0, 2/t]} x_d^{p - 1}dx_d} \cdot \braks{\int_{[0, 2/t]}\int_{\real^{d - 1}}\abs{Df(x', s)}^pdx'ds}\\ > &\le C_p x_d^p \cdot \norm{\one_{\bracs{x_d \in [0, 2/t]}} \cdot Df}_p^p \\ > \norm{\one_{\bracs{x_d \in [0, 2/t]}} \cdot tf}_p&\le C_p^{1/p} \norm{\one_{\bracs{x_d \in [0, 2/t]}} \cdot Df}_p > \end{align*} > $ > which goes to $0$ as $t \to \infty$ as well.