FKS2.lemma_10a

@[blueprint  "fks2-lemma-10a"  (title := "FKS2 Lemma 10a")  (statement := /-- If $a>0$, $c>0$ and $b < -c^2/16a$, then $g(a,b,c,x)$ decreases with $x$. -/)  (proof := /-- We apply Lemma \ref{fks2-lemma-10-substep-2}. There are no roots when $b < -\frac{c^2}{16a}$, and the derivative is always negative in this case. -/)  (latexEnv := "lemma")  (discussion := 612)]theorem lemma_10a {a b c : ℝ} (ha : a > 0) (hb : b < -c ^ 2 / (16 * a)) :    StrictAntiOn (g_bound a b c) (Set.Ioi 1) := by  refine strictAntiOn_of_deriv_neg (convex_Ioi 1) (fun x hx ↦ ?_) (fun x hx ↦ ?_)  · have : 0 < x := by linarith [hx.out]    exact (((continuousAt_id.rpow continuousAt_const (Or.inl this.ne')).mul      ((continuousAt_log this.ne').rpow continuousAt_const (Or.inl (log_pos hx.out).ne'))).mul      (continuous_exp.continuousAt.comp (continuousAt_const.mul      (continuous_sqrt.continuousAt.comp (continuousAt_log this.ne'))))).continuousWithinAt  · rw [interior_Ioi] at hx; rw [lemma_10_substep_2 hx]    let t := sqrt (log x)    have : -a * t^2 + c/2 * t + b = -a * (t - c/(4*a))^2 + (b + c^2/(16*a)) := by grind    have : b + c^2/(16*a) < 0 := by grind    linarith [mul_nonneg (le_of_lt ha) (sq_nonneg (t - c/(4*a)))]