← Mathematical handbook

theorem ProbabilityTheory.Copula.not_isCD_nelsen2 (θ : ℝ) (hθ : 1 < θ) : ¬(nelsen2 θ ⋯).IsCD

Positive upper-tail dependence excludes CD at every parameter above one.

theorem ProbabilityTheory.Copula.isCD_nelsen2_one : (nelsen2 1 ⋯).IsCD

The lower-Fréchet Nelsen 2 endpoint is CD.

theorem ProbabilityTheory.Copula.isCD_nelsen2_iff (θ : ℝ) (hθ : 1 ≤ θ) : (nelsen2 θ hθ).IsCD ↔ θ = 1

Nelsen 2 is CD exactly at θ = 1.

theorem ProbabilityTheory.Copula.not_isPQD_nelsen2 (θ : ℝ) (hθ : 1 ≤ θ) : ¬(nelsen2 θ hθ).IsPQD

A positive diagonal point has zero CDF for every finite parameter.

theorem ProbabilityTheory.Copula.not_isCI_nelsen2 (θ : ℝ) (hθ : 1 ≤ θ) : ¬(nelsen2 θ hθ).IsCI

No Nelsen 2 member is conditionally increasing.

theorem ProbabilityTheory.Copula.not_isTP2CDF_nelsen2 (θ : ℝ) (hθ : 1 ≤ θ) : ¬(nelsen2 θ hθ).IsTP2CDF

No Nelsen 2 CDF is TP2.

theorem ProbabilityTheory.Copula.not_hasMTP2Density_nelsen2 (θ : ℝ) (hθ : 1 ≤ θ) : ¬(nelsen2 θ hθ).HasMTP2Density

No Nelsen 2 copula has an MTP2 Lebesgue density.

theorem ProbabilityTheory.Copula.lowerOrthantLE_nelsen2 {θ η : ℝ} (hθ : 1 ≤ θ) (hη : 1 ≤ η) (hθη : θ ≤ η) : (nelsen2 θ hθ).LowerOrthantLE (nelsen2 η hη)

Nelsen 2 increases in lower-orthant order throughout its parameter range.