← Mathematical handbook

Table 6: Student-t and Laplace Spearman rho in Heinen–Valdesogo form

Heinen and Valdesogo (2020, Proposition 1) write Spearman's rho of a normal variance mixture as (6/π) E[arcsin(r V)] with V = W₃/√((W₁+W₃)(W₂+W₃)) for three independent copies Wᵢ of the mixing variance. For Student-t the variance is the reciprocal of a Gamma(ν/2,ν/2) precision (inverse gamma); for Laplace it is Gamma(1,1). The verified scale expectations are rewritten in exactly this variable.

noncomputable def Papers.AnsariRockel2024.hvV (w₁ w₂ w₃ : ℝ) : ℝ

The Heinen–Valdesogo mixing variable.

Equations

• Papers.AnsariRockel2024.hvV w₁ w₂ w₃ = w₃ / √((w₁ + w₃) * (w₂ + w₃))

theorem Papers.AnsariRockel2024.hv_integrand (r x y z : ℝ) : r * z ^ 2 / (√(z ^ 2 + x ^ 2) * √(z ^ 2 + y ^ 2)) = r * hvV (x ^ 2) (y ^ 2) (z ^ 2)

theorem Papers.AnsariRockel2024.student_spearmanRho_hv (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) : have μ := ProbabilityTheory.gammaProbability (ν / 2) (ν / 2) ⋯ ⋯; have W := fun (t : ℝ) => (√t)⁻¹ ^ 2; (Verification.studentBivariate r hr ν hν).spearmanRho = 6 / Real.pi * ∫ (a : ℝ), ∫ (t : ℝ × ℝ), Real.arcsin (r * hvV (W t.1) (W t.2) (W a)) ∂(↑μ).prod ↑μ ∂↑μ

Table 6: Student-t rho as (6/π)E[arcsin(rṼ₁)], Wᵢ inverse-gamma(ν/2,ν/2).

theorem Papers.AnsariRockel2024.laplace_spearmanRho_hv (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) : have μ := ProbabilityTheory.gammaProbability 1 1 ⋯ ⋯; have W := fun (t : ℝ) => √t ^ 2; (Verification.laplaceBivariate r hr).spearmanRho = 6 / Real.pi * ∫ (a : ℝ), ∫ (t : ℝ × ℝ), Real.arcsin (r * hvV (W t.1) (W t.2) (W a)) ∂(↑μ).prod ↑μ ∂↑μ

Table 6: Laplace rho as (6/π)E[arcsin(rṼ₂)], Wᵢ exponential(1).