← Copula mathematical handbook

Symmetries of the CDF discrepancy coefficients

The coefficients of Copula.Measures.CDFDistance (Hoeffding's D, Blum–Kiefer–Rosenblatt R, Bergsma–Dassios τ*, distance correlation) as well as the Schweizer–Wolff σ and Hoeffding's Φ² are invariant under transposition and under reflecting one coordinate (Nelsen, An Introduction to Copulas, 2nd ed., §5.3: measures of dependence are invariant under (U,V) ↦ (U, 1 - V)).

theorem ProbabilityTheory.Copula.cdfDeviation_transpose (C : Copula 2) (u v : ↑unitInterval) : C.transpose.cdfDeviation ![u, v] = C.cdfDeviation ![v, u]

theorem ProbabilityTheory.Copula.cdfDeviation_reflect_second (C : Copula 2) (u v : ↑unitInterval) : (C.reflect {1}).cdfDeviation ![u, v] = -C.cdfDeviation ![u, unitInterval.symm v]

@[simp]

theorem ProbabilityTheory.Copula.hoeffdingD_transpose (C : Copula 2) : C.transpose.hoeffdingD = C.hoeffdingD

@[simp]

theorem ProbabilityTheory.Copula.blumKieferRosenblattR_transpose (C : Copula 2) : C.transpose.blumKieferRosenblattR = C.blumKieferRosenblattR

@[simp]

theorem ProbabilityTheory.Copula.bergsmaDassiosTauStar_transpose (C : Copula 2) : C.transpose.bergsmaDassiosTauStar = C.bergsmaDassiosTauStar

@[simp]

theorem ProbabilityTheory.Copula.distanceCorrelation_transpose (C : Copula 2) : C.transpose.distanceCorrelation = C.distanceCorrelation

theorem ProbabilityTheory.Copula.hoeffdingD_reflect_second (C : Copula 2) : (C.reflect {1}).hoeffdingD = C.hoeffdingD

theorem ProbabilityTheory.Copula.blumKieferRosenblattR_reflect_second (C : Copula 2) : (C.reflect {1}).blumKieferRosenblattR = C.blumKieferRosenblattR

theorem ProbabilityTheory.Copula.schweizerWolff_reflect_second (C : Copula 2) : (C.reflect {1}).schweizerWolff = C.schweizerWolff

The Schweizer–Wolff σ is invariant under reflecting the second coordinate.

theorem ProbabilityTheory.Copula.schweizerWolff_reflect_first (C : Copula 2) : (C.reflect {0}).schweizerWolff = C.schweizerWolff

The Schweizer–Wolff σ is invariant under reflecting the first coordinate.

theorem ProbabilityTheory.Copula.hoeffdingPhiSq_reflect_second (C : Copula 2) : (C.reflect {1}).hoeffdingPhiSq = C.hoeffdingPhiSq

Hoeffding's Φ² is invariant under reflecting the second coordinate.

theorem ProbabilityTheory.Copula.hoeffdingPhiSq_reflect_first (C : Copula 2) : (C.reflect {0}).hoeffdingPhiSq = C.hoeffdingPhiSq

Hoeffding's Φ² is invariant under reflecting the first coordinate.

theorem ProbabilityTheory.Copula.bergsmaDassiosTauStar_reflect_second (C : Copula 2) : (C.reflect {1}).bergsmaDassiosTauStar = C.bergsmaDassiosTauStar

theorem ProbabilityTheory.Copula.distanceCorrelation_reflect_second (C : Copula 2) : (C.reflect {1}).distanceCorrelation = C.distanceCorrelation