Gaussian Spearman rho #
Comparison with an independent copula reduces rho to the lower-quadrant probability of a centered Gaussian pair with half the original correlation.
theorem
Verification.gaussianBivariate_comparison_probability
{r s : ℝ}
(hr : r ∈ Set.Icc (-1) 1)
(hs : s ∈ Set.Icc (-1) 1)
:
((gaussianBivariate r hr).toMeasure.prod (gaussianBivariate s hs).toMeasure).real
{p : (Fin 2 → ↑unitInterval) × (Fin 2 → ↑unitInterval) | p.1 ≤ p.2} = (ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation ((r + s) / 2))).real
{x : EuclideanSpace ℝ (Fin 2) | x.ofLp 0 ≤ 0 ∧ x.ofLp 1 ≤ 0}