English
If f is twice differentiable on R and f'' ≤ 0 on R, then f is concave on R.
Русский
Если f дважды дифференцируема на всей ℝ и f''(x) ≤ 0 для всех x, то f выпукла на ℝ? (кон.sec note: concave).
LaTeX
$$$\\forall f:\\mathbb{R}\\to\\mathbb{R},\\; \\text{Differentiable}(f, \\mathbb{R}) \\Rightarrow \\text{Differentiable}(\\mathrm{deriv}\,f, \\mathbb{R}) \\Rightarrow (\\forall x, (\\mathrm{deriv}^{[2]} f)(x) \\le 0) \\Rightarrow \\text{ConcaveOn}(\\mathbb{R}, \\mathbb{R}, f).$$
Lean4
/-- If a function `f` is twice differentiable on `ℝ`, and `f''` is nonpositive on `ℝ`,
then `f` is concave on `ℝ`. -/
theorem concaveOn_univ_of_deriv2_nonpos {f : ℝ → ℝ} (hf' : Differentiable ℝ f) (hf'' : Differentiable ℝ (deriv f))
(hf''_nonpos : ∀ x, deriv^[2] f x ≤ 0) : ConcaveOn ℝ univ f :=
concaveOn_of_deriv2_nonpos' convex_univ hf'.differentiableOn hf''.differentiableOn fun x _ => hf''_nonpos x
