Smooth-neighborhood density in H1 of a simplex

Given: Countable Choice, a nondegenerate simplex $K$, a real Sobolev class $u\in W^{1,2}(K)$, and $\epsilon >0$.

Countable Choice is inherited through the published Sobolev, density, change-of-variables, and mollification interfaces. (The Axiom of Countable Choice (${\mathrm{A}\mathrm{C}}_{\omega }$))

$W^{1,2}(K)$ consists of real $L^2$ classes with first weak derivatives in $L^2(K)$. (Integer-order Sobolev spaces and their norms)

For every $g\in L^2({\mathbb{R}}^d)$ and $\eta >0$, some $\varphi \in C_c^{\mathrm{\infty }}({\mathbb{R}}^d)$ satisfies $\mathrm{\parallel }g-\varphi {\mathrm{\parallel }}_2<\eta$. (Smooth compactly supported functions of an open set are dense in $L^2$)

An invertible linear map scales Lebesgue measure by its absolute determinant, and translations preserve measurability and measure. Thus an affine map $T(x)=Ax+b$ satisfies $\mathrm{\mid }T(E)\mathrm{\mid }=\mathrm{\mid }\det A\mathrm{\mid }\mathrm{\mid }E\mathrm{\mid }$. Applying this identity to indicator functions, then nonnegative simple functions and their increasing approximations, and finally positive and negative parts gives ${\int }_{T(E)}f(y)dy=\mathrm{\mid }\det A\mathrm{\mid }{\int }_{E}f(T(x))dx$ for integrable real $f$ (and for nonnegative measurable $f$). Null sets are preserved in both directions, so composition also respects almost-everywhere classes. (A linear map $T$ of ${\mathbb{R}}^n$ sends Lebesgue measurable sets to Lebesgue measurable sets, with ${\lambda }_n(T[E])=\mathrm{\mid }\det T\mathrm{\mid }{\lambda }_n(E)$ when $T$ is invertible and $T[E]$ Lebesgue null when it is not, Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation)

The smooth-bump lemma gives $\chi \in C_c^{\mathrm{\infty }}(B_{1\mathrm{/}2}(0))$ with $0\le \chi \le 1$ and $\chi =1$ on ${\bar{B}}_{1\mathrm{/}4}(0)$. Its support has finite measure by Lebesgue measure is sigma-finite, and every metrically bounded subset of ${\mathbb{R}}^n$ has finite outer measure, while $B_{1\mathrm{/}4}(0)$ contains the cube $(-1\mathrm{/}(8\sqrt{d}),1\mathrm{/}(8\sqrt{d}){)}^d$, whose measure is positive by A box in ${\mathbb{R}}^n$ with parameters $a_i\le b_i$ is Lebesgue measurable of measure ${\prod }_{i<n}(b_i-a_i)$, whichever of its faces are included. Thus $m:=\int \chi$ is finite and positive. The normalized bump $\rho :=\chi \mathrm{/}m$ has unit mass and support in $B_1(0)$; its rescalings are an $L^1$ approximate identity by A unit-mass smooth bump generates an $L^1$ approximate identity. (A smooth bump between concentric Euclidean balls, The mollifier family generated by a unit-mass smooth bump)

For every $g\in L^2({\mathbb{R}}^d)$, $\mathrm{\parallel }{\rho }_{\eta }\ast g-g{\mathrm{\parallel }}_2\to 0$ as $\eta \to 0^{+}$. (Every $L^1$ approximate identity converges to the identity in $L^p$ for $1\le p<\mathrm{\infty }$)

Interior mollification commutes with first weak derivatives: if $w\in H^1(U)$ and the $\eta$-neighborhood of $K$ lies inside $U$, then $D_i({\rho }_{\eta }\ast w)={\rho }_{\eta }\ast (D_{i}w)$ on $K$. (Interior mollification commutes with weak derivatives)

Convolution of a locally integrable function with a smooth compactly supported mollifier is smooth and derivatives pass under the integral sign. (Convolution with a mollifier is smooth, and derivatives pass under the integral sign)

An $L^2$ function on a bounded set is locally integrable by Holder's inequality and finiteness of Lebesgue measure on bounded sets. (Holder's inequality for integrals, including the endpoint cases, Lebesgue measure is sigma-finite, and every metrically bounded subset of ${\mathbb{R}}^n$ has finite outer measure)