Proper action of $\mathrm{SL}(2,\mathbb{R})$ by isometries on a Hilbert space A topological group $G$ has the Haagerup property (or is a-T-menable) if it admits a continuous metrically proper action by affine isometries on a Hilbert space $\mathcal{H}$. That is, an action $\alpha\colon G\curvearrowright \mathcal{H}$ such that for any $x\in\mathcal{H}$, $\|\alpha(g)x\|_{\mathcal{H}}\to\infty$ as $g\to\infty$ (meaning $g$ leaves every compact set).
It is well-known that $\mathrm{SL}(2,\mathbb{R})$ has the Haagerup property. A possible proof is to first verify that $F_2$, the free group on two generators, has the Haagerup property. Then to check that $F_2$ is a lattice in $\mathrm{SL}(2,\mathbb{R})$ (i.e. a discrete subgroup such that $\mathrm{SL}(2,\mathbb{R})/F_2$ has a finite invariant measure) and then to use the result that a lattice in a second-countable locally compact group has the Haagerup property if and only if the whole group does.
However, it is rather difficult to find somewhere an explicitly written metrically proper action of $\mathrm{SL}(2,\mathbb{R})$ on some Hilbert space. Can someone provide this?
 A: The first proof of the Haagerup Property for $\mathrm{SO}(n,1)$ (and hence $\mathrm{SL}_2(\mathbf{R})$), including explicit invariant conditionally negative definite kernels on real hyperbolic planes, is due to R. Gangolli, Positive definite kernels on homogeneous spaces and certain stochastic processes related to Lévy's Brownian motion of several parameters.
Ann. Inst. H. Poincaré Sect. B (N.S.) 3 1967 121-226. Here's the Numdam link (no paywall for old articles in French journals!). See notably p185 (and have in mind Schoenberg's theorem to go from positive-definite to conditionally negative definite).
All this was more explicitly said, and generalized to encompass $\mathrm{SU}(n,1)$, in Faraut, Harzallah (1974). Distances hilbertiennes invariantes sur un espace homogène. (French) Ann. Inst. Fourier (Grenoble) 24 (1974), no. 3, xiv, 171-217. 
Another proof (in the spirit of "measured walls"), inspired by work of Robertson and Steger, and working for all $\mathrm{SO}(n,1)$ (but not $\mathrm{SU}(n,1)$), can be found in the book of Bekka-Harpe-Valette, §2.6.
