⊢ ContinuousOn (fun x => sqrt x * log x) (Ioi 1)

x : ℝ
hx : x ∈ Ioi 1
⊢ (deriv^[2]) (fun x => sqrt x * log x) x < 0
⊢ StrictConcaveOn ℝ (Ioi 1) fun x => sqrt x * log x
apply strictConcaveOn_of_deriv2_neg' (convex_Ioi 1) _ fun x hx => ?_
no goals
⊢ ContinuousOn (fun x => sqrt x * log x) (Ioi 1)
exact continuous_sqrt.continuousOn.mul
  (continuousOn_log.mono fun x hx => ne_of_gt (zero_lt_one.trans hx))
x : ℝ
hx : x ∈ Ioi 1
⊢ -log x / (↑4 * sqrt x ^ 3) < 0
x : ℝ
hx : x ∈ Ioi 1
⊢ (deriv^[2]) (fun x => sqrt x * log x) x < 0
rw [deriv2_sqrt_mul_log x]
no goals
x : ℝ
hx : x ∈ Ioi 1
⊢ -log x / (↑4 * sqrt x ^ 3) < 0
exact div_neg_of_neg_of_pos (neg_neg_of_pos (log_pos hx))
  (mul_pos four_pos (pow_pos (sqrt_pos.mpr (zero_lt_one.trans hx)) 3))