← Mathematical handbook

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

Equations

• Verification.powerIncrementRatio r t = ((1 + t) ^ r - 1) / t ^ r

theorem Verification.powerIncrementRatio_deriv {r t : ℝ} (ht : 0 < t) : HasDerivAt (powerIncrementRatio r) (r * (1 + t - (1 + t) ^ r) / (t * (1 + t) * t ^ r)) t

theorem Verification.powerIncrementRatio_monotone {r : ℝ} (hr : 0 ≤ r) (hr1 : r ≤ 1) : MonotoneOn (powerIncrementRatio r) (Set.Ioi 0)

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

Equations

• Verification.n14Comparison θ η t = ((1 + t ^ θ⁻¹) ^ (θ / η) - 1) ^ η

theorem Verification.n14Comparison_ratio {θ η t : ℝ} (hθ : 0 < θ) (hη : 0 < η) (ht : 0 < t) : n14Comparison θ η t / t = powerIncrementRatio (θ / η) (t ^ θ⁻¹) ^ η

theorem Verification.n14Comparison_ratio_monotone {θ η : ℝ} (hθ : 0 < θ) (hη : 0 < η) (hθη : θ ≤ η) : MonotoneOn (fun (t : ℝ) => n14Comparison θ η t / t) (Set.Ioi 0)

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