← Mathematical handbook

Corrected Gaussian Chatterjee xi formula

theorem Verification.gaussian_xi_integral_quadrant {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) : ∫ (b : ℝ), ∫ (x : ℝ), ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) ((b - r * x) / √(1 - r ^ 2)) ^ 2 ∂ProbabilityTheory.gaussianReal 0 1 ∂ProbabilityTheory.gaussianReal 0 1 = (ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation ((1 + r ^ 2) / 2))).real {x : EuclideanSpace ℝ (Fin 2) | x.ofLp 0 ≤ 0 ∧ x.ofLp 1 ≤ 0}

theorem Verification.gaussianBivariate_chatterjeeXi {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (gaussianBivariate r hr).chatterjeeXi = 3 / Real.pi * Real.arcsin ((1 + r ^ 2) / 2) - 1 / 2