← Mathematical handbook

theorem Papers.AnsariRockel2024.elliptical_rho_conditional_comparison {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (a b c : ℝ) (hab : 0 < a ^ 2 + b ^ 2) (hac : 0 < a ^ 2 + c ^ 2) : (((ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1)).prod ((ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1))).real {p : (ℝ × ℝ) × ℝ × ℝ | b * p.1.2 ≤ a * p.1.1 ∧ c * p.2.2 ≤ a * (r * p.1.1 + √(1 - r ^ 2) * p.2.1)} = 1 / 4 + Real.arcsin (r * a ^ 2 / (√(a ^ 2 + b ^ 2) * √(a ^ 2 + c ^ 2))) / (2 * Real.pi)

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

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