← Mathematical handbook

noncomputable def Verification.n17R (a t : ℝ) : ℝ

Equations

• Verification.n17R a t = a⁻¹ * Verification.n17A a * Real.exp (-t)

noncomputable def Verification.n17LogSecond (a t : ℝ) : ℝ

Equations

• Verification.n17LogSecond a t = -t + (a⁻¹ - 2) * Real.log (Verification.n17Base a t) + Real.log (1 + Verification.n17R a t)

noncomputable def Verification.n17LogSecondPrime (a t : ℝ) : ℝ

Equations

• Verification.n17LogSecondPrime a t = -1 - (a⁻¹ - 2) * Verification.n17A a * Real.exp (-t) / Verification.n17Base a t - Verification.n17R a t / (1 + Verification.n17R a t)

theorem Verification.n17R_pos {a : ℝ} (ha : a ≠ 0) (t : ℝ) : 0 < n17R a t

theorem Verification.n17R_deriv (a t : ℝ) : HasDerivAt (n17R a) (-n17R a t) t

theorem Verification.n17LogSecond_deriv {a t : ℝ} (ha : a ≠ 0) (ht : 0 ≤ t) : HasDerivAt (n17LogSecond a) (n17LogSecondPrime a t) t

theorem Verification.n17LogSecond_deriv2 {a t : ℝ} (ha : a ≠ 0) (ht : 0 ≤ t) : HasDerivAt (n17LogSecondPrime a) (n17R a t * (1 - a) * (2 + 2 * n17R a t + (1 - a) * n17R a t ^ 2) / (n17Base a t ^ 2 * (1 + n17R a t) ^ 2)) t

theorem Verification.n17Second_logconvex {a : ℝ} (ha : a ≠ 0) (ha1 : a ≤ 1) : ConvexOn ℝ (Set.Ioi 0) fun (t : ℝ) => Real.log (n17Second a t)