← Mathematical handbook

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

Equations

• Verification.n16DiagBase θ t = 2 * t ^ 2 + (θ - 1) * t - 2 * θ

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

Equations

• Verification.n16Diagonal θ t = t * (2 * θ / (√(Verification.n16DiagBase θ t ^ 2 + 4 * θ * t ^ 2) - Verification.n16DiagBase θ t))

theorem Verification.n16Diagonal_eq {θ : ℝ} (hθ : 0 < θ) (t : ↑unitInterval) : n16Diagonal θ ↑t = (nelsen16 θ ⋯).diagonal t

theorem Verification.n16Diagonal_deriv_zero {θ : ℝ} (hθ : 0 < θ) : HasDerivAt (n16Diagonal θ) (1 / 2) 0

theorem Verification.nelsen16_lowerTail_pos {θ : ℝ} (hθ : 0 < θ) : (nelsen16 θ ⋯).HasLowerTailDependence (1 / 2)

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

theorem Verification.nelsen16_upperTail (θ : ℝ) (hθ : 0 ≤ θ) : (nelsen16 θ hθ).HasUpperTailDependence 0

theorem Verification.nelsen16_tails (θ : ℝ) (hθ : 0 ≤ θ) : (nelsen16 θ hθ).HasLowerTailDependence (if θ = 0 then 0 else 1 / 2) ∧ (nelsen16 θ hθ).HasUpperTailDependence 0