x : ℝ
hx : x ∈ interior (Icc 0 π)
⊢ (deriv^[2]) sin x < 0
⊢ StrictConcaveOn ℝ (Icc 0 π) sin
apply strictConcaveOn_of_deriv2_neg (convex_Icc _ _) continuousOn_sin fun x hx => ?_
x : ℝ
hx : x ∈ Ioo 0 π
⊢ (deriv^[2]) sin x < 0
x : ℝ
hx : x ∈ interior (Icc 0 π)
⊢ (deriv^[2]) sin x < 0
rw [interior_Icc] at hx
no goals
x : ℝ
hx : x ∈ Ioo 0 π
⊢ (deriv^[2]) sin x < 0
simp [sin_pos_of_mem_Ioo hx]