← Copula mathematical handbook

Dependence coefficients from CDF discrepancies

All coefficients here are functionals of the deviation C(u,v) - u v of a bivariate copula from independence (cdfDeviation).

• Hoeffding's D = ∫ (C - Π)² dC integrates the squared discrepancy against the copula itself; hoeffdingDNormalized = 30 D takes the value one at the Fréchet–Hoeffding bounds.
• The Blum–Kiefer–Rosenblatt coefficient R = ∫ (C - Π)² dΠ integrates against independent uniform coordinates; 90 R is Hoeffding's Φ² (hoeffdingPhiSq, see hoeffdingPhiSq_eq_ninety_mul_blumKieferRosenblattR).
• For copulas (which always have atomless margins) the Bergsma–Dassios sign covariance τ* has the CDF representation 12 D + 24 R, which is used as its definition here.
• Distance correlation of the two uniform coordinates is √Φ².

The Schweizer–Wolff σ (schweizerWolff) and Hoeffding's Φ² (hoeffdingPhiSq) are defined in Copula.Measures.SchweizerWolff and Copula.Measures.Hoeffding; here they are rewritten in terms of cdfDeviation. References: Nelsen, An Introduction to Copulas, 2nd ed., §5.3; Blum, Kiefer and Rosenblatt (1961); Bergsma and Dassios (2014). No equivalence to finite-sample estimators is asserted.

noncomputable def ProbabilityTheory.Copula.cdfDeviation (C : Copula 2) (x : Fin 2 → ↑unitInterval) : ℝ

The difference between a bivariate copula CDF and the product CDF.

Equations

• C.cdfDeviation x = C.cdf x - ↑(x 0) * ↑(x 1)

theorem ProbabilityTheory.Copula.cdfDeviation_apply (C : Copula 2) (x : Fin 2 → ↑unitInterval) : C.cdfDeviation x = C.cdf x - ↑(x 0) * ↑(x 1)

theorem ProbabilityTheory.Copula.cdfDeviation_two (C : Copula 2) (u v : ↑unitInterval) : C.cdfDeviation ![u, v] = C.cdf ![u, v] - ↑u * ↑v

theorem ProbabilityTheory.Copula.continuous_cdfDeviation (C : Copula 2) : Continuous C.cdfDeviation

