Lemma 2.9.1980451E036222

Proof. If $n=1$, then $\mathbb P^0(\mathbb C)$ is a single point, and both sides equal $1$; so let $n\geq 2$. Let $\gamma $ be the probability measure on $\mathbb C^ n=\mathbb R^{2n}$ with density $\mathrm e^{-\pi |z|^2}$. Unitary maps are orthogonal on $\mathbb R^{2n}$, so they preserve Lebesgue measure and $|z|$; hence $\gamma $ is unitarily invariant. Moreover $\gamma (\{ 0\} )=0$. The map $z\mapsto \mathbb Cz$ from $\mathbb C^ n\setminus \{ 0\} $ to $\mathbb P^{n-1}(\mathbb C)$, that is, $z\mapsto zz^*/|z|^2$, is continuous and commutes with the action of $\mathrm U(n)$. Hence the image of $\gamma $ under this map is a unitarily invariant Borel probability measure, and by the uniqueness in proposition 2.9.18 it is $\sigma $.

The metric $d$ is unitarily invariant, because unitary matrices preserve $\langle \cdot ,\cdot \rangle $. Since $\sigma $ is invariant and the unitary group acts transitively, we may therefore take $\xi _0=\mathbb Ce_1$, the first coordinate line. Write $z=(z_1,z')$ with $z'\in \mathbb C^{n-1}$. For the line $\xi =\mathbb Cz$, the condition $d(\xi ,\xi _0)<a$ means $|z_1|>\cos a\, |z|$, because $\arccos $ is strictly decreasing; that is, $|z_1|^2\sin ^2a>\cos ^2a\, |z'|^2$, or $|z_1|^2>\cot ^2a\, |z'|^2$, where $\cot (\pi /2)=0$. Thus the preimage of the ball under $z\mapsto \mathbb Cz$ is the set of $z\neq 0$ with $|z_1|^2>\cot ^2a\, |z'|^2$. We compute its $\gamma $-measure by Fubini's theorem, integrating first in $z_1$. For $c\geq 0$, polar coordinates in $\mathbb C$ give

and we apply this with $c=\cot ^2a\, |z'|^2$. Using lemma 2.9.2 in $\mathbb C^{n-1}=\mathbb R^{2n-2}$ with $\xi =0$ and $t=1+\cot ^2a$, we obtain

The last assertion follows from $\sin a\leq a$. $\square$