convexOn_univ_of_deriv — Mathlib

English

If f is differentiable and f' is monotone on ℝ, then f is convex on ℝ.

Русский

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

LaTeX

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

Lean4

/-- If a function `f` is differentiable and `f'` is monotone on `ℝ` then `f` is convex. -/
theorem convexOn_univ_of_deriv {f : ℝ → ℝ} (hf : Differentiable ℝ f) (hf'_mono : Monotone (deriv f)) :
    ConvexOn ℝ univ f :=
  (hf'_mono.monotoneOn _).convexOn_of_deriv convex_univ hf.continuous.continuousOn hf.differentiableOn

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