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 выпукла? (конвексная часть).
LaTeX
$$$\\forall f:\\mathbb{R}\\to\\mathbb{R},\\; \\text{Differentiable}(f) \\Rightarrow \\text{Differentiable}(\\mathrm{deriv}\\,f) \\Rightarrow (\\forall x, (\\mathrm{deriv}^{[2]} f)(x) \\le 0) \\Rightarrow \\text{ConcaveOn}(\\mathbb{R}, \\mathbb{R}, f).$$
Lean4
/-- If `f : 𝕜 → 𝕜` is concave on `s`, then for any point `x ∈ s` the slope of the secant line of `f`
through `x` is antitone on `s \ {x}`. -/
theorem slope_anti (hfc : ConcaveOn 𝕜 s f) (hx : x ∈ s) : AntitoneOn (slope f x) (s \ { x }) :=
by
rw [← neg_neg f, slope_neg_fun]
exact (ConvexOn.slope_mono hfc.neg hx).neg
