← Mathematical handbook

Nelsen 8 dependence exclusions in Ansari–Rockel 2024

theorem Papers.AnsariRockel2024.nelsen8_not_pqd (θ : ℝ) (hθ : 1 ≤ θ) : ¬(ProbabilityTheory.Copula.nelsen8 θ hθ).IsPQD

Table 3 support: every Nelsen 8 member fails positive quadrant dependence.

theorem Papers.AnsariRockel2024.nelsen8_not_ci (θ : ℝ) (hθ : 1 ≤ θ) : ¬(ProbabilityTheory.Copula.nelsen8 θ hθ).IsCI

Table 3: no Nelsen 8 member is conditionally increasing.

theorem Papers.AnsariRockel2024.nelsen8_not_tp2_cdf (θ : ℝ) (hθ : 1 ≤ θ) : ¬(ProbabilityTheory.Copula.nelsen8 θ hθ).IsTP2CDF

Table 3: the Nelsen 8 CDF is never TP2.

theorem Papers.AnsariRockel2024.nelsen8_not_mtp2_density (θ : ℝ) (hθ : 1 ≤ θ) : ¬(ProbabilityTheory.Copula.nelsen8 θ hθ).HasMTP2Density

Table 3: no Nelsen 8 member admits an MTP2 density.

theorem Papers.AnsariRockel2024.nelsen8_cd_one : (ProbabilityTheory.Copula.nelsen8 1 ⋯).IsCD

Table 3: the θ=1 lower-Fréchet member is conditionally decreasing.

theorem Papers.AnsariRockel2024.nelsen8_not_cd (θ : ℝ) (hθ : 1 < θ) : ¬(ProbabilityTheory.Copula.nelsen8 θ ⋯).IsCD

Table 3: all Nelsen 8 parameters strictly above one fail CD.

theorem Papers.AnsariRockel2024.nelsen8_cd_iff (θ : ℝ) (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.nelsen8 θ hθ).IsCD ↔ θ = 1

Table 3: Nelsen 8 is CD exactly at its lower-Fréchet endpoint.