← Copula mathematical handbook

Spearman's rho of the AMH copula in dilogarithm form

Nelsen, An Introduction to Copulas, second edition, Example 5.7 (Table 4.1, family 4.2.3): for 0 < |θ| < 1 ρ_θ = 12 (1 + θ)/θ² · Li₂(θ) − 3 (θ + 12)/θ − 24 (1 − θ)/θ² · log (1 − θ), where Li₂(x) = ∑ₙ xⁿ / n² is the dilogarithm (dilogSeries); in Nelsen's notation Li₂(θ) = dilog(1 − θ) for dilog(x) = ∫₁ˣ log t/(1 − t) dt.

The proof uses the partial fraction decomposition 1 / ((k+1)² (k+2)²) = 1/(k+1)² + 1/(k+2)² − 2/(k+1) + 2/(k+2) in the series of spearmanRho_amh and the power series of Li₂ and of −log (1 − x).

noncomputable def ProbabilityTheory.Copula.dilogSeries (x : ℝ) : ℝ

The dilogarithm as a power series, Li₂(x) = ∑ₙ x^{n+1} / (n+1)² (|x| ≤ 1).

Equations

• ProbabilityTheory.Copula.dilogSeries x = ∑' (n : ℕ), x ^ (n + 1) / (↑n + 1) ^ 2

theorem ProbabilityTheory.Copula.summable_dilogSeries {x : ℝ} (hx : |x| ≤ 1) : Summable fun (n : ℕ) => x ^ (n + 1) / (↑n + 1) ^ 2

theorem ProbabilityTheory.Copula.spearmanRho_amh_dilog (θ : ℝ) (hmin : -1 ≤ θ) (hmax : θ ≤ 1) (h0 : θ ≠ 0) (habs : |θ| < 1) : (amh θ hmin hmax).spearmanRho = 12 * (1 + θ) / θ ^ 2 * dilogSeries θ - 3 * (θ + 12) / θ - 24 * (1 - θ) / θ ^ 2 * Real.log (1 - θ)

Spearman's rho of the AMH copula in dilogarithm form (Nelsen, Example 5.7): for 0 < |θ| < 1, ρ = 12 (1 + θ)/θ² · Li₂(θ) − 3 (θ + 12)/θ − 24 (1 − θ)/θ² · log (1 − θ).