← Mathematical handbook

noncomputable def Verification.n22Diagonal (θ t : ℝ) : ℝ

Equations

• Verification.n22Diagonal θ t = (1 - Real.sin (min (2 * Real.arcsin (1 - t ^ θ)) (Real.pi / 2))) ^ θ⁻¹

theorem Verification.n22Diagonal_deriv_one {θ : ℝ} (hθ : 0 < θ) : HasDerivAt (n22Diagonal θ) 2 1

theorem Verification.nelsen22_upperTail (θ : ℝ) (hθ : θ ∈ Set.Icc 0 1) : (nelsen22 θ hθ).HasUpperTailDependence 0