← Copula mathematical handbook

Gumbel CDF total positivity from log-convexity

theorem ProbabilityTheory.Copula.isTP2CDF_gumbel (θ : ℝ) (hθ : 1 ≤ θ) : (gumbel θ hθ).IsTP2CDF

The Gumbel–Hougaard CDF is TP2 for every finite θ ≥ 1. This does not assert an MTP2 Lebesgue density.

theorem ProbabilityTheory.Copula.isTP2CDF_tawn (θ : ℝ) (hθ : 1 ≤ θ) (α β : ↑unitInterval) : (tawn θ hθ α β).IsTP2CDF

Every Tawn copula has a TP2 CDF, including zero and unit weights. This does not assert an MTP2 Lebesgue density.