Convexity of functions and derivatives

Here we relate convexity of functions ℝ → ℝ to properties of their derivatives.

Main results

• MonotoneOn.convexOn_of_deriv, convexOn_of_deriv2_nonneg : if the derivative of a function is increasing or its second derivative is nonnegative, then the original function is convex.

theorem MonotoneOn.convexOn_of_deriv {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D)) (hf'_mono : MonotoneOn (deriv f) (interior D)) : ConvexOn ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ, is differentiable on its interior, and f' is monotone on the interior, then f is convex on D.

theorem AntitoneOn.concaveOn_of_deriv {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D)) (h_anti : AntitoneOn (deriv f) (interior D)) : ConcaveOn ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ, is differentiable on its interior, and f' is antitone on the interior, then f is concave on D.

theorem StrictMonoOn.exists_slope_lt_deriv_aux {x : ℝ} {y : ℝ} {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc x y)) (hxy : x < y) (hf'_mono : StrictMonoOn (deriv f) (Set.Ioo x y)) (h : ∀ w ∈ Set.Ioo x y, deriv f w ≠ 0) : ∃ a ∈ Set.Ioo x y, (f y - f x) / (y - x) < deriv f a

theorem StrictMonoOn.exists_slope_lt_deriv {x : ℝ} {y : ℝ} {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc x y)) (hxy : x < y) (hf'_mono : StrictMonoOn (deriv f) (Set.Ioo x y)) : ∃ a ∈ Set.Ioo x y, (f y - f x) / (y - x) < deriv f a

theorem StrictMonoOn.exists_deriv_lt_slope_aux {x : ℝ} {y : ℝ} {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc x y)) (hxy : x < y) (hf'_mono : StrictMonoOn (deriv f) (Set.Ioo x y)) (h : ∀ w ∈ Set.Ioo x y, deriv f w ≠ 0) : ∃ a ∈ Set.Ioo x y, deriv f a < (f y - f x) / (y - x)

theorem StrictMonoOn.exists_deriv_lt_slope {x : ℝ} {y : ℝ} {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc x y)) (hxy : x < y) (hf'_mono : StrictMonoOn (deriv f) (Set.Ioo x y)) : ∃ a ∈ Set.Ioo x y, deriv f a < (f y - f x) / (y - x)

theorem StrictMonoOn.strictConvexOn_of_deriv {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : 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'.

theorem StrictAntiOn.strictConcaveOn_of_deriv {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (h_anti : StrictAntiOn (deriv f) (interior D)) : StrictConcaveOn ℝ D f

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

theorem Monotone.convexOn_univ_of_deriv {f : ℝ → ℝ} (hf : Differentiable ℝ f) (hf'_mono : Monotone (deriv f)) : ConvexOn ℝ Set.univ f

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

theorem Antitone.concaveOn_univ_of_deriv {f : ℝ → ℝ} (hf : Differentiable ℝ f) (hf'_anti : Antitone (deriv f)) : ConcaveOn ℝ Set.univ f

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

theorem StrictMono.strictConvexOn_univ_of_deriv {f : ℝ → ℝ} (hf : Continuous f) (hf'_mono : StrictMono (deriv f)) : StrictConvexOn ℝ Set.univ f

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

theorem StrictAnti.strictConcaveOn_univ_of_deriv {f : ℝ → ℝ} (hf : Continuous f) (hf'_anti : StrictAnti (deriv f)) : StrictConcaveOn ℝ Set.univ f

If a function f is continuous and f' is strictly antitone on ℝ then f is strictly concave. Note that we don't require differentiability, since it is guaranteed at all but at most one point by the strict antitonicity of f'.

theorem convexOn_of_deriv2_nonneg {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D)) (hf'' : DifferentiableOn ℝ (deriv f) (interior D)) (hf''_nonneg : ∀ x ∈ interior D, 0 ≤ deriv^[2] f x) : ConvexOn ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ, is twice differentiable on its interior, and f'' is nonnegative on the interior, then f is convex on D.

theorem concaveOn_of_deriv2_nonpos {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D)) (hf'' : DifferentiableOn ℝ (deriv f) (interior D)) (hf''_nonpos : ∀ x ∈ interior D, deriv^[2] f x ≤ 0) : ConcaveOn ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ, is twice differentiable on its interior, and f'' is nonpositive on the interior, then f is concave on D.

theorem convexOn_of_hasDerivWithinAt2_nonneg {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} {f' : ℝ → ℝ} {f'' : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x) (hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x) (hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x) : ConvexOn ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ, is twice differentiable on its interior, and f'' is nonnegative on the interior, then f is convex on D.

theorem concaveOn_of_hasDerivWithinAt2_nonpos {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} {f' : ℝ → ℝ} {f'' : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x) (hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x) (hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0) : ConcaveOn ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ, is twice differentiable on its interior, and f'' is nonpositive on the interior, then f is concave on D.

theorem strictConvexOn_of_deriv2_pos {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf'' : ∀ x ∈ interior D, 0 < deriv^[2] f x) : StrictConvexOn ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ and f'' is strictly positive on the interior, then f is strictly convex on D. Note that we don't require twice differentiability explicitly as it is already implied by the second derivative being strictly positive, except at at most one point.

theorem strictConcaveOn_of_deriv2_neg {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf'' : ∀ x ∈ interior D, deriv^[2] f x < 0) : StrictConcaveOn ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ and f'' is strictly negative on the interior, then f is strictly concave on D. Note that we don't require twice differentiability explicitly as it already implied by the second derivative being strictly negative, except at at most one point.

theorem convexOn_of_deriv2_nonneg' {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf' : DifferentiableOn ℝ f D) (hf'' : DifferentiableOn ℝ (deriv f) D) (hf''_nonneg : ∀ x ∈ D, 0 ≤ deriv^[2] f x) : ConvexOn ℝ D f

If a function f is twice differentiable on an open convex set D ⊆ ℝ and f'' is nonnegative on D, then f is convex on D.

theorem concaveOn_of_deriv2_nonpos' {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf' : DifferentiableOn ℝ f D) (hf'' : DifferentiableOn ℝ (deriv f) D) (hf''_nonpos : ∀ x ∈ D, deriv^[2] f x ≤ 0) : ConcaveOn ℝ D f

If a function f is twice differentiable on an open convex set D ⊆ ℝ and f'' is nonpositive on D, then f is concave on D.

theorem strictConvexOn_of_deriv2_pos' {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf'' : ∀ x ∈ D, 0 < deriv^[2] f x) : StrictConvexOn ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ and f'' is strictly positive on D, then f is strictly convex on D. Note that we don't require twice differentiability explicitly as it is already implied by the second derivative being strictly positive, except at at most one point.

theorem strictConcaveOn_of_deriv2_neg' {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf'' : ∀ x ∈ D, deriv^[2] f x < 0) : StrictConcaveOn ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ and f'' is strictly negative on D, then f is strictly concave on D. Note that we don't require twice differentiability explicitly as it is already implied by the second derivative being strictly negative, except at at most one point.

theorem convexOn_univ_of_deriv2_nonneg {f : ℝ → ℝ} (hf' : Differentiable ℝ f) (hf'' : Differentiable ℝ (deriv f)) (hf''_nonneg : ∀ (x : ℝ), 0 ≤ deriv^[2] f x) : ConvexOn ℝ Set.univ f

If a function f is twice differentiable on ℝ, and f'' is nonnegative on ℝ, then f is convex on ℝ.

theorem concaveOn_univ_of_deriv2_nonpos {f : ℝ → ℝ} (hf' : Differentiable ℝ f) (hf'' : Differentiable ℝ (deriv f)) (hf''_nonpos : ∀ (x : ℝ), deriv^[2] f x ≤ 0) : ConcaveOn ℝ Set.univ f

If a function f is twice differentiable on ℝ, and f'' is nonpositive on ℝ, then f is concave on ℝ.

theorem strictConvexOn_univ_of_deriv2_pos {f : ℝ → ℝ} (hf : Continuous f) (hf'' : ∀ (x : ℝ), 0 < deriv^[2] f x) : StrictConvexOn ℝ Set.univ f

If a function f is continuous on ℝ, and f'' is strictly positive on ℝ, then f is strictly convex on ℝ. Note that we don't require twice differentiability explicitly as it is already implied by the second derivative being strictly positive, except at at most one point.

theorem strictConcaveOn_univ_of_deriv2_neg {f : ℝ → ℝ} (hf : Continuous f) (hf'' : ∀ (x : ℝ), deriv^[2] f x < 0) : StrictConcaveOn ℝ Set.univ f

If a function f is continuous on ℝ, and f'' is strictly negative on ℝ, then f is strictly concave on ℝ. Note that we don't require twice differentiability explicitly as it is already implied by the second derivative being strictly negative, except at at most one point.