← Copula mathematical handbook

The deviation C - Π of a bivariate copula from independence

Scaffolding for the Schweizer–Wolff measure σ and Hoeffding's Φ² (Nelsen, An Introduction to Copulas, 2nd ed., Section 5.3). Both are integrals of a continuous function φ of the deviation C(u,v) - u v against the uniform measure on [0,1]². This file collects the common facts: continuity, integrability, invariance under transposition and survival copulas, the vanishing criterion, and the link ρ = 12 ∫∫ (C - Π) with Spearman's rho (Nelsen Section 5.1.2).

theorem ProbabilityTheory.Copula.cdf_independence_two (x : Fin 2 → ↑unitInterval) : (independence 2).cdf x = ↑(x 0) * ↑(x 1)

theorem ProbabilityTheory.Copula.integral_independence_coord_mul : ∫ (x : Fin 2 → ↑unitInterval), ↑(x 0) * ↑(x 1) ∂(independence 2).toMeasure = 1 / 4

theorem ProbabilityTheory.Copula.continuous_cdf_sub_mul (C : Copula 2) : Continuous fun (x : Fin 2 → ↑unitInterval) => C.cdf x - ↑(x 0) * ↑(x 1)

The deviation C(u,v) - u v from independence is continuous.

theorem ProbabilityTheory.Copula.integrable_comp_cdf_sub_mul {φ : ℝ → ℝ} (hφ : Continuous φ) (C : Copula 2) (μ : MeasureTheory.Measure (Fin 2 → ↑unitInterval)) [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.Integrable (fun (x : Fin 2 → ↑unitInterval) => φ (C.cdf x - ↑(x 0) * ↑(x 1))) μ

theorem ProbabilityTheory.Copula.integral_independence_swap (f : (Fin 2 → ↑unitInterval) → ℝ) (hf : Measurable f) : ∫ (x : Fin 2 → ↑unitInterval), f x ∂(independence 2).toMeasure = ∫ (x : Fin 2 → ↑unitInterval), f ![x 1, x 0] ∂(independence 2).toMeasure

The uniform measure on [0,1]² is invariant under exchanging the coordinates.

theorem ProbabilityTheory.Copula.integral_independence_reflect (f : (Fin 2 → ↑unitInterval) → ℝ) (hf : Measurable f) : ∫ (x : Fin 2 → ↑unitInterval), f x ∂(independence 2).toMeasure = ∫ (x : Fin 2 → ↑unitInterval), f (reflectPoint Finset.univ x) ∂(independence 2).toMeasure

The uniform measure on [0,1]² is invariant under x ↦ 1 - x.

theorem ProbabilityTheory.Copula.integral_comp_cdf_sub_transpose (φ : ℝ → ℝ) (hφ : Continuous φ) (C : Copula 2) : ∫ (x : Fin 2 → ↑unitInterval), φ (C.transpose.cdf x - ↑(x 0) * ↑(x 1)) ∂(independence 2).toMeasure = ∫ (x : Fin 2 → ↑unitInterval), φ (C.cdf x - ↑(x 0) * ↑(x 1)) ∂(independence 2).toMeasure

Functionals of the deviation C - Π are invariant under transposition.

theorem ProbabilityTheory.Copula.integral_comp_cdf_sub_survival (φ : ℝ → ℝ) (hφ : Continuous φ) (C : Copula 2) : ∫ (x : Fin 2 → ↑unitInterval), φ (C.survivalCopula.cdf x - ↑(x 0) * ↑(x 1)) ∂(independence 2).toMeasure = ∫ (x : Fin 2 → ↑unitInterval), φ (C.cdf x - ↑(x 0) * ↑(x 1)) ∂(independence 2).toMeasure

Functionals of the deviation C - Π are invariant under passing to the survival copula.

theorem ProbabilityTheory.Copula.eq_independence_of_integral_comp_eq_zero {φ : ℝ → ℝ} (hφ : Continuous φ) (hnn : ∀ (t : ℝ), 0 ≤ φ t) (hz : ∀ (t : ℝ), φ t = 0 → t = 0) {C : Copula 2} (h : ∫ (x : Fin 2 → ↑unitInterval), φ (C.cdf x - ↑(x 0) * ↑(x 1)) ∂(independence 2).toMeasure = 0) : C = independence 2

If a nonnegative continuous function of the deviation C - Π integrates to zero, then C is the independence copula (a continuous nonnegative function that integrates to zero against a measure with full support vanishes identically).

theorem ProbabilityTheory.Copula.spearmanRho_eq_twelve_integral_cdf_sub (C : Copula 2) : C.spearmanRho = 12 * ∫ (x : Fin 2 → ↑unitInterval), C.cdf x - ↑(x 0) * ↑(x 1) ∂(independence 2).toMeasure

Spearman's rho as a multiple of the integral of C - Π (Nelsen Section 5.1.2).