← Copula mathematical handbook

theorem ProbabilityTheory.Copula.nelsen7_tau_rho (θ : ↑unitInterval) : (nelsen7 θ).kendallTau = -1 + ↑θ / 3 * ((nelsen7 θ).spearmanRho + 3)

Nelsen 7's tau is an affine transform of its rho at the same parameter.

theorem ProbabilityTheory.Copula.nelsen7_tau_interior (θ : ↑unitInterval) (h0 : 0 < ↑θ) (h1 : ↑θ < 1) : (nelsen7 θ).kendallTau = 2 - 2 / ↑θ - 2 * (↑θ - 1) ^ 2 * Real.log (1 - ↑θ) / ↑θ ^ 2

Table 6's exact Nelsen 7 Kendall-tau formula at interior parameters.

theorem ProbabilityTheory.Copula.nelsen7_tau (θ : ↑unitInterval) : (nelsen7 θ).kendallTau = if θ = 0 then -1 else if θ = 1 then 0 else 2 - 2 / ↑θ - 2 * (↑θ - 1) ^ 2 * Real.log (1 - ↑θ) / ↑θ ^ 2

Table 6's exact Nelsen 7 Kendall-tau formula on the full closed interval.