← Mathematical handbook

theorem Papers.AnsariRockel2024.nelsen7_integral_cdf_first (θ v : ↑unitInterval) : ∫ (u : ↑unitInterval), (ProbabilityTheory.Copula.nelsen7 θ).cdf ![u, v] = ↑v ^ 2 / (2 * (↑θ * ↑v + 1 - ↑θ))

The inner CDF integral in the paper's Spearman-rho calculation, valid also at the countermonotonic and independence endpoints.

theorem Papers.AnsariRockel2024.nelsen7_rho_integral (θ : ↑unitInterval) : (ProbabilityTheory.Copula.nelsen7 θ).spearmanRho = (12 * ∫ (v : ↑unitInterval), ↑v ^ 2 / (2 * (↑θ * ↑v + 1 - ↑θ))) - 3

Appendix A.5.1's one-variable rho integral, including both endpoints; its logarithmic evaluation remains a separate calculus step.

theorem Papers.AnsariRockel2024.nelsen7_rho_interior (θ : ↑unitInterval) (h0 : 0 < ↑θ) (h1 : ↑θ < 1) : (ProbabilityTheory.Copula.nelsen7 θ).spearmanRho = 12 * ((3 * ↑θ ^ 2 - 2 * ↑θ - 2 * (↑θ - 1) ^ 2 * Real.log (1 - ↑θ)) / (4 * ↑θ ^ 3)) - 3

Appendix A.5.1's closed Spearman-rho expression at interior parameters.

theorem Papers.AnsariRockel2024.nelsen7_rho (θ : ↑unitInterval) : (ProbabilityTheory.Copula.nelsen7 θ).spearmanRho = if θ = 0 then -1 else if θ = 1 then 0 else 12 * ((3 * ↑θ ^ 2 - 2 * ↑θ - 2 * (↑θ - 1) ^ 2 * Real.log (1 - ↑θ)) / (4 * ↑θ ^ 3)) - 3

Table 6's exact Nelsen 7 Spearman-rho formula on the full parameter interval, with the two singular logarithmic endpoints stated separately.