← Copula mathematical handbook

Spearman rho of Nelsen's seventh family

The rational CDF integral and its logarithmic evaluation cover the full closed parameter interval, with separate finite endpoint values.

theorem ProbabilityTheory.Copula.integral_unit_linear_hinge (h : ℝ) (hh : 0 ≤ h) (t : ↑unitInterval) : ∫ (u : ↑unitInterval), max 0 (h * (↑u - ↑t)) = h * (1 - ↑t) ^ 2 / 2

Integral of a nonnegative linear hinge on the unit interval.

theorem ProbabilityTheory.Copula.integral_unit_affine_reciprocal (a : ℝ) (ha : 0 < a) (ha1 : a < 1) : ∫ (v : ↑unitInterval), 1 / (a * ↑v + 1 - a) = -Real.log (1 - a) / a

Affine reciprocal integral on the unit interval.

theorem ProbabilityTheory.Copula.integral_unit_nelsen7_rational (a : ℝ) (ha : 0 < a) (ha1 : a < 1) : ∫ (v : ↑unitInterval), ↑v ^ 2 / (2 * (a * ↑v + 1 - a)) = (3 * a ^ 2 - 2 * a - 2 * (a - 1) ^ 2 * Real.log (1 - a)) / (4 * a ^ 3)

The logarithmic one-variable integral in Nelsen 7's Spearman rho.

theorem ProbabilityTheory.Copula.nelsen7_integral_cdf_first (θ v : ↑unitInterval) : ∫ (u : ↑unitInterval), (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 ProbabilityTheory.Copula.nelsen7_rho_integral (θ : ↑unitInterval) : (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 ProbabilityTheory.Copula.nelsen7_rho_interior (θ : ↑unitInterval) (h0 : 0 < ↑θ) (h1 : ↑θ < 1) : (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 ProbabilityTheory.Copula.nelsen7_rho (θ : ↑unitInterval) : (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.