← Mathematical handbook

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

Equations

• Verification.n13Second p t = p * (1 + t) ^ p / (1 + t) ^ 2 * (p * (1 + t) ^ p - p + 1) * Verification.n13Psi p t

noncomputable def Verification.n13LogSecondCore (p x : ℝ) : ℝ

Equations

• Verification.n13LogSecondCore p x = Real.log p + (p - 2) * Real.log x + Real.log (p * x ^ p + 1 - p) + 1 - x ^ p

noncomputable def Verification.n13LogSecondDeriv (p x : ℝ) : ℝ

Equations

• Verification.n13LogSecondDeriv p x = (p - 2) / x + p ^ 2 * x ^ p / (x * (p * x ^ p + 1 - p)) - p * x ^ p / x

theorem Verification.n13LogSecondCore_deriv {p x : ℝ} (hx : 0 < x) (hB : p * x ^ p + 1 - p ≠ 0) : HasDerivAt (n13LogSecondCore p) (n13LogSecondDeriv p x) x

theorem Verification.n13LogSecondCore_deriv2 {p x : ℝ} (hx : 0 < x) (hB : p * x ^ p + 1 - p ≠ 0) : HasDerivAt (n13LogSecondDeriv p) ((2 - p - p * (1 - p) * (p * x ^ p / (p * x ^ p + 1 - p)) - p ^ 2 * (p * x ^ p / (p * x ^ p + 1 - p)) ^ 2 + (1 - p) * p * x ^ p) / x ^ 2) x

theorem Verification.n13LogSecondCore_deriv2_nonneg {p x : ℝ} (hp : 0 < p) (hp1 : p ≤ 1) (hx : 0 < x) : 0 ≤ (2 - p - p * (1 - p) * (p * x ^ p / (p * x ^ p + 1 - p)) - p ^ 2 * (p * x ^ p / (p * x ^ p + 1 - p)) ^ 2 + (1 - p) * p * x ^ p) / x ^ 2

theorem Verification.n13_logSecond_eq {p t : ℝ} (hp : 0 < p) (hp1 : p ≤ 1) (ht : 0 ≤ t) : Real.log (n13Second p t) = n13LogSecondCore p (1 + t)

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

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