concaveOn_univ_of_deriv — Mathlib

English

If f is differentiable and f' is antitone on ℝ, then f is concave on ℝ.

Русский

Если f дифференцируема и f' антитонона на ℝ, то f конкавна на ℝ.

LaTeX

$$$$\\text{Differentiable}(f) \\land \\text{Antitone}(\\operatorname{deriv} f) \\Rightarrow \\operatorname{ConcaveOn}_{\\mathbb{R}} \\mathbb{R} f.$$$$

Lean4

/-- If a function `f` is differentiable and `f'` is antitone on `ℝ` then `f` is concave. -/
theorem concaveOn_univ_of_deriv {f : ℝ → ℝ} (hf : Differentiable ℝ f) (hf'_anti : Antitone (deriv f)) :
    ConcaveOn ℝ univ f :=
  (hf'_anti.antitoneOn _).concaveOn_of_deriv convex_univ hf.continuous.continuousOn hf.differentiableOn

Похожие утверждения