← Mathematical handbook

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

Equations

• Verification.n13Diagonal θ t = if t = 0 then 0 else Real.exp (1 - (2 * (1 - Real.log t) ^ θ - 1) ^ θ⁻¹)

theorem Verification.n13Diagonal_eq (θ : ℝ) (hθ : 0 < θ) (t : ↑unitInterval) : n13Diagonal θ ↑t = (nelsen13 θ ⋯).diagonal t

theorem Verification.n13Diagonal_deriv_one (θ : ℝ) (hθ : 0 < θ) : HasDerivAt (n13Diagonal θ) 2 1

theorem Verification.nelsen13_upperTail (θ : ℝ) (hθ : 0 ≤ θ) : (nelsen13 θ hθ).HasUpperTailDependence 0

theorem Verification.nelsen13_lowerTail_pos (θ : ℝ) (hθ : 0 < θ) : (nelsen13 θ ⋯).HasLowerTailDependence 0

theorem Verification.nelsen13_tails (θ : ℝ) (hθ : 0 ≤ θ) : (nelsen13 θ hθ).HasLowerTailDependence 0 ∧ (nelsen13 θ hθ).HasUpperTailDependence 0