← Mathematical handbook

CDF-level TP2 for named Table 3 and 5 families

These are statements about the actual copula CDF. They do not assert MTP2 of a Lebesgue density, which is a separate property in the article.

theorem Papers.AnsariRockel2024.nelsen12_tp2_cdf (θ : ℝ) (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.nelsen12 θ hθ).IsTP2CDF

theorem Papers.AnsariRockel2024.nelsen14_tp2_cdf (θ : ℝ) (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.nelsen14 θ hθ).IsTP2CDF

theorem Papers.AnsariRockel2024.gumbel_tp2_cdf (θ : ℝ) (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.gumbel θ hθ).IsTP2CDF

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

theorem Papers.AnsariRockel2024.marshallOlkin_tp2_cdf (α β : ↑unitInterval) : (ProbabilityTheory.Copula.marshallOlkin α β).IsTP2CDF

theorem Papers.AnsariRockel2024.cuadrasAuge_tp2_cdf (α : ↑unitInterval) : (ProbabilityTheory.Copula.cuadrasAuge α).IsTP2CDF