Derivative of Moreau envelope in Hilbert space with respect to regularization parameter $\lambda$ using Hopf-Lax formula?

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.

Let $$\lambda>0$$ and $$y$$ be such that $$\lambda+y>0$$. Let $$p_0=prox[\lambda f](x)$$ and $$p_y=prox[(\lambda+y)f](x)$$. By definition, the objective function at $$y+\lambda$$ of the minimizer $$p_y$$ is smaller than the same objective at $$p_0$$, \begin{align} h(y) &= f_{\lambda+y}(x)-f_\lambda(x) + \frac{y}{2\lambda^2}\|x-p_0\|^2 \\&\le \frac{\|x-p_0\|^2}{2(\lambda+y)} + f(p_0) - f(p_0) - \frac{\|x-p_0\|^2}{2\lambda} + \frac{y}{2\lambda^2}\|x-p_0\|^2 \\&= \|x-p_0\|^2 \frac{y^2}{2\lambda^2(y+\lambda)}. \end{align} Because $$\lambda\mapsto f_\lambda(x)$$ is convex in $$\lambda$$, $$y\mapsto h(y)$$ is also convex and $$h(0)=0$$ gives $$h(y)\ge - h(-y)\ge - \|x-p_0\|^2 \frac{y^2}{2\lambda^2(-y+\lambda)}.$$ This gives $$h(y)=O(y^2)$$ hence the desired derivative.