← Mathematical handbook

noncomputable def Verification.n20LogDeriv (p t : ℝ) : ℝ

Equations

• Verification.n20LogDeriv p t = -Real.log (t + Real.exp 1) - (p + 1) * Real.log (Real.log (t + Real.exp 1))

noncomputable def Verification.n20LogDerivPrime (p t : ℝ) : ℝ

Equations

• Verification.n20LogDerivPrime p t = -1 / (t + Real.exp 1) - (p + 1) / ((t + Real.exp 1) * Real.log (t + Real.exp 1))

theorem Verification.n20LogDeriv_deriv {p t : ℝ} (ht : 0 ≤ t) : HasDerivAt (n20LogDeriv p) (n20LogDerivPrime p t) t

theorem Verification.n20LogDeriv_deriv2 {p t : ℝ} (ht : 0 ≤ t) : HasDerivAt (n20LogDerivPrime p) (1 / (t + Real.exp 1) ^ 2 + (p + 1) * (Real.log (t + Real.exp 1) + 1) / ((t + Real.exp 1) * Real.log (t + Real.exp 1)) ^ 2) t

theorem Verification.n20PsiDeriv_logconvex {p : ℝ} (hp : 0 < p) : ConvexOn ℝ (Set.Ioi 0) fun (t : ℝ) => Real.log (-n20PsiDeriv p t)

theorem Verification.nelsen20_isCI (θ : ℝ) (hθ : 0 ≤ θ) : (nelsen20 θ hθ).IsCI