← Mathematical handbook

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

Equations

• Verification.n17LogDeriv a t = -t + (a⁻¹ - 1) * Real.log (Verification.n17Base a t)

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

Equations

• Verification.n17LogDerivPrime a t = -1 - (a⁻¹ - 1) * Verification.n17A a * Real.exp (-t) / Verification.n17Base a t

theorem Verification.n17LogDeriv_deriv {a t : ℝ} (ht : 0 ≤ t) : HasDerivAt (n17LogDeriv a) (n17LogDerivPrime a t) t

theorem Verification.n17LogDeriv_deriv2 {a t : ℝ} (ht : 0 ≤ t) : HasDerivAt (n17LogDerivPrime a) ((a⁻¹ - 1) * n17A a * Real.exp (-t) / n17Base a t ^ 2) t

theorem Verification.n17PsiDeriv_logconvex {a : ℝ} (ha : a ≠ 0) (ha1 : a ≤ 1) : ConvexOn ℝ (Set.Ioi 0) fun (t : ℝ) => Real.log (-n17PsiDeriv a t)

theorem Verification.n17Ratio_lt_one {a u : ℝ} (ha : a ≠ 0) (hu : u ∈ Set.Ioo 0 1) : n17Ratio a u < 1

theorem Verification.n17Inv_deriv {a u : ℝ} (ha : a ≠ 0) (hu : 0 < u) : HasDerivAt (fun (x : ℝ) => -Real.log (n17Ratio a x)) (-a * (1 + u) ^ (a - 1) / ((1 + u) ^ a - 1)) u

theorem Verification.nelsen17_isCI (θ : ℝ) (hθ : θ ≠ 0) (hθ1 : -1 ≤ θ) : (nelsen17 θ hθ).IsCI

theorem Verification.n17PsiDeriv_logconcave {a : ℝ} (ha : a ≠ 0) (ha1 : 1 ≤ a) : ConcaveOn ℝ (Set.Ioi 0) fun (t : ℝ) => Real.log (-n17PsiDeriv a t)

theorem Verification.nelsen17_isCD (θ : ℝ) (hθ : θ ≠ 0) (hθ1 : θ ≤ -1) : (nelsen17 θ hθ).IsCD