← Mathematical handbook

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

Equations

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

theorem Verification.joePsiDeriv_deriv {p t : ℝ} (ht : 0 < t) : HasDerivAt (joePsiDeriv p) (joeSecond p t) t

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

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

Equations

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

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

Equations

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

theorem Verification.joe_scaledLog_deriv {p t : ℝ} (hB : 1 - p * Real.exp (-t) ≠ 0) : HasDerivAt (fun (x : ℝ) => Real.log (1 - p * Real.exp (-x))) (p * Real.exp (-t) / (1 - p * Real.exp (-t))) t

theorem Verification.joe_scaledLog_deriv2 {p t : ℝ} (hB : 1 - p * Real.exp (-t) ≠ 0) : HasDerivAt (fun (x : ℝ) => p * Real.exp (-x) / (1 - p * Real.exp (-x))) (-p * Real.exp (-t) / (1 - p * Real.exp (-t)) ^ 2) t

theorem Verification.joeLogSecond_deriv {p t : ℝ} (ht : 0 < t) (hB : 1 - p * Real.exp (-t) ≠ 0) : HasDerivAt (joeLogSecond p) (joeLogSecondDeriv p t) t

theorem Verification.joeLogSecond_deriv2 {p t : ℝ} (ht : 0 < t) (hB : 1 - p * Real.exp (-t) ≠ 0) : HasDerivAt (joeLogSecondDeriv p) ((2 - p) * Real.exp (-t) / (1 - Real.exp (-t)) ^ 2 - p * Real.exp (-t) / (1 - p * Real.exp (-t)) ^ 2) t

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