← Mathematical handbook

Proposition 3.1: the exact Bernstein Spearman-rho formula

theorem Papers.Rockel2025Approximation.bernstein_rho_grid (C : ProbabilityTheory.Copula 2) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : (C.bernstein m n hm hn).spearmanRho = (12 * ∑ i : Fin m, ∑ j : Fin n, C.cdf ![bernstein.z i.succ, bernstein.z j.succ]) / ((↑m + 1) * (↑n + 1)) - 3

The boundary-zero rows/columns vanish, leaving the source indices 1,...,m and 1,...,n.

theorem Papers.Rockel2025Approximation.bernstein_rho_frobenius (C : ProbabilityTheory.Copula 2) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : (C.bernstein m n hm hn).spearmanRho = 12 * ∑ i : Fin m, ∑ j : Fin n, 1 / ((↑m + 1) * (↑n + 1)) * C.cdf ![bernstein.z i.succ, bernstein.z j.succ] - 3

The Frobenius form 12 tr(Gamma^T D)-3 with Gamma_ij=1/((m+1)(n+1)).