← Mathematical handbook

theorem Verification.n20Second_pos {p t : ℝ} (hp : 0 < p) (ht : 0 ≤ t) : 0 < n20Second p t

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

Equations

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

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

Equations

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

theorem Verification.n20LogSecond_deriv {p t : ℝ} (hp : 0 < p) (ht : 0 ≤ t) : HasDerivAt (n20LogSecond p) (n20LogSecondPrime p t) t

theorem Verification.n20LogSecond_deriv2 {p t : ℝ} (hp : 0 < p) (ht : 0 ≤ t) : HasDerivAt (n20LogSecondPrime p) ((2 + (p + 2) * (Real.log (t + Real.exp 1) + 1) / Real.log (t + Real.exp 1) ^ 2 - (Real.log (t + Real.exp 1) + p + 2) / (Real.log (t + Real.exp 1) + p + 1) ^ 2) / (t + Real.exp 1) ^ 2) t

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