← Mathematical handbook

Exact Spearman rho for arbitrary rectangular Bernstein copulas

theorem Verification.bernstein_cdf_integral (C : ProbabilityTheory.Copula 2) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : ∫ (x : Fin 2 → ↑unitInterval), (C.bernstein m n hm hn).cdf x ∂(ProbabilityTheory.Copula.independence 2).toMeasure = (∑ i : Fin (m + 1), ∑ j : Fin (n + 1), C.cdf ![bernstein.z i, bernstein.z j]) / ((↑m + 1) * (↑n + 1))

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

Frobenius sum form of Proposition 3.1; the zero-index terms vanish automatically.