← Copula mathematical handbook

Spearman's rho of the Ali--Mikhail--Haq family as a series

For |θ| ≤ 1 the AMH copula C(u, v) = u v / (1 - θ (1-u) (1-v)) has the expansion C(u, v) = ∑ₖ θᵏ · u(1-u)ᵏ · v(1-v)ᵏ, and ∫₀¹ t (1-t)ᵏ dt = 1 / ((k+1)(k+2)). Integrating term by term gives (Nelsen, An Introduction to Copulas, Example 5.7 in dilogarithm form) ρ = 12 ∑ₖ θᵏ / ((k+1)² (k+2)²) - 3, which is the series of the dilogarithm expression.

theorem ProbabilityTheory.Copula.SpearmanAMH.integral_unit_mul_one_sub_pow (k : ℕ) : ∫ (t : ↑unitInterval), ↑t * (1 - ↑t) ^ k = 1 / ((↑k + 1) * (↑k + 2))

noncomputable def ProbabilityTheory.Copula.SpearmanAMH.term (θ : ℝ) (k : ℕ) (x : Fin 2 → ↑unitInterval) : ℝ

The k-th term of the AMH expansion: θᵏ · u (1-u)ᵏ · v (1-v)ᵏ.

Equations

• ProbabilityTheory.Copula.SpearmanAMH.term θ k x = θ ^ k * (↑(x 0) * (1 - ↑(x 0)) ^ k * (↑(x 1) * (1 - ↑(x 1)) ^ k))

theorem ProbabilityTheory.Copula.SpearmanAMH.g_nonneg (k : ℕ) (t : ↑unitInterval) : 0 ≤ ↑t * (1 - ↑t) ^ k

theorem ProbabilityTheory.Copula.SpearmanAMH.hasSum_cdf_amh (θ : ℝ) (hmin : -1 ≤ θ) (hmax : θ ≤ 1) (a b : ↑unitInterval) : HasSum (fun (k : ℕ) => term θ k ![a, b]) ((amh θ hmin hmax).cdf ![a, b])

theorem ProbabilityTheory.Copula.SpearmanAMH.continuous_term (θ : ℝ) (k : ℕ) : Continuous (term θ k)

theorem ProbabilityTheory.Copula.SpearmanAMH.integral_term (θ : ℝ) (k : ℕ) : ∫ (x : Fin 2 → ↑unitInterval), term θ k x ∂(independence 2).toMeasure = θ ^ k * (1 / ((↑k + 1) * (↑k + 2))) ^ 2

theorem ProbabilityTheory.Copula.SpearmanAMH.norm_term (θ : ℝ) (k : ℕ) (x : Fin 2 → ↑unitInterval) : ‖term θ k x‖ = |θ| ^ k * (↑(x 0) * (1 - ↑(x 0)) ^ k * (↑(x 1) * (1 - ↑(x 1)) ^ k))

theorem ProbabilityTheory.Copula.SpearmanAMH.integral_norm_term (θ : ℝ) (k : ℕ) : ∫ (x : Fin 2 → ↑unitInterval), ‖term θ k x‖ ∂(independence 2).toMeasure = |θ| ^ k * (1 / ((↑k + 1) * (↑k + 2))) ^ 2

theorem ProbabilityTheory.Copula.SpearmanAMH.summable_integral_norm_term (θ : ℝ) (hθ : |θ| ≤ 1) : Summable fun (k : ℕ) => ∫ (x : Fin 2 → ↑unitInterval), ‖term θ k x‖ ∂(independence 2).toMeasure

theorem ProbabilityTheory.Copula.hasSum_spearmanRho_amh (θ : ℝ) (hmin : -1 ≤ θ) (hmax : θ ≤ 1) : HasSum (fun (k : ℕ) => 12 * (θ ^ k / ((↑k + 1) ^ 2 * (↑k + 2) ^ 2))) ((amh θ hmin hmax).spearmanRho + 3)

Spearman's rho of the AMH copula (|θ| ≤ 1) as a convergent series: ρ + 3 = ∑ₖ 12 θᵏ / ((k+1)² (k+2)²).

theorem ProbabilityTheory.Copula.spearmanRho_amh (θ : ℝ) (hmin : -1 ≤ θ) (hmax : θ ≤ 1) : (amh θ hmin hmax).spearmanRho = 12 * ∑' (k : ℕ), θ ^ k / ((↑k + 1) ^ 2 * (↑k + 2) ^ 2) - 3

Spearman's rho of the AMH copula (|θ| ≤ 1): ρ = 12 ∑ₖ θᵏ / ((k+1)² (k+2)²) - 3.