Rank correlations of the bivariate Gaussian copula #

For the bivariate Gaussian copula C_r with correlation r ∈ [-1, 1]:

blomqvistBeta_bivariateGaussian: β(C_r) = (2/π) arcsin r (Sheppard's formula P(X ≤ 0, Y ≤ 0) = 1/4 + arcsin r / (2π));
kendallTau_bivariateGaussian: τ(C_r) = (2/π) arcsin r;
spearmanRho_bivariateGaussian: ρ_S(C_r) = (6/π) arcsin (r/2).

All three reduce to Sheppard's orthant formula (orthant_nonpos_of_linear_laws): Kendall's tau is 4 P(X' ≤ X, Y' ≤ Y) − 1 for an independent copy (X', Y'), and (X − X', Y − Y') is bivariate normal with correlation r; Spearman's rho is 12 P(X' ≤ X, Y'' ≤ Y) − 3 for independent X', Y'' ~ N(0, 1), and (X − X', Y − Y'') is bivariate normal with correlation r/2.

References #

W. F. Sheppard (1899); K. Pearson (1907) for ρ_S; W. H. Kruskal, Ordinal measures of association, J. Amer. Statist. Assoc. 53 (1958), 814–861.
R. B. Nelsen, An Introduction to Copulas, 2nd ed., Springer 2006, §5.1.
H. Joe, Dependence Modeling with Copulas, CRC Press 2014, §4.3.

source

theorem ProbabilityTheory.Copula.corr_quadratic_nonneg {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (a b : ℝ) :

0 ≤ a ^ 2 + 2 * a * b * r + b ^ 2

The variance a² + 2abr + b² of aX + bY is nonnegative for |r| ≤ 1.

source

theorem ProbabilityTheory.Copula.integral_measureReal_prodMk {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure β) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {S : Set (α × β)} (hS : MeasurableSet S) :

∫ (x : α), ν.real (Prod.mk x ⁻¹' S) ∂μ = (μ.prod ν).real S

The integral of a section measure is the measure of the set in the product.

source

theorem ProbabilityTheory.Copula.map_linear_sub_prod {μ ν : MeasureTheory.Measure (ℝ × ℝ)} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] (a b : ℝ) {v w : NNReal} (hμ : MeasureTheory.Measure.map (fun (p : ℝ × ℝ) => a * p.1 + b * p.2) μ = gaussianReal 0 v) (hν : MeasureTheory.Measure.map (fun (p : ℝ × ℝ) => a * p.1 + b * p.2) ν = gaussianReal 0 w) :

MeasureTheory.Measure.map (fun (z : (ℝ × ℝ) × ℝ × ℝ) => a * (z.2.1 - z.1.1) + b * (z.2.2 - z.1.2)) (μ.prod ν) = gaussianReal 0 (↑v + ↑w).toNNReal

If L(p) = a p₁ + b p₂ has centered Gaussian laws N(0, v) under μ and N(0, w) under ν, then L(q) − L(p) has law N(0, v + w) under μ ⊗ ν (for (p, q) ~ μ ⊗ ν).

source