Let $\mathcal H$ be a Hilbert space, $f \colon \mathcal H \to (- \infty, \infty]$ a proper, convex, lower semi-continuous function and $\lambda > 0$. The $\lambda$-Moreau envelope of $f$ is $$ f_{\lambda} \colon \mathcal H \to \mathbb R, \qquad x \mapsto \min_{y \in H} f(y) + \frac{1}{2\lambda} \| x - y \|_H^2. $$ We have $\frac{\partial}{\partial x} f_{\lambda}(x) = \frac{1}{\lambda} \left( x - \text{prox}_{\lambda f}(x)\right)$, (where $\text{prox}$ is the proximal operator, which maps $x$ to the minimzer $y$ in the above formula) but I am interested in $\frac{\partial}{\partial \lambda} f_{\lambda}$.

For $\mathcal H = \mathbb R^n$ the Hopf-Lax formula (see e.g. Evans: PDE, thm. 4 in section 3.3.2b) with convex, smooth Hamiltonian $H \colon \mathcal H \to \mathbb R$, $x \mapsto \frac{1}{2} \| x \|_2^2$ (which has superlinear growth at infinity) states that if $f$ is Lipschitz continuous, then $(t, x) \mapsto f_t(x)$ is the unique viscosity solution of the Hamilton-Jacobi-Bellmann equation $$ \begin{cases} \partial_t u_t(x, t) + \frac{1}{2} \| \nabla_x u(t, x) \|_2^2 = 0, \qquad x \in \mathbb R^n, t > 0, \\ u(0, x) = f(x), \qquad x \in \mathbb R^n \end{cases}, $$ which shows that $\frac{\partial}{\partial \lambda} f_{\lambda}(x) = - \frac{1}{2 \lambda^2} \| x - \text{prox}_{\lambda f}(x) \|_2^2$ for $\lambda > 0$ and $x \in \mathbb R^n$.

Is there a corresponding result in Hilbert spaces and can the Lipschitz continuity assumption on $f$ be relaxed?

**Edit.**
Can we perhaps use an envelope theorem, by defining
$$
g \colon \text{dom}(f) \times \mathcal H \times \mathbb R, \qquad
(x, y, \lambda) \mapsto - f(x) - \frac{1}{2 \lambda} \| x - y \|_{\mathcal H}^2
$$
and the *value function*
$$
V \colon \mathcal H \times \mathbb R \to \mathbb R, \qquad
(y, \lambda) \mapsto \sup_{x \in \text{dom}(f)} g(x, y, \lambda)
= - f_{\lambda}(y).
$$
Since $\partial_y g$ and $\partial_{\lambda} g$ exist, the multidimensional version of the envelope theorem should somehow state that if $V$ is totally differentiable, then $\nabla V(y, \lambda) = (\partial_y g, \partial_{\lambda} g)$, yielding the desired result.