← Mathematical handbook

theorem Verification.joe_logBase_deriv {t : ℝ} (ht : 0 < t) : HasDerivAt (fun (x : ℝ) => Real.log (1 - Real.exp (-x))) (Real.exp (-t) / (1 - Real.exp (-t))) t

theorem Verification.joe_logBase_deriv2 {t : ℝ} (ht : 0 < t) : HasDerivAt (fun (x : ℝ) => Real.exp (-x) / (1 - Real.exp (-x))) (-Real.exp (-t) / (1 - Real.exp (-t)) ^ 2) t

theorem Verification.joe_logBase_concave : ConcaveOn ℝ (Set.Ioi 0) fun (t : ℝ) => Real.log (1 - Real.exp (-t))

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

Equations

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

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

theorem Verification.joePsiDeriv_neg {p t : ℝ} (hp : 0 < p) (ht : 0 < t) : joePsiDeriv p t < 0

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

theorem Verification.joe_isCI (θ : ℝ) (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.joe θ hθ).IsCI