FKS2.lemma_10_substep_2

@[blueprint  "fks2-lemma-10-substep-2"  (title := "FKS2 Sublemma 10-2")  (statement := /-- $\frac{d}{dx} g(a, b, c, x) $ is negative when $-au^2 + \frac{c}{2}u + b < 0$, where $u = \sqrt{\log(x)}$.  -/)  (proof := /-- Clear from previous sublemma. -/)  (latexEnv := "sublemma")  (discussion := 611)]theorem lemma_10_substep_2 {a b c x : ℝ} (hx : x > 1) :  deriv (g_bound a b c) x < 0 ↔    -a * (sqrt (log x)) ^ 2 + (c / 2) * sqrt (log x) + b < 0 := by  have hlogx := log_pos hx  rw [lemma_10_substep hx, sq_sqrt hlogx.le]  have hpos : 0 < x ^ (-a - 1) * (log x) ^ (b - 1) * exp (c * sqrt (log x)) := by positivity  rw [show ∀ y, y * x ^ (-a - 1) * (log x) ^ (b - 1) * exp (c * sqrt (log x)) =      y * (x ^ (-a - 1) * (log x) ^ (b - 1) * exp (c * sqrt (log x))) from fun _ ↦ by ring]  rw [mul_neg_iff]  constructor <;> intro h  · rcases h with ⟨-, hc⟩ | ⟨h, -⟩ <;> linarith  · exact Or.inr ⟨by linarith, hpos⟩