← Copula mathematical handbook

Spearman's rho of the AMH copula at the endpoints of the parameter range

By spearmanRho_amh, ρ_θ = 12 ∑ₖ θᵏ / ((k+1)² (k+2)²) − 3 for |θ| ≤ 1. Using the partial fraction decomposition 1 / ((k+1)² (k+2)²) = 1/(k+1)² + 1/(k+2)² − 2 / ((k+1)(k+2)) we evaluate the series at the two endpoints (Nelsen, Example 5.7):

• θ = 1: ρ = 4 π² − 39 ≈ 0.4784, using ∑ 1/n² = π²/6 (hasSum_zeta_two);
• θ = −1: ρ = 33 − 48 log 2 ≈ −0.2711, the minimum of ρ over the AMH family, using the integral ∑ (−1)ᵏ / ((k+1)(k+2)) = ∫₀¹ (1−t)/(1+t) dt = 2 log 2 − 1 and the reflection ∑ (−1)ᵏ/(k+1)² + ∑ (−1)ᵏ/(k+2)² = 1.

theorem ProbabilityTheory.Copula.SpearmanAMHEndpoints.partial_fraction (k : ℕ) : 1 / ((↑k + 1) ^ 2 * (↑k + 2) ^ 2) = 1 / (↑k + 1) ^ 2 + 1 / (↑k + 2) ^ 2 - 2 * (1 / ((↑k + 1) * (↑k + 2)))

theorem ProbabilityTheory.Copula.SpearmanAMHEndpoints.summable_sq : Summable fun (k : ℕ) => 1 / (↑k + 1) ^ 2

theorem ProbabilityTheory.Copula.SpearmanAMHEndpoints.hasSum_telescope : HasSum (fun (k : ℕ) => 1 / ((↑k + 1) * (↑k + 2))) 1

theorem ProbabilityTheory.Copula.SpearmanAMHEndpoints.integral_pow_one_sub (k : ℕ) : ∫ (t : ℝ) in Set.Ioc 0 1, t ^ k * (1 - t) = 1 / ((↑k + 1) * (↑k + 2))

theorem ProbabilityTheory.Copula.SpearmanAMHEndpoints.integral_frac : ∫ (t : ℝ) in Set.Ioc 0 1, (1 - t) / (1 + t) = 2 * Real.log 2 - 1

theorem ProbabilityTheory.Copula.SpearmanAMHEndpoints.hasSum_alt : HasSum (fun (k : ℕ) => (-1) ^ k * (1 / ((↑k + 1) * (↑k + 2)))) (2 * Real.log 2 - 1)

theorem ProbabilityTheory.Copula.hasSum_amh_one : HasSum (fun (k : ℕ) => 1 / ((↑k + 1) ^ 2 * (↑k + 2) ^ 2)) (Real.pi ^ 2 / 3 - 3)

The AMH series at θ = 1: ∑ 1/((k+1)²(k+2)²) = π²/3 − 3.

theorem ProbabilityTheory.Copula.spearmanRho_amh_one : (amh 1 ⋯ ⋯).spearmanRho = 4 * Real.pi ^ 2 - 39

Spearman's rho of the AMH copula at θ = 1: ρ = 4 π² − 39.

theorem ProbabilityTheory.Copula.hasSum_amh_neg_one : HasSum (fun (k : ℕ) => (-1) ^ k / ((↑k + 1) ^ 2 * (↑k + 2) ^ 2)) (3 - 4 * Real.log 2)

The AMH series at θ = -1: ∑ (-1)ᵏ/((k+1)²(k+2)²) = 3 − 4 log 2.

theorem ProbabilityTheory.Copula.spearmanRho_amh_neg_one : (amh (-1) ⋯ ⋯).spearmanRho = 33 - 48 * Real.log 2

Spearman's rho of the AMH copula at θ = −1: ρ = 33 − 48 log 2 ≈ −0.2711.