The weighted area form is SL2(R)-invariant

Write ${\varphi }_g(w)=g\cdot w=(aw+b)\mathrm{/}(cw+d)$ and $j(g,w)=cw+d$. Expanding ${\varphi }_g(w)$ against the conjugate denominator gives $\mathrm{Im}{\varphi }_g(w)=\mathrm{Im}w\mathrm{/}\mathrm{\mid }cw+d{\mathrm{\mid }}^2$, and multiplying matrices gives the cocycle law $j(gh,w)=j(g,h\cdot w)j(h,w)$, which for $gh=1$ yields $j(g^{-1},g\cdot w)=j(g,w{)}^{-1}$. By [F3], $\mathrm{\mid }{\det }_{\mathbb{R}}D{\varphi }_g(w)\mathrm{\mid }=\mathrm{\mid }j(g,w){\mathrm{\mid }}^{-4}$; by the imaginary-part identity, $(\mathrm{Im}{\varphi }_g(w){)}^{n-2}=(\mathrm{Im}w{)}^{n-2}\mathrm{\mid }j(g,w){\mathrm{\mid }}^{-2(n-2)}$. The inverse relation gives $\mathrm{\mid }j(g^{-1},{\varphi }_g(w))\mathrm{\mid }=\mathrm{\mid }j(g,w){\mathrm{\mid }}^{-1}$, so $\mathrm{\mid }{\pi }_n(g)f({\varphi }_g(w)){\mathrm{\mid }}^2=\mathrm{\mid }j(g,w){\mathrm{\mid }}^{2n}\mathrm{\mid }f(w){\mathrm{\mid }}^2$. Multiplying these three factors cancels the exponent $2n-2(n-2)-4=0$, proving the stated pullback identity for the weighted density.

Set $w=(z-i)\mathrm{/}(z+i)$ and $F_f(w)=(z+i{)}^{n}f(z)$. The inverse $z=i(1+w)\mathrm{/}(1-w)$ gives $y=(1-\mathrm{\mid }w{\mathrm{\mid }}^2)\mathrm{/}\mathrm{\mid }1-w{\mathrm{\mid }}^2$ and $\mathrm{\mid }dz\mathrm{/}dw{\mathrm{\mid }}^2=4\mathrm{/}\mathrm{\mid }1-w{\mathrm{\mid }}^4$, so [F3] and [F4] give $\mathrm{\parallel }f{\mathrm{\parallel }}_n^2=2^{2-2n}{\int }_{\mathbb{D}}\mathrm{\mid }{F}_f(w){\mathrm{\mid }}^2(1-\mathrm{\mid }w{\mathrm{\mid }}^2{)}^{n-2}dA(w)$. Here $F_{f_{n,j}}=w^j$. Write $g^{-1}=\left(\begin{array}{cc}A& B\\ C& D\end{array}\right)$ and put $P_g(w)=i(A-iC)(1+w)+(B-iD)(1-w)$ and $R_g(w)=i(A+iC)(1+w)+(B+iD)(1-w)$. Substitution in [F1] gives $F_{{\pi }_n(g)f_{n,j}}(w)=(2i{)}^n{P}_g(w{)}^j\mathrm{/}{R}_g(w{)}^{n+j}$. At $g=e$ one has $P_e(w)=2iw$ and $R_e(w)=2i$. Continuity of their coefficients makes $\mathrm{\mid }{R}_g(w)\mathrm{\mid }\ge 1$ on $\mathrm{\mid }w\mathrm{\mid }\le 1$ for $g$ sufficiently close to $e$, and the displayed rational functions converge uniformly there to $w^j$. Since $n\ge 2$, the disk weight has finite integral, at most $\pi$; hence this uniform convergence implies $\mathrm{\parallel }{\pi }_n(g)f_{n,j}-f_{n,j}{\mathrm{\parallel }}_n\to 0$. Linearity proves continuity at $e$ on their finite span.

The map ${\varphi }_g:\mathfrak{H}\to \mathfrak{H}$ is a C1 diffeomorphism with inverse ${\varphi }_{g^{-1}}$. Apply [F4] to the nonnegative measurable function $z\mapsto \mathrm{\mid }{\pi }_n(g)f(z){\mathrm{\mid }}^2(\mathrm{Im}z{)}^{n-2}$; the pullback identity of step 1.1 gives $\mathrm{\parallel }{\pi }_n(g)f{\mathrm{\parallel }}_n^2=\mathrm{\parallel }f{\mathrm{\parallel }}_n^2$, including the extended integral identity when either side is infinite. For $f\in {\mathcal{H}}_n^{+}$ this is finite, so ${\pi }_n(g)$ maps that space into itself and is an isometry. By [F1], ${\pi }_n(g^{-1})$ is its inverse and the maps obey the group law. Thus they are bijective linear isometries; conjugation gives the same claims for ${\pi }_n^{-}$.

This span is dense by [F5], and every ${\pi }_n(g)$ is an isometry by step 2.1. For arbitrary $f$ and a vector $p$ in the span, $\mathrm{\parallel }{\pi }_n(g)f-f{\mathrm{\parallel }}_n\le 2\mathrm{\parallel }f-p{\mathrm{\parallel }}_n+\mathrm{\parallel }{\pi }_n(g)p-p{\mathrm{\parallel }}_n$. First approximate $f$ and then use step 1.2 to obtain continuity at $e$. At $g_0$, the group law gives $\mathrm{\parallel }{\pi }_n(g)f-{\pi }_n(g_0)f{\mathrm{\parallel }}_n=\mathrm{\parallel }{\pi }_n(g_0^{-1}g)f-f{\mathrm{\parallel }}_n\to 0$. Thus [F6] gives strong continuity on $G$; complex conjugation gives the same conclusion for ${\pi }_n^{-}$.