← Copula mathematical handbook

Spearman's rho of the Gumbel--Barnett family (Nelsen 4.2.9)

For C(u, v) = u v exp (-θ log u log v) the inner integral is elementary: ∫₀¹ u v u^(-θ log v) du = v / (2 - θ log v), so ρ = 12 ∫₀¹ v / (2 - θ log v) dv - 3. The remaining integral is an exponential integral (∫₀^∞ e^(-2s) / (2 + θ s) ds), which has no elementary closed form.

theorem ProbabilityTheory.Copula.SpearmanNelsen9.integral_cdf_nelsen9 (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) (v : ↑unitInterval) : ∫ (u : ↑unitInterval), (nelsen9 θ hθ h1).cdf ![u, v] = ↑v / (2 - θ * Real.log ↑v)

The inner integral of the Gumbel--Barnett CDF.

theorem ProbabilityTheory.Copula.spearmanRho_nelsen9 (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) : (nelsen9 θ hθ h1).spearmanRho = (12 * ∫ (v : ℝ) in 0..1, v / (2 - θ * Real.log v)) - 3

Spearman's rho of the Gumbel--Barnett copula (Nelsen 4.2.9, 0 < θ ≤ 1): ρ = 12 ∫₀¹ v / (2 - θ log v) dv - 3.