Density of smooth function in Hilbert spaces I am looking for a simple reference to the following fact:

If $f:\Omega\to\mathbb{R}$ is continuous, where $\Omega\subset H$ is an open subset of a separable Hilbert space $H$, then for any $\varepsilon$ we can find a $C^\infty$ smooth function $f_\varepsilon:\Omega\to\mathbb{R}$ such that $|f(x)-f_\varepsilon(x)|<\varepsilon$ for $x\in\Omega$.

This result is stated on page 758 in [2] and it follows from results of [1] and the existence of a smooth partition of unity in $H$.
Is there any more direct and more recent reference? It is quite hard to read the original paper of  Bonic and Frampton since they discuss much more general results and I believe there should be a much more straightforward reference to this fact.
[1] R. Bonic, J. Frampton, Smooth functions on Banach manifolds. J. Math. Mech. 15 (1966), 877–898.
[2] J. Eells,  A setting for global analysis. Bull. Amer. Math. Soc.  72 (1966), 751–807.
 A: I think the paper of Bonic and Frampton is a good reference, but it is true that for a specific result like the one you are after, there is some amount of lingo that one can bypass. Here is my take on their proof, very heavily inspired by their Theorem 1. I must add that there might very well be a more readable proof of the fact in a classical book, I did not go through an extensive search.
Let $H$ be a separable Hilbert space,¹ and fix $\phi:\mathbb R\to\mathbb R_+$ a smooth function with $\{\phi>0\}=(0,\infty)$, for instance $t\mapsto\mathbf 1_{t>0}\exp(-1/t)$.

Lemma 1 (bump function).
There exists a smooth function $f:H\to\mathbb R$ with bounded support.

In particular, we immediately get (using translations and dilations, and considering squares) that the collection of open sets $\{f>0\}$, for $f:H\to\mathbb R_+$ smooth, is a basis.
Proof.
The function $Q:x\mapsto|x|_H^2/2$ is smooth (its derivatives are $D_xQ=\langle x,\cdot\rangle_H$, $D_x^2Q = \langle\cdot,\cdot\rangle_H$, $D_x^kQ=0$ for $k\geq3$), so $x\mapsto\phi(1-Q(x))$ is such a function by smoothness of composite functions.

Lemma 2 (Partition of unity).
Let $\mathscr U$ be a collection of open sets in $H$ with union $\Omega$. There exists sequences of open sets $U_n\in\mathscr U$ and smooth functions $f_n:H\to\mathbb R_+$ such that

*

*$\operatorname{supp}(f_n)\subset U_n$;

*every point $x\in\Omega$ admits a neighbourhood $V_x$ such that $\{f_n>0\}$ intersects $V_x$ only for finitely many $n$.

*the function $\sum_{n\geq0}(f_n)_{|\Omega}$ (well-defined and smooth according to the previous point) is constant equal to 1.


Proof.
It suffices to find sequences that satisfy 1. and 2., together with the fact that for every $x\in\Omega$, $f_n(x)>0$ for at least one $n$. Indeed, if $\mathscr V$ is the collection of every open ball whose closure belongs to some $U\in\mathscr V$, and $\tilde f_n$ is given by the modified lemma, then the collection of $f_n:=\tilde f_n/\sum_{m\geq0}\tilde f_m$ satisfies 1., 2. and 3. (the sum might not be well-defined and smooth out of $\Omega$, but it is fine in a neighbourhood of $\operatorname{supp}(\tilde f_n)$ by definition of $\mathscr V$).
We know from the bump function lemma that open sets of the form $\{g>0\}$ for $g:H\to\mathbb R_+$ and $\operatorname{supp}(g)\subset U\in\mathscr U$ cover $\Omega$. Passing to a countable subcover,² we find a countable collection of smooth non-negative functions $g_n$ such that for every $x\in\Omega$, we have $g_n(x)>0$ for at least one $n$.
Define
$$f_n:x\mapsto g_n(x)\prod_{m<n}\phi\big(2^{-n}-g_m(x)\big).$$
Let us show that for an appropriate choice of $U_n$, it satisfies 1., 2. and the modified 3. It is clearly non-negative and smooth. We have
$$\{f_n>0\} = \{g_n>0\}\cap\bigcap_{m<n}\{g_m<2^{-n}\},$$
so $\operatorname{supp}(f_n)\subset\operatorname{supp}(g_n)\subset U_n$ for a well-chosen $U_n\in\mathscr U$; this is point 1. For fixed $x\in\Omega$, if $n(x)$ is the first $n$ such that $g_n(x)>0$ (which exists by the above), then clearly $x\in\{f_{n(x)}>0\}$; this is point 3. Now setting
$$V_x = \{g_{n(x)}>g_{n(x)}(x)/2\},$$
clearly $V_x$ is an open neighbourhood of $x$. Moreover, for all $n>n(x)$ large enough, $2^{-n}<g_{n(x)}(x)/2$ and $\{f_n>0\}\subset\{g_{n(x)}<2^{-n}\}$ cannot intersect $V_x$. This is point 2.
Using the lemma, the result you state is classical.

Proposition.
For $\Omega\subset H$ open, $u:\Omega\to\mathbb R$ continuous and $\varepsilon>0$, there exists $u_\varepsilon:\Omega\to\mathbb R$ smooth such that $|u-u_\varepsilon|_\infty<\varepsilon$.

Proof.
Let $\mathscr U$ be the collection of open balls in $\Omega$ such that $|u-u(\text{centre})|_\infty<\varepsilon/2$ over said ball. Since $u$ is continuous, it is an open cover of $\Omega$. By the lemma, there exists sequences $(f_n)$, $(x_n)$, $(r_n)$ satisfying points 1., 2. and 3. with $U_n=B_{x_n}(r_n)$ the open ball with centre $x_n$ and radius $r_n$. The sum
$$u_\varepsilon:=\sum_{n\geq0}u(x_n)f_n$$
satisfies $|u-u_\varepsilon|_\infty<\infty$, since
$$|(u-u_\varepsilon)(x)| = \left|\sum_{n\geq0}\big(u(x)-u(x_n)\big)f_n(x)\right|\leq\sum_{n\geq0}\varepsilon f_n(x)=\varepsilon.$$

¹ It is possible that the result is true for $H$ larger (not separable), using things like: from every cover $\mathscr U$ of $H$, we can extract a (possibly uncountable) subcover $\mathscr V$ with a map $\mathscr V\mapsto\mathbb N$ such that all $U,V\in\mathscr V$ with the same label are disjoint. This is true in every paracompact space, but I am not entirely sure we can modify Lemma 2 to get this general case.
² $H$ is separable, hence it admits a countable basis, and the same holds for $\Omega$. For every pair $U\subset V$ of elements in the countable basis, take one $W$ in the support-of-smooth-functions basis such that $U\subset W\subset V$, if it exists; the result is a countable subcover. This relies on choice as is, but if the countable dense subset is given one can find a (big) explicit such countable cover.
