← Mathematical handbook

Remaining mapping rows: Cuadras–Augé CDF and endpoints, Marshall–Olkin endpoint,

and the TP2 ⇒ CI implication

theorem Papers.AnsariRockel2024.cuadrasAuge_cdf (δ u v : ↑unitInterval) : (ProbabilityTheory.Copula.cuadrasAuge δ).cdf ![u, v] = min ↑u ↑v * max ↑u ↑v ^ (1 - ↑δ)

Table 1: the Cuadras–Augé CDF min(u,v)·max(u,v)^(1-δ) on the closed square.

theorem Papers.AnsariRockel2024.cuadrasAuge_one : ProbabilityTheory.Copula.cuadrasAuge 1 = ProbabilityTheory.Copula.comonotonic 2

Table 4: Cuadras–Augé at δ=1 is the comonotonic copula M.

theorem Papers.AnsariRockel2024.cuadrasAuge_zero : ProbabilityTheory.Copula.cuadrasAuge 0 = ProbabilityTheory.Copula.independence 2

Table 4: Cuadras–Augé at δ=0 is independence.

theorem Papers.AnsariRockel2024.marshallOlkin_one_one_eq : ProbabilityTheory.Copula.marshallOlkin 1 1 = ProbabilityTheory.Copula.comonotonic 2

Table 4: Marshall–Olkin with both weights one is M.

theorem Papers.AnsariRockel2024.marshallOlkin_diag (δ : ↑unitInterval) : ProbabilityTheory.Copula.marshallOlkin δ δ = ProbabilityTheory.Copula.cuadrasAuge δ

Table 4: equal Marshall–Olkin weights give the Cuadras–Augé subfamily.

theorem Papers.AnsariRockel2024.mtp2_density_isCI {C : ProbabilityTheory.Copula 2} (h : C.HasMTP2Density) : C.IsCI

Section 2: a TP2 (MTP2) Lebesgue density implies conditional increasingness.