Real analytic approximation of Lipschitz functions on Hilbert space and other Banach spaces

Let X be a separable Banach space with a separating polynomial. We show that there exists C⩾1 (depending only on X) such that for every Lipschitz function f:X→R, and every ε>0, there exists a Lipschitz, real analytic function g:X→R such that |f(x)−g(x)|⩽ε and Lip(g)⩽CLip(f). This result is new even in the case when X is a Hilbert space. Furthermore, in the Hilbertian case we also show that C can be assumed to be any number greater than 1.