Documentation

Copula.Dependence.NelsenEndpoints

← Copula mathematical handbook

Dependence properties at the Nelsen 12 and 14 lower endpoints #

Both families equal Clayton(1) at parameter one. These results are deliberately restricted to that endpoint; they do not establish the full parameter rows.

source
theorem ProbabilityTheory.Copula.isCI_nelsen12_one :
(nelsen12 1 ⋯).IsCI
source
theorem ProbabilityTheory.Copula.isCI_nelsen14_one :
(nelsen14 1 ⋯).IsCI
source
theorem ProbabilityTheory.Copula.isTP2CDF_nelsen12_one :
(nelsen12 1 ⋯).IsTP2CDF
source
theorem ProbabilityTheory.Copula.isTP2CDF_nelsen14_one :
(nelsen14 1 ⋯).IsTP2CDF
source
theorem ProbabilityTheory.Copula.hasMTP2Density_nelsen12_one :
(nelsen12 1 ⋯).HasMTP2Density
source
theorem ProbabilityTheory.Copula.hasMTP2Density_nelsen14_one :
(nelsen14 1 ⋯).HasMTP2Density
source
theorem ProbabilityTheory.Copula.not_isCD_nelsen12_one :
¬(nelsen12 1 ⋯).IsCD
source
theorem ProbabilityTheory.Copula.not_isCD_nelsen14_one :
¬(nelsen14 1 ⋯).IsCD
source
theorem ProbabilityTheory.Copula.isPQD_nelsen12 (θ : ℝ) (hθ : 1 ≤ θ) :
(nelsen12 θ hθ).IsPQD

All Nelsen 12 members are PQD: the parameter order puts them above the positive Clayton(1) endpoint. This is weaker than the open CI row.

source
theorem ProbabilityTheory.Copula.isTP2CDF_nelsen12 (θ : ℝ) (hθ : 1 ≤ θ) :
(nelsen12 θ hθ).IsTP2CDF

Nelsen 12 has a TP2 CDF for every finite admissible parameter.

source
theorem ProbabilityTheory.Copula.isTP2CDF_nelsen14 (θ : ℝ) (hθ : 1 ≤ θ) :
(nelsen14 θ hθ).IsTP2CDF

Nelsen 14 has a TP2 CDF for every finite admissible parameter.

source
theorem ProbabilityTheory.Copula.isPQD_nelsen14 (θ : ℝ) (hθ : 1 ≤ θ) :
(nelsen14 θ hθ).IsPQD

Every finite Nelsen 14 copula is positively quadrant dependent.

source
theorem ProbabilityTheory.Copula.not_isCD_nelsen12 (θ : ℝ) (hθ : 1 ≤ θ) :
¬(nelsen12 θ hθ).IsCD

Nelsen 12 cannot be conditionally decreasing at any finite admissible parameter: its lower-tail coefficient is strictly positive.

source
theorem ProbabilityTheory.Copula.not_isCD_nelsen14 (θ : ℝ) (hθ : 1 ≤ θ) :
¬(nelsen14 θ hθ).IsCD

Nelsen 14 cannot be conditionally decreasing at any finite admissible parameter: its lower-tail coefficient is one half.