← Mathematical handbook

theorem Verification.nelsen22_zero_diagonal {θ : ℝ} (hθ : 0 < θ) (hθ1 : θ ≤ 1) : ∃ (q : ↑unitInterval), 0 < q ∧ (nelsen22 θ ⋯).cdf ![q, q] = 0

theorem Verification.nelsen22_not_pqd {θ : ℝ} (hθ : 0 < θ) (hθ1 : θ ≤ 1) : ¬(nelsen22 θ ⋯).IsPQD

theorem Verification.nelsen22_not_ci {θ : ℝ} (hθ : 0 < θ) (hθ1 : θ ≤ 1) : ¬(nelsen22 θ ⋯).IsCI

theorem Verification.nelsen22_not_density_tp2 {θ : ℝ} (hθ : 0 < θ) (hθ1 : θ ≤ 1) : ¬(nelsen22 θ ⋯).HasMTP2Density

theorem Verification.nelsen22_lowerTail_positive {θ : ℝ} (hθ : 0 < θ) (hθ1 : θ ≤ 1) : (nelsen22 θ ⋯).HasLowerTailDependence 0

theorem Verification.nelsen22_isCI_iff (θ : ℝ) (hθ : θ ∈ Set.Icc 0 1) : (nelsen22 θ hθ).IsCI ↔ θ = 0

theorem Verification.nelsen22_density_tp2_iff (θ : ℝ) (hθ : θ ∈ Set.Icc 0 1) : (nelsen22 θ hθ).HasMTP2Density ↔ θ = 0

theorem Verification.nelsen22_lowerTail (θ : ℝ) (hθ : θ ∈ Set.Icc 0 1) : (nelsen22 θ hθ).HasLowerTailDependence 0