← Copula mathematical handbook

The uniform distance to independence

Schweizer and Wolff (1981) proposed normalized L¹, L² and L∞ distances between a copula C and the independence copula Π (Nelsen, An Introduction to Copulas, 2nd ed., §5.3.1). The L¹ version is schweizerWolff (σ), the square of the L² version is Hoeffding's hoeffdingPhiSq (Φ²), and this file adds the uniform version

κ(C) = 4 sup |C(u,v) - uv|.

We prove: the supremum is attained, κ takes values in [0,1], vanishes exactly under independence, is invariant under transposition and reflections, is 4-Lipschitz for the uniform distance of copulas, and dominates |β| (Blomqvist's beta) and σ / 3. Iterated-integral forms of σ and Φ² are also recorded. The equality case κ = 1 ↔ |β| = 1 is in Copula.Measures.Bounds.

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

Schweizer–Wolff's uniform (L∞) distance to independence, κ(C) = 4 sup |C - Π|.

Equations

• C.schweizerWolffKappa = 4 * C.uniformCDFDistance (ProbabilityTheory.Copula.independence 2)

theorem ProbabilityTheory.Copula.abs_cdfDeviation_le_schweizerWolffKappa (C : Copula 2) (x : Fin 2 → ↑unitInterval) : 4 * |C.cdfDeviation x| ≤ C.schweizerWolffKappa

theorem ProbabilityTheory.Copula.abs_cdf_sub_mul_le_schweizerWolffKappa (C : Copula 2) (u v : ↑unitInterval) : 4 * |C.cdf ![u, v] - ↑u * ↑v| ≤ C.schweizerWolffKappa

theorem ProbabilityTheory.Copula.schweizerWolffKappa_le_iff (C : Copula 2) (q : ℝ) : C.schweizerWolffKappa ≤ q ↔ ∀ (u v : ↑unitInterval), 4 * |C.cdf ![u, v] - ↑u * ↑v| ≤ q

theorem ProbabilityTheory.Copula.schweizerWolffKappa_nonneg (C : Copula 2) : 0 ≤ C.schweizerWolffKappa

theorem ProbabilityTheory.Copula.exists_schweizerWolffKappa_eq (C : Copula 2) : ∃ (u : ↑unitInterval) (v : ↑unitInterval), 4 * |C.cdf ![u, v] - ↑u * ↑v| = C.schweizerWolffKappa

The supremum defining κ is attained.

theorem ProbabilityTheory.Copula.schweizerWolffKappa_le_one (C : Copula 2) : C.schweizerWolffKappa ≤ 1

theorem ProbabilityTheory.Copula.schweizerWolffKappa_mem_Icc (C : Copula 2) : C.schweizerWolffKappa ∈ Set.Icc 0 1

theorem ProbabilityTheory.Copula.schweizerWolffKappa_eq_zero_iff (C : Copula 2) : C.schweizerWolffKappa = 0 ↔ C = independence 2

@[simp]

theorem ProbabilityTheory.Copula.schweizerWolffKappa_independence : (independence 2).schweizerWolffKappa = 0

theorem ProbabilityTheory.Copula.schweizerWolffKappa_pos_iff (C : Copula 2) : 0 < C.schweizerWolffKappa ↔ C ≠ independence 2

theorem ProbabilityTheory.Copula.schweizerWolffKappa_le_of_abs_eq (C D : Copula 2) (h : ∀ (u v : ↑unitInterval), ∃ (u' : ↑unitInterval) (v' : ↑unitInterval), |C.cdf ![u, v] - ↑u * ↑v| = |D.cdf ![u', v'] - ↑u' * ↑v'|) : C.schweizerWolffKappa ≤ D.schweizerWolffKappa

Two copulas with the same absolute deviation from independence at every point have the same κ.

@[simp]

theorem ProbabilityTheory.Copula.schweizerWolffKappa_transpose (C : Copula 2) : C.transpose.schweizerWolffKappa = C.schweizerWolffKappa

@[simp]

theorem ProbabilityTheory.Copula.schweizerWolffKappa_reflect_second (C : Copula 2) : (C.reflect {1}).schweizerWolffKappa = C.schweizerWolffKappa

@[simp]

theorem ProbabilityTheory.Copula.schweizerWolffKappa_reflect_first (C : Copula 2) : (C.reflect {0}).schweizerWolffKappa = C.schweizerWolffKappa

theorem ProbabilityTheory.Copula.abs_schweizerWolffKappa_sub_le (C D : Copula 2) : |C.schweizerWolffKappa - D.schweizerWolffKappa| ≤ 4 * C.uniformCDFDistance D

κ is 4-Lipschitz for the uniform distance of copulas.

theorem ProbabilityTheory.Copula.continuous_schweizerWolffKappa_mix (C D : Copula 2) : Continuous fun (a : ↑unitInterval) => (C.mix D a).schweizerWolffKappa

κ is continuous along mixtures.

theorem ProbabilityTheory.Copula.abs_blomqvistBeta_le_schweizerWolffKappa (C : Copula 2) : |C.blomqvistBeta| ≤ C.schweizerWolffKappa

theorem ProbabilityTheory.Copula.schweizerWolff_eq_iterated (C : Copula 2) : C.schweizerWolff = 12 * ∫ (v : ↑unitInterval) (u : ↑unitInterval), |C.cdf ![u, v] - ↑u * ↑v|

The L¹ distance as an iterated integral with the second coordinate outside.

theorem ProbabilityTheory.Copula.hoeffdingPhiSq_eq_iterated (C : Copula 2) : C.hoeffdingPhiSq = 90 * ∫ (v : ↑unitInterval) (u : ↑unitInterval), (C.cdf ![u, v] - ↑u * ↑v) ^ 2

Hoeffding's Φ² as an iterated integral with the second coordinate outside.

theorem ProbabilityTheory.Copula.schweizerWolff_le_three_mul_schweizerWolffKappa (C : Copula 2) : C.schweizerWolff ≤ 3 * C.schweizerWolffKappa

The L¹ distance is dominated by the uniform one: σ ≤ 3 κ.

theorem ProbabilityTheory.Copula.hoeffdingPhiSq_le_schweizerWolffKappa_sq (C : Copula 2) : C.hoeffdingPhiSq ≤ 45 / 8 * C.schweizerWolffKappa ^ 2

Hoeffding's Φ² is dominated by the uniform distance: Φ² ≤ 90/16 κ².