theorem ProbabilityTheory.Copula.integrable_cdfDeviation_sq (C : Copula 2) (μ : MeasureTheory.Measure (Fin 2 → ↑unitInterval)) [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.Integrable (fun (x : Fin 2 → ↑unitInterval) => C.cdfDeviation x ^ 2) μ

theorem ProbabilityTheory.Copula.integrable_abs_cdfDeviation (C : Copula 2) (μ : MeasureTheory.Measure (Fin 2 → ↑unitInterval)) [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.Integrable (fun (x : Fin 2 → ↑unitInterval) => |C.cdfDeviation x|) μ

@[simp]

theorem ProbabilityTheory.Copula.cdfDeviation_independence (x : Fin 2 → ↑unitInterval) : (independence 2).cdfDeviation x = 0

noncomputable def ProbabilityTheory.Copula.hoeffdingD (C : Copula 2) : ℝ

Unscaled population Hoeffding D = ∫ (C - Π)² dC.

Equations

• C.hoeffdingD = ∫ (x : Fin 2 → ↑unitInterval), C.cdfDeviation x ^ 2 ∂C.toMeasure

noncomputable def ProbabilityTheory.Copula.hoeffdingDNormalized (C : Copula 2) : ℝ

Hoeffding's coefficient scaled to take value one at the monotone extremes.

Equations

• C.hoeffdingDNormalized = 30 * C.hoeffdingD

noncomputable def ProbabilityTheory.Copula.blumKieferRosenblattR (C : Copula 2) : ℝ

Unscaled population Blum–Kiefer–Rosenblatt R = ∫ (C - Π)² dΠ.

Equations

• C.blumKieferRosenblattR = ∫ (x : Fin 2 → ↑unitInterval), C.cdfDeviation x ^ 2 ∂(ProbabilityTheory.Copula.independence 2).toMeasure

noncomputable def ProbabilityTheory.Copula.bergsmaDassiosTauStar (C : Copula 2) : ℝ

Bergsma–Dassios sign covariance in its atomless-marginal CDF representation. The unscaled convention has value 2/3 at both monotone extremes.

Equations

• C.bergsmaDassiosTauStar = 12 * C.hoeffdingD + 24 * C.blumKieferRosenblattR

noncomputable def ProbabilityTheory.Copula.distanceCorrelation (C : Copula 2) : ℝ

Distance correlation of the two uniform copula coordinates, √Φ². This is rank-transformed distance correlation, not distance correlation of arbitrary original margins.

Equations

• C.distanceCorrelation = √C.hoeffdingPhiSq

theorem ProbabilityTheory.Copula.hoeffdingPhiSq_eq_ninety_mul_blumKieferRosenblattR (C : Copula 2) : C.hoeffdingPhiSq = 90 * C.blumKieferRosenblattR

Hoeffding's Φ² is the normalized Blum–Kiefer–Rosenblatt coefficient 90 R.

theorem ProbabilityTheory.Copula.schweizerWolff_eq_integral_abs_cdfDeviation (C : Copula 2) : C.schweizerWolff = 12 * ∫ (x : Fin 2 → ↑unitInterval), |C.cdfDeviation x| ∂(independence 2).toMeasure

The Schweizer–Wolff σ in terms of cdfDeviation.

theorem ProbabilityTheory.Copula.hoeffdingD_nonneg (C : Copula 2) : 0 ≤ C.hoeffdingD

theorem ProbabilityTheory.Copula.blumKieferRosenblattR_nonneg (C : Copula 2) : 0 ≤ C.blumKieferRosenblattR

theorem ProbabilityTheory.Copula.bergsmaDassiosTauStar_nonneg (C : Copula 2) : 0 ≤ C.bergsmaDassiosTauStar

theorem ProbabilityTheory.Copula.distanceCorrelation_nonneg (C : Copula 2) : 0 ≤ C.distanceCorrelation

theorem ProbabilityTheory.Copula.distanceCorrelation_sq (C : Copula 2) : C.distanceCorrelation ^ 2 = C.hoeffdingPhiSq

@[simp]

theorem ProbabilityTheory.Copula.hoeffdingD_independence : (independence 2).hoeffdingD = 0

@[simp]

theorem ProbabilityTheory.Copula.blumKieferRosenblattR_independence : (independence 2).blumKieferRosenblattR = 0

@[simp]

theorem ProbabilityTheory.Copula.bergsmaDassiosTauStar_independence : (independence 2).bergsmaDassiosTauStar = 0

@[simp]

theorem ProbabilityTheory.Copula.distanceCorrelation_independence : (independence 2).distanceCorrelation = 0

theorem ProbabilityTheory.Copula.integral_independence_two (f : (Fin 2 → ↑unitInterval) → ℝ) (hf : Continuous f) : ∫ (x : Fin 2 → ↑unitInterval), f x ∂(independence 2).toMeasure = ∫ (u : ↑unitInterval) (v : ↑unitInterval), f ![u, v]

Integrals against the bivariate independence copula are iterated Lebesgue integrals, with the first coordinate outside.

theorem ProbabilityTheory.Copula.blumKieferRosenblattR_eq_zero_iff (C : Copula 2) : C.blumKieferRosenblattR = 0 ↔ C = independence 2

The uniform squared CDF discrepancy detects independence, including for singular copulas.

theorem ProbabilityTheory.Copula.bergsmaDassiosTauStar_eq_zero_iff (C : Copula 2) : C.bergsmaDassiosTauStar = 0 ↔ C = independence 2

theorem ProbabilityTheory.Copula.distanceCorrelation_eq_zero_iff (C : Copula 2) : C.distanceCorrelation = 0 ↔ C = independence 2