← Mathematical handbook

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

Equations

• Verification.n19Second θ t = θ * (Real.log (t + Real.exp θ) + 2) / ((t + Real.exp θ) ^ 2 * Real.log (t + Real.exp θ) ^ 3)

theorem Verification.n19Second_pos {θ t : ℝ} (hθ : 0 < θ) (ht : 0 ≤ t) : 0 < n19Second θ t

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

Equations

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

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

Equations

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

theorem Verification.n19LogSecond_deriv {θ t : ℝ} (hθ : 0 < θ) (ht : 0 ≤ t) : HasDerivAt (n19LogSecond θ) (n19LogSecondPrime θ t) t

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

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