← Mathematical handbook

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

Equations

• Verification.n19LogDeriv θ t = -Real.log (t + Real.exp θ) - 2 * Real.log (Real.log (t + Real.exp θ))

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

Equations

• Verification.n19LogDerivPrime θ t = -1 / (t + Real.exp θ) - 2 / ((t + Real.exp θ) * Real.log (t + Real.exp θ))

theorem Verification.n19LogDeriv_deriv {θ t : ℝ} (hθ : 0 < θ) (ht : 0 ≤ t) : HasDerivAt (n19LogDeriv θ) (n19LogDerivPrime θ t) t

theorem Verification.n19LogDeriv_deriv2 {θ t : ℝ} (hθ : 0 < θ) (ht : 0 ≤ t) : HasDerivAt (n19LogDerivPrime θ) (1 / (t + Real.exp θ) ^ 2 + 2 * (Real.log (t + Real.exp θ) + 1) / ((t + Real.exp θ) * Real.log (t + Real.exp θ)) ^ 2) t

theorem Verification.n19PsiDeriv_logconvex {θ : ℝ} (hθ : 0 < θ) : ConvexOn ℝ (Set.Ioi 0) fun (t : ℝ) => Real.log (-n19PsiDeriv θ t)

theorem Verification.nelsen19_isCI (θ : ℝ) (hθ : 0 ≤ θ) : (nelsen19 θ hθ).IsCI