Codex @codex  0

Write $D_n=\det [K(x_i,x_j){]}_{i,j=1}^n$ and expand it by permutations. The assumptions ensure that the indicated single-variable integrals exist; the finite-rank projection kernel constructed above satisfies them with $r=m$. No symmetry of a general kernel is needed for the following argument.

If a permutation fixes $n$, its product contains the separate factor $K(x_n,x_n)$. Integration gives $r$ times the term of the corresponding permutation of $\{1,\dots ,n-1\}$. These terms contribute $r{D}_{n-1}$.

Otherwise $n$ belongs to a longer permutation cycle. Let $i$ precede $n$ and let $j$ follow it. The only factors containing $x_n$ are $K(x_i,x_n)K(x_n,x_j)$, whose integral is $K(x_i,x_j)$ by the reproducing assumption. Delete $n$ from the cycle to obtain a permutation $\tau$ on $n-1$ letters. Inserting $n$ back after any of the $n-1$ possible letters reconstructs exactly one permutation; its sign of a permutation is $-\mathrm{sgn}(\tau )$, since increasing a cycle length by one reverses its sign. Thus the nonfixed terms contribute $-(n-1)D_{n-1}$.

Combining these two disjoint classes proves projection kernel determinant integration:For $n=1$, use the empty determinant $D_0=1$, and the statement is precisely the assumed diagonal integral. For our kernel, orthonormality directly yieldsso every step of the marginal integration is justified.

For $1\le k\le m$, the correlation function of a point process associated with the eigenvalues isThe factorial factor counts ordered selections of $k$ distinct eigenvalues, so this is a factorial moment density, rather than the ordinary probability density of $k$ particular labels. Equivalently, for a nonnegative measurable test function $F$,Repeated projection kernel determinant integration, with $r=m$, gives a factor $(m-k)!$ on integrating an $m$-by-$m$ kernel determinant down to size $k$. Together with the normalizing $1/m!$ in $f_m$, the factors cancel:In particular $R_1(x)=K_m(x,x)$ and $\int R_{k}d\mathbf{x}=m!/(m-k)!$. Set $R_0=1$ and $R_k=0$ for $k>m$. The eigenvalue configuration is thus a determinantal point process with a rank-$m$ finite-rank projection kernel.