← Copula mathematical handbook

Benchmarks for CDF discrepancy coefficients

The singular Fréchet–Hoeffding bounds M, W and the absolutely continuous FGM family check the normalizations of Hoeffding's D, Blum–Kiefer–Rosenblatt R, Hoeffding's Φ², Bergsma–Dassios τ* and distance correlation. In particular Φ²(M) = Φ²(W) = 1 (Nelsen, An Introduction to Copulas, 2nd ed., §5.3.1).

theorem ProbabilityTheory.Copula.integral_unit_bridge_sq (u : ↑unitInterval) : ∫ (v : ↑unitInterval), (min ↑u ↑v - ↑u * ↑v) ^ 2 = ↑u ^ 2 * (1 - ↑u) ^ 2 / 3

@[simp]

theorem ProbabilityTheory.Copula.hoeffdingD_comonotonic : (comonotonic 2).hoeffdingD = 1 / 30

@[simp]

theorem ProbabilityTheory.Copula.hoeffdingD_countermonotonic : countermonotonic.hoeffdingD = 1 / 30

@[simp]

theorem ProbabilityTheory.Copula.blumKieferRosenblattR_comonotonic : (comonotonic 2).blumKieferRosenblattR = 1 / 90

theorem ProbabilityTheory.Copula.cdfDeviation_fgm (θ : ℝ) (hθ : |θ| ≤ 1) (x : Fin 2 → ↑unitInterval) : (fgm θ hθ).cdfDeviation x = θ * (↑(x 0) * (1 - ↑(x 0))) * (↑(x 1) * (1 - ↑(x 1)))

theorem ProbabilityTheory.Copula.blumKieferRosenblattR_fgm (θ : ℝ) (hθ : |θ| ≤ 1) : (fgm θ hθ).blumKieferRosenblattR = θ ^ 2 / 900

@[simp]

theorem ProbabilityTheory.Copula.hoeffdingPhiSq_comonotonic : (comonotonic 2).hoeffdingPhiSq = 1

Hoeffding's Φ² of the upper Fréchet–Hoeffding bound is one.

@[simp]

theorem ProbabilityTheory.Copula.distanceCorrelation_comonotonic : (comonotonic 2).distanceCorrelation = 1

@[simp]

theorem ProbabilityTheory.Copula.bergsmaDassiosTauStar_comonotonic : (comonotonic 2).bergsmaDassiosTauStar = 2 / 3

@[simp]

theorem ProbabilityTheory.Copula.blumKieferRosenblattR_countermonotonic : countermonotonic.blumKieferRosenblattR = 1 / 90

@[simp]

theorem ProbabilityTheory.Copula.hoeffdingPhiSq_countermonotonic : countermonotonic.hoeffdingPhiSq = 1

Hoeffding's Φ² of the lower Fréchet–Hoeffding bound is one.

@[simp]

theorem ProbabilityTheory.Copula.distanceCorrelation_countermonotonic : countermonotonic.distanceCorrelation = 1

@[simp]

theorem ProbabilityTheory.Copula.bergsmaDassiosTauStar_countermonotonic : countermonotonic.bergsmaDassiosTauStar = 2 / 3

@[simp]

theorem ProbabilityTheory.Copula.hoeffdingDNormalized_independence : (independence 2).hoeffdingDNormalized = 0

@[simp]

theorem ProbabilityTheory.Copula.hoeffdingDNormalized_comonotonic : (comonotonic 2).hoeffdingDNormalized = 1

@[simp]

theorem ProbabilityTheory.Copula.hoeffdingDNormalized_countermonotonic : countermonotonic.hoeffdingDNormalized = 1