The weighted discrete-series space is a Hilbert space with K-type basis

Fix $z_0\in \mathfrak{H}$ and choose $r>0$ with $\overline{D(z_0,r)}\subset \mathfrak{H}$. The Cauchy formula and Cauchy–Schwarz on each circle centered at $z_0$ give $\mathrm{\mid }f(z_0){\mathrm{\mid }}^2\le (2\pi {)}^{-1}{\int }_0^{2\pi }\mathrm{\mid }f(z_0+s{e}^{it}){\mathrm{\mid }}^{2}dt$ for $0<s<r$; integrating with $2s\mathrm{/}{r}^2$ yields $\mathrm{\mid }f(z_0){\mathrm{\mid }}^2\le (\pi r^2{)}^{-1}{\int }_{D(z_0,r)}\mathrm{\mid }f{\mathrm{\mid }}^{2}dA$. Since $y^{n-2}$ has a positive lower bound on this disk, $\mathrm{\mid }f(z_0)\mathrm{\mid }\le C_{z_0,r}\mathrm{\parallel }f{\mathrm{\parallel }}_n$. If $z\in D(z_i,r_i\mathrm{/}2)$, then $D(z,r_i\mathrm{/}2)\subset D(z_i,r_i)$; applying the same estimate there and using a lower bound for the weight on $D(z_i,r_i)$ gives a uniform evaluation bound on $D(z_i,r_i\mathrm{/}2)$. A finite subcover of any compact $C\subset \mathfrak{H}$ therefore gives one constant $C_C$ for all $z\in C$.

Set $w=(z-i)\mathrm{/}(z+i)$ for $z\in \mathfrak{H}$. Then $\mathrm{\mid }w{\mathrm{\mid }}^2-1=-4y\mathrm{/}\mathrm{\mid }z+i{\mathrm{\mid }}^2<0$, so $w\in \mathbb{D}$, and solving $w=(z-i)\mathrm{/}(z+i)$ gives the inverse $z=i(1+w)\mathrm{/}(1-w)$ with $\mathrm{Im}z=(1-\mathrm{\mid }w{\mathrm{\mid }}^2)\mathrm{/}\mathrm{\mid }1-w{\mathrm{\mid }}^2>0$ for $w\in \mathbb{D}$; hence $z\mapsto w$ is a bijection $\mathfrak{H}\to \mathbb{D}$. Since $z+i=2i\mathrm{/}(1-w)$ and $dz\mathrm{/}dw=2i\mathrm{/}(1-w{)}^2$, the real Jacobian of $w\mapsto z$ is $\mathrm{\mid }dz\mathrm{/}dw{\mathrm{\mid }}^2=4\mathrm{/}\mathrm{\mid }1-w{\mathrm{\mid }}^4$, and [F2] gives $\mathrm{\parallel }f{\mathrm{\parallel }}_n^2=2^{2-2n}{\int }_{\mathbb{D}}\mathrm{\mid }F(w){\mathrm{\mid }}^2(1-\mathrm{\mid }w{\mathrm{\mid }}^2{)}^{n-2}dA(w)$ for $F(w):=(z+i{)}^{n}f(z)$. For $f_{n,j}$ one has $F(w)=(z-i{)}^j(z+i{)}^{-j}=w^j$, and consequently $\mathrm{\parallel }{f}_{n,j}{\mathrm{\parallel }}_n^2=2^{2-2n}2\pi {\int }_0^1{\rho }^{2j+1}(1-{\rho }^2{)}^{n-2}d\rho$, which is finite since $(1-{\rho }^2{)}^{n-2}\le 1$ and ${\int }_0^1{\rho }^{2j+1}d\rho =(2j+2{)}^{-1}$, and is positive since the integrand is positive on $(0,1)$. Distinct monomials are orthogonal because ${\int }_0^{2\pi }{e}^{i(j-k)\theta }d\theta =0$ for $j\mathrm{\ne }k$.

On ${\mathbb{R}}^2$ give the measure ${\mu }_n$ the density ${\mathbf{1}}_{\mathfrak{H}}(x,y)y^{n-2}$ relative to Lebesgue measure, and extend functions on $\mathfrak{H}$ by zero below the real axis. The map ${\mathcal{H}}_n^{+}\to$ the weighted square-integrable function space for ${\mu }_n$ is injective: a zero class has norm zero, and the estimate of step 1.1 then makes every point value zero. The integral pairing thus restricts to a positive-definite inner product. If $(f_m)$ is Cauchy in this norm, [F5] gives a limit class $h$; step 1.1 makes $(f_m)$ uniformly Cauchy on every compact subset of $\mathfrak{H}$, so it converges locally uniformly to a holomorphic $f$ by [F4]. On each compact $Q⋐\mathfrak{H}$, the density is bounded and $Q$ has finite area, so local uniform convergence gives convergence in the restricted weighted integral norm on $Q$. Restriction of $f_m\to h$ to $Q$ and uniqueness of limits imply $f=h$ a.e. on $Q$. The compact exhaustion $Q_m=\{z:\mathrm{\mid }z\mathrm{\mid }\le m,\mathrm{Im}z\ge 1\mathrm{/}m\}$ covers $\mathfrak{H}$, so $f=h$ a.e. globally; hence $f\in {\mathcal{H}}_n^{+}$ and $\mathrm{\parallel }{f}_m-f{\mathrm{\parallel }}_n\to 0$. Thus ${\mathcal{H}}_n^{+}$ is a complex Hilbert space.

