← Mathematical handbook

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

Equations

• Verification.gumbelPsiDeriv p t = -p * t ^ (p - 1) * Real.exp (-t ^ p)

theorem Verification.gumbelPsi_deriv {p t : ℝ} (ht : 0 < t) : HasDerivAt (fun (x : ℝ) => Real.exp (-x ^ p)) (gumbelPsiDeriv p t) t

theorem Verification.gumbelPsiDeriv_neg {p t : ℝ} (hp : 0 < p) (ht : 0 < t) : gumbelPsiDeriv p t < 0

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

theorem Verification.gumbel_isCI (θ : ℝ) (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.gumbel θ hθ).IsCI

theorem Verification.gumbel_schur_monotone {θ η : ℝ} (hθ : 1 ≤ θ) (hη : 1 ≤ η) (hθη : θ ≤ η) : (ProbabilityTheory.Copula.gumbel θ hθ).SchurBothLE (ProbabilityTheory.Copula.gumbel η hη)