A point process is determinantal with kernel relative to a specified reference measure if every correlation function of a point process is the indicated determinant. A rank- finite-rank projection kernel gives an exactly -point process, whose symmetric joint density is .
For real monic orthogonal polynomials with squared weighted norms under a positive weight , the functions form an orthonormal set for the unweighted reference measure. Their finite-rank projection kernel turns the squared weighted Vandermonde determinant into a kernel determinant. Normalization on the full labelled configuration space is .
Write 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 . No symmetry of a general kernel is needed for the following argument.
If a permutation fixes , its product contains the separate factor . Integration gives times the term of the corresponding permutation of . These terms contribute .
Otherwise belongs to a longer permutation cycle. Let precede and let follow it. The only factors containing are , whose integral is by the reproducing assumption. Delete from the cycle to obtain a permutation on letters. Inserting back after any of the possible letters reconstructs exactly one permutation; its sign of a permutation is , since increasing a cycle length by one reverses its sign. Thus the nonfixed terms contribute .
Combining these two disjoint classes proves projection kernel determinant integration:
For , use the empty determinant , and the statement is precisely the assumed diagonal integral. For our kernel, orthonormality directly yields
so every step of the marginal integration is justified.
For , the correlation function of a point process associated with the eigenvalues is
The factorial factor counts ordered selections of distinct eigenvalues, so this is a factorial moment density, rather than the ordinary probability density of particular labels. Equivalently, for a nonnegative measurable test function ,
Repeated projection kernel determinant integration, with , gives a factor on integrating an -by- kernel determinant down to size . Together with the normalizing in , the factors cancel:
In particular and . Set and for . The eigenvalue configuration is thus a determinantal point process with a rank- finite-rank projection kernel.