Theorems · Theorem · real analysis

StrictMonoOn.strictConvexOn_of_deriv

∀ {D : Set ℝ}, Convex ℝ D → ∀ {f : ℝ → ℝ}, ContinuousOn f D → StrictMonoOn (deriv f) (interior D) → StrictConvexOn ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ, and f' is strictly monotone on the interior, then f is strictly convex on D. Note that we don't require differentiability, since it is guaranteed at all but at most one point by the strict monotonicity of f'.

Defined in

Mathlib.Analysis.Convex.Deriv

Cited by

4 results in Mathlib

Foundations

Depth 191 from the axioms · uses propext, Classical.choice, Quot.sound