← Mathematical handbook

noncomputable def Verification.n21UpperCore (θ s : ℝ) : ℝ

Equations

• Verification.n21UpperCore θ s = 1 - (2 * (1 - s) ^ θ⁻¹ - 1) ^ θ

theorem Verification.n21UpperCore_deriv_zero {θ : ℝ} (hθ : 0 < θ) : HasDerivAt (n21UpperCore θ) 2 0

theorem Verification.nelsen21_upperTail (θ : ℝ) (hθ : 1 ≤ θ) : (nelsen21 θ hθ).HasUpperTailDependence (2 - 2 ^ θ⁻¹)

theorem Verification.nelsen21_not_nqd_above_one (θ : ℝ) (hθ : 1 < θ) : ¬(nelsen21 θ ⋯).IsNQD

theorem Verification.nelsen21_isCD_iff (θ : ℝ) (hθ : 1 ≤ θ) : (nelsen21 θ hθ).IsCD ↔ θ = 1

theorem Verification.nelsen21_isNQD_iff (θ : ℝ) (hθ : 1 ≤ θ) : (nelsen21 θ hθ).IsNQD ↔ θ = 1