An integrating factor for a nonlinear differential inequality

theorem NairTenenbaum.hasDerivAt_exp_mul_rpow {L R : ℝ → ℝ} {s L' P a h : ℝ} (hL : HasDerivAt L L' s) (hR : HasDerivAt R (-P) s) (hpos : 0 < L s) : HasDerivAt (fun (x : ℝ) => Real.exp (-a * h * R x) * L x ^ h) (Real.exp (-a * h * R s) * (a * h * P * L s ^ h + h * L s ^ (h - 1) * L')) s

theorem NairTenenbaum.neg_deriv_exp_mul_rpow_le {L R : ℝ → ℝ} {s L' P B a h : ℝ} (hL : HasDerivAt L L' s) (hR : HasDerivAt R (-P) s) (hpos : 0 < L s) (hh : 0 ≤ h) (hineq : -L' ≤ a * P * L s + B * L s ^ (1 - h)) : -deriv (fun (x : ℝ) => Real.exp (-a * h * R x) * L x ^ h) s ≤ h * Real.exp (-a * h * R s) * B