← Mathematical handbook

Exact Cuadras–Augé conditional law and all three Table 6 coefficients

theorem Papers.AnsariRockel2024.cuadrasAuge_conditionalCDF (δ v : ↑unitInterval) : (fun (u : ↑unitInterval) => (ProbabilityTheory.Copula.cuadrasAuge δ).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => Verification.cuadrasConditional δ u v

A conditional CDF version on the full closed parameter range; the value at the moving diagonal is irrelevant to the almost-everywhere identity.

theorem Papers.AnsariRockel2024.cuadrasAuge_rho (δ : ↑unitInterval) : (ProbabilityTheory.Copula.cuadrasAuge δ).spearmanRho = 3 * ↑δ / (4 - ↑δ)

Table 6: Spearman rho, including independence and comonotonicity.

theorem Papers.AnsariRockel2024.cuadrasAuge_xi (δ : ↑unitInterval) : (ProbabilityTheory.Copula.cuadrasAuge δ).chatterjeeXi = ↑δ ^ 2 / (2 - ↑δ)

Table 6 and Appendix A.5: Chatterjee xi on all of [0,1].

theorem Papers.AnsariRockel2024.cuadrasAuge_tau (δ : ↑unitInterval) : (ProbabilityTheory.Copula.cuadrasAuge δ).kendallTau = ↑δ / (2 - ↑δ)

Table 6: Kendall tau, including the singular comonotonic endpoint.

theorem Papers.AnsariRockel2024.cuadrasAuge_density_tp2 (δ : ↑unitInterval) : (ProbabilityTheory.Copula.cuadrasAuge δ).HasMTP2Density ↔ δ = 0

Table 5: the exact TP2-density domain, including the singular endpoint.

theorem Papers.AnsariRockel2024.cuadrasAuge_absolutelyContinuous (δ : ↑unitInterval) : (ProbabilityTheory.Copula.cuadrasAuge δ).toMeasure.AbsolutelyContinuous MeasureTheory.volume ↔ δ = 0

Positive parameters charge the diagonal, so absolute continuity holds only at independence.