Expand $F(w)={\sum }_{j\ge 0}{a}_j{w}^j$ by [F3]. For each $0<\rho <1$ this series converges uniformly on $\mathrm{\mid }w\mathrm{\mid }=\rho$; integrating finite partial sums and using orthogonality of exponentials, then taking the uniform limit, gives $(2\pi {)}^{-1}{\int }_0^{2\pi }\mathrm{\mid }F(\rho e^{i\theta }){\mathrm{\mid }}^{2}d\theta ={\sum }_{j\ge 0}\mathrm{\mid }{a}_j{\mathrm{\mid }}^2{\rho }^{2j}$. Integrating radially and applying [F6] to the increasing finite partial sums yields ${\int }_{\mathbb{D}}\mathrm{\mid }F(w){\mathrm{\mid }}^2(1-\mathrm{\mid }w{\mathrm{\mid }}^2{)}^{n-2}dA(w)={\sum }_{j\ge 0}\mathrm{\mid }{a}_j{\mathrm{\mid }}^{2}2\pi {\int }_0^1{\rho }^{2j+1}(1-{\rho }^2{)}^{n-2}d\rho$. This sum is finite by step 1.2; applying the same identity to $F-{\sum }_{j=0}^N{a}_j{w}^j$ shows that the squared norm of the remainder is its series tail, which tends to zero. Thus the $f_{n,j}$ have dense algebraic span in ${\mathcal{H}}_n^{+}$, and step 1.2 makes them a complete orthogonal family.

In the disk coordinate the K-action is $F_{{\pi }_n(k_{\theta })f}(w)=e^{-in\theta }{F}_f(e^{-2i\theta }w)$. The orbit map of each polynomial in $w$ is therefore norm-continuous. The maps ${\pi }_n(k)$ are isometries by [F1], and polynomials are dense by step 2.2; approximating $f$ by a polynomial $p$ and using $\mathrm{\parallel }{\pi }_n(k)f-{\pi }_n(k_0)f{\mathrm{\parallel }}_n\le 2\mathrm{\parallel }f-p{\mathrm{\parallel }}_n+\mathrm{\parallel }{\pi }_n(k)p-{\pi }_n(k_0)p{\mathrm{\parallel }}_n$ proves strong continuity on all of ${\mathcal{H}}_n^{+}$. Since each ${\pi }_n(k)$ has inverse ${\pi }_n(k^{-1})$, this is a strongly continuous unitary representation of compact $K$.

The compact-group decomposition [F7] applies by steps 2.1 and 3.1. Its irreducible K-types are finite-dimensional; because $K=\mathrm{S}\mathrm{O}(2)$ is abelian, the commuting unitary operators on any such finite-dimensional space have a common eigenline, and irreducibility forces that line to be the whole space. Thus every K-type is a character line. The complete orthogonal family from step 2.2 consists of eigenvectors with distinct characters ${\chi }_j(k_{\theta })=e^{-i(n+2j)\theta }$ by [F1]. An eigenvector for a different character is orthogonal to every $f_{n,j}$ by unitarity and therefore vanishes by density. Each listed isotypic subspace is exactly $\mathbb{C}{f}_{n,j}$, since it is orthogonal to all other character lines and the family is complete.

For each $j$, [F7] gives the type projection $P_{j}f={\int }_K\overline{{\chi }_j(k)}{\pi }_n(k)fdk$, where $\overline{{\chi }_j}={\chi }_j^{-1}$. The point-evaluation map $E_z:f\mapsto f(z)$ is bounded by step 1.1, so [F8] lets it pass through the Bochner integral. In disk coordinates, the scalar integrand is ${\sum }_{\mathrm{\ell }\ge 0}{a}_{\mathrm{\ell }}{w}^{\mathrm{\ell }}\overline{{\chi }_j(k)}{\chi }_{\mathrm{\ell }}(k)$ by step 3.1; for fixed $\mathrm{\mid }w\mathrm{\mid }<1$ this series converges uniformly in $k$. Haar invariance makes the integral of every nontrivial character zero (translate by an element where its value is not $1$), while the trivial character has integral $1$. Thus $E_z(P_{j}f)$ corresponds to $a_j{w}^j$, so $P_{j}f=a_j{f}_{n,j}$. The Hilbert expansion of step 2.2 is therefore $f={\sum }_{j\ge 0}{P}_{j}f$. Complex conjugation gives the same Hilbert and K-type conclusions for ${\mathcal{H}}_n^{-}$.