← Mathematical handbook

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

Equations

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

theorem Verification.gumbelPsiDeriv_deriv {p t : ℝ} (ht : 0 < t) : HasDerivAt (gumbelPsiDeriv p) (gumbelSecond p t) t

theorem Verification.gumbelSecond_pos {p t : ℝ} (hp : 0 < p) (hp1 : p ≤ 1) (ht : 0 < t) : 0 < gumbelSecond p t

theorem Verification.gumbelSecond_logconvex {p : ℝ} (hp : 0 < p) (hp1 : p ≤ 1) : ConvexOn ℝ (Set.Ioi 0) fun (t : ℝ) => Real.log (gumbelSecond p t)