← Mathematical handbook

noncomputable def Verification.n20PowerExp (r t : ℝ) : ℝ

Equations

• Verification.n20PowerExp r t = Real.exp (Real.log (t + Real.exp 1) ^ r)

noncomputable def Verification.n20PowerExpPrime (r t : ℝ) : ℝ

Equations

• Verification.n20PowerExpPrime r t = r * Real.log (t + Real.exp 1) ^ (r - 1) * Verification.n20PowerExp r t / (t + Real.exp 1)

theorem Verification.n20_log_ge_one {t : ℝ} (ht : 0 ≤ t) : 1 ≤ Real.log (t + Real.exp 1)

theorem Verification.n20PowerExp_deriv {r t : ℝ} (ht : 0 ≤ t) : HasDerivAt (n20PowerExp r) (n20PowerExpPrime r t) t

theorem Verification.n20PowerExp_deriv2 {r t : ℝ} (ht : 0 ≤ t) : HasDerivAt (n20PowerExpPrime r) (r * Real.log (t + Real.exp 1) ^ (r - 2) * n20PowerExp r t * (r - 1 + Real.log (t + Real.exp 1) * (r * Real.log (t + Real.exp 1) ^ (r - 1) - 1)) / (t + Real.exp 1) ^ 2) t

theorem Verification.n20PowerExp_convex {r : ℝ} (hr : 1 ≤ r) : ConvexOn ℝ (Set.Ici 0) (n20PowerExp r)

noncomputable def Verification.n20Comparison (θ η t : ℝ) : ℝ

Equations

• Verification.n20Comparison θ η t = Verification.n20PowerExp (η / θ) t - Real.exp 1

theorem Verification.n20Comparison_superadd {θ η s t : ℝ} (hθ : 0 < θ) (hθη : θ ≤ η) (hs : 0 ≤ s) (ht : 0 ≤ t) : n20Comparison θ η s + n20Comparison θ η t ≤ n20Comparison θ η (s + t)