Gaussian Kendall tau on the closed correlation interval #
Strict normal-CDF monotonicity and Gaussian difference stability reduce the actual copula's Kendall functional to its Gaussian lower-quadrant probability. The singular endpoints are handled by their benchmark copulas.
theorem
Verification.gaussianBivariate_tau_quadrant
{r : ℝ}
(hr : r ∈ Set.Icc (-1) 1)
:
(gaussianBivariate r hr).kendallTau = 4 * (ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation r)).real
{x : EuclideanSpace ℝ (Fin 2) | x.ofLp 0 ≤ 0 ∧ x.ofLp 1 ≤ 0} - 1