← Mathematical handbook

noncomputable def Verification.bbSecond (p q t : ℝ) : ℝ

Equations

• Verification.bbSecond p q t = p * q * t ^ p / t ^ 2 * (1 + t ^ p) ^ (-q - 2) * ((1 + p * q) * t ^ p + 1 - p)

theorem Verification.bbPsiDeriv_deriv {p q t : ℝ} (ht : 0 < t) : HasDerivAt (bbPsiDeriv p q) (bbSecond p q t) t

theorem Verification.bbSecond_pos {p q t : ℝ} (hp : 0 < p) (hp1 : p ≤ 1) (hq : 0 < q) (ht : 0 < t) : 0 < bbSecond p q t

noncomputable def Verification.bbLogSecondCore (p a t : ℝ) : ℝ

Equations

• Verification.bbLogSecondCore p a t = (p - 2) * Real.log t + Real.log (a * t ^ p + 1 - p)

noncomputable def Verification.bbLogSecondCoreDeriv (p a t : ℝ) : ℝ

Equations

• Verification.bbLogSecondCoreDeriv p a t = (p - 2) / t + p * (a * t ^ p) / (t * (a * t ^ p + 1 - p))

theorem Verification.bbLogSecondCore_deriv {p a t : ℝ} (ht : 0 < t) (hB : a * t ^ p + 1 - p ≠ 0) : HasDerivAt (bbLogSecondCore p a) (bbLogSecondCoreDeriv p a t) t

theorem Verification.bbLogSecondCore_deriv2 {p a t : ℝ} (ht : 0 < t) (hB : a * t ^ p + 1 - p ≠ 0) : HasDerivAt (bbLogSecondCoreDeriv p a) ((2 - p - p * (1 - p) * (a * t ^ p / (a * t ^ p + 1 - p)) - p ^ 2 * (a * t ^ p / (a * t ^ p + 1 - p)) ^ 2) / t ^ 2) t

theorem Verification.bbLogSecondCore_convex {p a : ℝ} (hp : 0 < p) (hp1 : p ≤ 1) (ha : 0 < a) : ConvexOn ℝ (Set.Ioi 0) (bbLogSecondCore p a)

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