← Copula mathematical handbook

Dilution by independence

For the mixture a C + (1 - a) Π the deviation from independence scales by a, so σ scales by a, Φ² and R by a². Hoeffding's D and Blum–Kiefer–Rosenblatt R have different mixture laws because their integrating measures differ; the identities below distinguish the two definitions even when they happen to agree on a particular parametric family.

theorem ProbabilityTheory.Copula.cdfDeviation_mix_independence (C : Copula 2) (a : ↑unitInterval) (x : Fin 2 → ↑unitInterval) : (C.mix (independence 2) a).cdfDeviation x = ↑a * C.cdfDeviation x

theorem ProbabilityTheory.Copula.blumKieferRosenblattR_mix_independence (C : Copula 2) (a : ↑unitInterval) : (C.mix (independence 2) a).blumKieferRosenblattR = ↑a ^ 2 * C.blumKieferRosenblattR

theorem ProbabilityTheory.Copula.hoeffdingD_mix_independence (C : Copula 2) (a : ↑unitInterval) : (C.mix (independence 2) a).hoeffdingD = ↑a ^ 3 * C.hoeffdingD + ↑a ^ 2 * (1 - ↑a) * C.blumKieferRosenblattR

theorem ProbabilityTheory.Copula.schweizerWolff_mix_independence (C : Copula 2) (a : ↑unitInterval) : (C.mix (independence 2) a).schweizerWolff = ↑a * C.schweizerWolff

σ(a C + (1 - a) Π) = a σ(C).

theorem ProbabilityTheory.Copula.hoeffdingPhiSq_mix_independence (C : Copula 2) (a : ↑unitInterval) : (C.mix (independence 2) a).hoeffdingPhiSq = ↑a ^ 2 * C.hoeffdingPhiSq

Φ²(a C + (1 - a) Π) = a² Φ²(C).

theorem ProbabilityTheory.Copula.distanceCorrelation_mix_independence (C : Copula 2) (a : ↑unitInterval) : (C.mix (independence 2) a).distanceCorrelation = ↑a * C.distanceCorrelation