← Mathematical handbook

CDF total positivity and a singular density endpoint for Clayton copulas

This classifies IsTP2CDF, a property distinct from MTP2 of a density. The W endpoint also has no Lebesgue MTP2 density.

theorem ProbabilityTheory.Copula.isTP2CDF_clayton_positive (θ : ℝ) (hθ : 0 < θ) : (clayton 2 θ hθ).IsTP2CDF

Every positive bivariate Clayton copula has a TP2 CDF.

theorem ProbabilityTheory.Copula.not_isTP2CDF_clayton_negative (θ : ℝ) (hθ : -1 ≤ θ) (hn : θ < 0) : ¬(claytonNegative θ hθ hn).IsTP2CDF

A negative Clayton copula does not have a TP2 CDF.

theorem ProbabilityTheory.Copula.not_hasMTP2Density_clayton_negative_one : ¬(claytonNegative (-1) ⋯ ⋯).HasMTP2Density

The negative endpoint is W and therefore has no Lebesgue MTP2 density.