← Mathematical handbook

noncomputable def Verification.n17Diagonal (a t : ℝ) : ℝ

Equations

• Verification.n17Diagonal a t = (1 + ((1 + t) ^ a - 1) ^ 2 / Verification.n17A a) ^ a⁻¹ - 1

theorem Verification.n17Diagonal_deriv {a t : ℝ} (ht : 1 + t ≠ 0) (hb : 1 + ((1 + t) ^ a - 1) ^ 2 / n17A a ≠ 0) : HasDerivAt (n17Diagonal a) (2 * ((1 + t) ^ a - 1) * (a * (1 + t) ^ (a - 1)) / n17A a * a⁻¹ * (1 + ((1 + t) ^ a - 1) ^ 2 / n17A a) ^ (a⁻¹ - 1)) t

theorem Verification.n17Diagonal_deriv_zero (a : ℝ) : HasDerivAt (n17Diagonal a) 0 0

theorem Verification.n17Diagonal_deriv_one {a : ℝ} (ha : a ≠ 0) : HasDerivAt (n17Diagonal a) 2 1

theorem Verification.n17Diagonal_eq (θ : ℝ) (hθ : θ ≠ 0) (t : ↑unitInterval) : n17Diagonal (-θ) ↑t = (nelsen17 θ hθ).diagonal t

theorem Verification.nelsen17_tails (θ : ℝ) (hθ : θ ≠ 0) : (nelsen17 θ hθ).HasLowerTailDependence 0 ∧ (nelsen17 θ hθ).HasUpperTailDependence 0