← Mathematical handbook

CDF-level total positivity of Ali–Mikhail–Haq copulas

This concerns TP2 of the CDF and does not assert an MTP2 Lebesgue density.

theorem ProbabilityTheory.Copula.isTP2CDF_amh (θ : ℝ) (hmin : -1 ≤ θ) (hmax : θ ≤ 1) (hθ : 0 ≤ θ) : (amh θ hmin hmax).IsTP2CDF

For θ≥0, the AMH CDF itself is TP2 on the entire closed square.

theorem ProbabilityTheory.Copula.isTP2CDF_amh_iff (θ : ℝ) (hmin : -1 ≤ θ) (hmax : θ ≤ 1) : (amh θ hmin hmax).IsTP2CDF ↔ 0 ≤ θ

The AMH CDF is TP2 exactly for nonnegative parameters.

theorem ProbabilityTheory.Copula.not_hasMTP2Density_amh_of_neg (θ : ℝ) (hmin : -1 ≤ θ) (hmax : θ ≤ 1) (hθ : θ < 0) : ¬(amh θ hmin hmax).HasMTP2Density

No negative AMH parameter has an MTP2 Lebesgue density.

theorem ProbabilityTheory.Copula.hasMTP2Density_amh_zero : (amh 0 ⋯ ⋯).HasMTP2Density

At θ=0, AMH has the constant independence MTP2 density.

theorem ProbabilityTheory.Copula.hasMTP2Density_amh_one : (amh 1 ⋯ ⋯).HasMTP2Density

At θ=1, AMH has the actual Clayton(1) MTP2 density.