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.
• ConvexOn.monotoneOn_deriv: if a function is convex and differentiable, then its derivative is monotone.

Monotonicity of f' implies convexity of f

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.

Convexity of f implies monotonicity of f'

In this section we prove inequalities relating derivatives of convex functions to slopes of secant lines, and deduce that if f is convex then its derivative is monotone (and similarly for strict convexity / strict monotonicity).

Convex functions, derivative at left endpoint of secant

theorem ConvexOn.le_slope_of_hasDerivWithinAt_Ioi {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} {f' : ℝ} (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivWithinAt f f' (Set.Ioi x) x) : f' ≤ slope f x y

If f : ℝ → ℝ is convex on S and right-differentiable at x ∈ S, then the slope of any secant line with left endpoint at x is bounded below by the right derivative of f at x.

theorem ConvexOn.right_deriv_le_slope {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableWithinAt ℝ f (Set.Ioi x) x) : derivWithin f (Set.Ioi x) x ≤ slope f x y

Reformulation of ConvexOn.le_slope_of_hasDerivWithinAt_Ioi using derivWithin.

theorem ConvexOn.le_slope_of_hasDerivWithinAt {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} {f' : ℝ} (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivWithinAt f f' S x) : f' ≤ slope f x y

If f : ℝ → ℝ is convex on S and differentiable within S at x, then the slope of any secant line with left endpoint at x is bounded below by the derivative of f within S at x.

This is fractionally weaker than ConvexOn.le_slope_of_hasDerivWithinAt_Ioi but simpler to apply under a DifferentiableOn S hypothesis.

theorem ConvexOn.derivWithin_le_slope {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableWithinAt ℝ f S x) : derivWithin f S x ≤ slope f x y

Reformulation of ConvexOn.le_slope_of_hasDerivWithinAt using derivWithin.

theorem ConvexOn.le_slope_of_hasDerivAt {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} {f' : ℝ} (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (ha : HasDerivAt f f' x) : f' ≤ slope f x y

If f : ℝ → ℝ is convex on S and differentiable at x ∈ S, then the slope of any secant line with left endpoint at x is bounded below by the derivative of f at x.

theorem ConvexOn.deriv_le_slope {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableAt ℝ f x) : deriv f x ≤ slope f x y

Reformulation of ConvexOn.le_slope_of_hasDerivAt using deriv

Convex functions, derivative at right endpoint of secant

theorem ConvexOn.slope_le_of_hasDerivWithinAt_Iio {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} {f' : ℝ} (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivWithinAt f f' (Set.Iio y) y) : slope f x y ≤ f'

If f : ℝ → ℝ is convex on S and left-differentiable at y ∈ S, then the slope of any secant line with right endpoint at y is bounded above by the left derivative of f at y.

theorem ConvexOn.slope_le_left_deriv {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableWithinAt ℝ f (Set.Iio y) y) : slope f x y ≤ derivWithin f (Set.Iio y) y

Reformulation of ConvexOn.slope_le_of_hasDerivWithinAt_Iio using derivWithin.

theorem ConvexOn.slope_le_of_hasDerivWithinAt {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} {f' : ℝ} (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivWithinAt f f' S y) : slope f x y ≤ f'

If f : ℝ → ℝ is convex on S and differentiable within S at y, then the slope of any secant line with right endpoint at y is bounded above by the derivative of f within S at y.

This is fractionally weaker than ConvexOn.slope_le_of_hasDerivWithinAt_Iio but simpler to apply under a DifferentiableOn S hypothesis.

theorem ConvexOn.slope_le_derivWithin {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableWithinAt ℝ f S y) : slope f x y ≤ derivWithin f S y

Reformulation of ConvexOn.slope_le_of_hasDerivWithinAt using derivWithin.

theorem ConvexOn.slope_le_of_hasDerivAt {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} {f' : ℝ} (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivAt f f' y) : slope f x y ≤ f'

If f : ℝ → ℝ is convex on S and differentiable at y ∈ S, then the slope of any secant line with right endpoint at y is bounded above by the derivative of f at y.

theorem ConvexOn.slope_le_deriv {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableAt ℝ f y) : slope f x y ≤ deriv f y

Reformulation of ConvexOn.slope_le_of_hasDerivAt using deriv.

Convex functions, monotonicity of derivative

theorem ConvexOn.monotoneOn_derivWithin {S : Set ℝ} {f : ℝ → ℝ} (hfc : ConvexOn ℝ S f) (hfd : DifferentiableOn ℝ f S) : MonotoneOn (derivWithin f S) S

If f is convex on S and differentiable on S, then its derivative within S is monotone on S.

theorem ConvexOn.monotoneOn_deriv {S : Set ℝ} {f : ℝ → ℝ} (hfc : ConvexOn ℝ S f) (hfd : ∀ x ∈ S, DifferentiableAt ℝ f x) : MonotoneOn (deriv f) S

If f is convex on S and differentiable at all points of S, then its derivative is monotone on S.

Strict convex functions, derivative at left endpoint of secant

theorem StrictConvexOn.lt_slope_of_hasDerivWithinAt_Ioi {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} {f' : ℝ} (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivWithinAt f f' (Set.Ioi x) x) : f' < slope f x y

If f : ℝ → ℝ is strictly convex on S and right-differentiable at x ∈ S, then the slope of any secant line with left endpoint at x is strictly greater than the right derivative of f at x.

theorem StrictConvexOn.right_deriv_lt_slope {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableWithinAt ℝ f (Set.Ioi x) x) : derivWithin f (Set.Ioi x) x < slope f x y

theorem StrictConvexOn.lt_slope_of_hasDerivWithinAt {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} {f' : ℝ} (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivWithinAt f f' S x) : f' < slope f x y

If f : ℝ → ℝ is strictly convex on S and differentiable within S at x ∈ S, then the slope of any secant line with left endpoint at x is strictly greater than the derivative of f within S at x.

This is fractionally weaker than StrictConvexOn.lt_slope_of_hasDerivWithinAt_Ioi but simpler to apply under a DifferentiableOn S hypothesis.

theorem StrictConvexOn.derivWithin_lt_slope {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableWithinAt ℝ f S x) : derivWithin f S x < slope f x y

theorem StrictConvexOn.lt_slope_of_hasDerivAt {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} {f' : ℝ} (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivAt f f' x) : f' < slope f x y

If f : ℝ → ℝ is strictly convex on S and differentiable at x ∈ S, then the slope of any secant line with left endpoint at x is strictly greater than the derivative of f at x.

theorem StrictConvexOn.deriv_lt_slope {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableAt ℝ f x) : deriv f x < slope f x y

Strict convex functions, derivative at right endpoint of secant

theorem StrictConvexOn.slope_lt_of_hasDerivWithinAt_Iio {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} {f' : ℝ} (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivWithinAt f f' (Set.Iio y) y) : slope f x y < f'

If f : ℝ → ℝ is strictly convex on S and differentiable at y ∈ S, then the slope of any secant line with right endpoint at y is strictly less than the left derivative at y.

theorem StrictConvexOn.slope_lt_left_deriv {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableWithinAt ℝ f (Set.Iio y) y) : slope f x y < derivWithin f (Set.Iio y) y

theorem StrictConvexOn.slope_lt_of_hasDerivWithinAt {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} {f' : ℝ} (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivWithinAt f f' S y) : slope f x y < f'

If f : ℝ → ℝ is strictly convex on S and differentiable within S at y ∈ S, then the slope of any secant line with right endpoint at y is strictly less than the derivative of f within S at y.

This is fractionally weaker than StrictConvexOn.slope_lt_of_hasDerivWithinAt_Iio but simpler to apply under a DifferentiableOn S hypothesis.

theorem StrictConvexOn.slope_lt_derivWithin {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableWithinAt ℝ f S y) : slope f x y < derivWithin f S y

theorem StrictConvexOn.slope_lt_of_hasDerivAt {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} {f' : ℝ} (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivAt f f' y) : slope f x y < f'

If f : ℝ → ℝ is strictly convex on S and differentiable at y ∈ S, then the slope of any secant line with right endpoint at y is strictly less than the derivative of f at y.

theorem StrictConvexOn.slope_lt_deriv {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableAt ℝ f y) : slope f x y < deriv f y

Strict convex functions, strict monotonicity of derivative

theorem StrictConvexOn.strictMonoOn_derivWithin {S : Set ℝ} {f : ℝ → ℝ} (hfc : StrictConvexOn ℝ S f) (hfd : DifferentiableOn ℝ f S) : StrictMonoOn (derivWithin f S) S

If f is convex on S and differentiable on S, then its derivative within S is monotone on S.

theorem StrictConvexOn.strictMonoOn_deriv {S : Set ℝ} {f : ℝ → ℝ} (hfc : StrictConvexOn ℝ S f) (hfd : ∀ x ∈ S, DifferentiableAt ℝ f x) : StrictMonoOn (deriv f) S

If f is convex on S and differentiable at all points of S, then its derivative is monotone on S.

Concave functions, derivative at left endpoint of secant

theorem ConcaveOn.slope_le_of_hasDerivWithinAt_Ioi {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} {f' : ℝ} (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivWithinAt f f' (Set.Ioi x) x) : slope f x y ≤ f'

theorem ConcaveOn.slope_le_right_deriv {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableWithinAt ℝ f (Set.Ioi x) x) : slope f x y ≤ derivWithin f (Set.Ioi x) x

theorem ConcaveOn.slope_le_of_hasDerivWithinAt {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} {f' : ℝ} (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : HasDerivWithinAt f f' S x) : slope f x y ≤ f'

theorem ConcaveOn.slope_le_derivWithin {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableWithinAt ℝ f S x) : slope f x y ≤ derivWithin f S x

theorem ConcaveOn.slope_le_of_hasDerivAt {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} {f' : ℝ} (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivAt f f' x) : slope f x y ≤ f'

theorem ConcaveOn.slope_le_deriv {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableAt ℝ f x) : slope f x y ≤ deriv f x

Concave functions, derivative at right endpoint of secant

theorem ConcaveOn.le_slope_of_hasDerivWithinAt_Iio {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} {f' : ℝ} (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivWithinAt f f' (Set.Iio y) y) : f' ≤ slope f x y

theorem ConcaveOn.left_deriv_le_slope {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableWithinAt ℝ f (Set.Iio y) y) : derivWithin f (Set.Iio y) y ≤ slope f x y

theorem ConcaveOn.le_slope_of_hasDerivWithinAt {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} {f' : ℝ} (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivWithinAt f f' S y) : f' ≤ slope f x y

theorem ConcaveOn.derivWithin_le_slope {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableWithinAt ℝ f S y) : derivWithin f S y ≤ slope f x y

theorem ConcaveOn.le_slope_of_hasDerivAt {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} {f' : ℝ} (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivAt f f' y) : f' ≤ slope f x y

theorem ConcaveOn.deriv_le_slope {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableAt ℝ f y) : deriv f y ≤ slope f x y

Concave functions, anti-monotonicity of derivative

theorem ConcaveOn.antitoneOn_derivWithin {S : Set ℝ} {f : ℝ → ℝ} (hfc : ConcaveOn ℝ S f) (hfd : DifferentiableOn ℝ f S) : AntitoneOn (derivWithin f S) S

theorem ConcaveOn.antitoneOn_deriv {S : Set ℝ} {f : ℝ → ℝ} (hfc : ConcaveOn ℝ S f) (hfd : ∀ x ∈ S, DifferentiableAt ℝ f x) : AntitoneOn (deriv f) S

If f is concave on S and differentiable at all points of S, then its derivative is antitone (monotone decreasing) on S.

Strict concave functions, derivative at left endpoint of secant

theorem StrictConcaveOn.slope_lt_of_hasDerivWithinAt_Ioi {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} {f' : ℝ} (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivWithinAt f f' (Set.Ioi x) x) : slope f x y < f'

theorem StrictConcaveOn.slope_lt_right_deriv {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableWithinAt ℝ f (Set.Ioi x) x) : slope f x y < derivWithin f (Set.Ioi x) x

theorem StrictConcaveOn.slope_lt_of_hasDerivWithinAt {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} {f' : ℝ} (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : HasDerivWithinAt f f' S x) : slope f x y < f'

theorem StrictConcaveOn.slope_lt_derivWithin {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableWithinAt ℝ f S x) : slope f x y < derivWithin f S x

theorem StrictConcaveOn.slope_lt_of_hasDerivAt {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} {f' : ℝ} (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : HasDerivAt f f' x) : slope f x y < f'

theorem StrictConcaveOn.slope_lt_deriv {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableAt ℝ f x) : slope f x y < deriv f x

Strict concave functions, derivative at right endpoint of secant

theorem StrictConcaveOn.lt_slope_of_hasDerivWithinAt_Iio {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} {f' : ℝ} (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivWithinAt f f' (Set.Iio y) y) : f' < slope f x y

theorem StrictConcaveOn.left_deriv_lt_slope {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableWithinAt ℝ f (Set.Iio y) y) : derivWithin f (Set.Iio y) y < slope f x y

theorem StrictConcaveOn.lt_slope_of_hasDerivWithinAt {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} {f' : ℝ} (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivWithinAt f f' S y) : f' < slope f x y

theorem StrictConcaveOn.derivWithin_lt_slope {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableWithinAt ℝ f S y) : derivWithin f S y < slope f x y

theorem StrictConcaveOn.lt_slope_of_hasDerivAt {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} {f' : ℝ} (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivAt f f' y) : f' < slope f x y

theorem StrictConcaveOn.deriv_lt_slope {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} {y : ℝ} (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableAt ℝ f y) : deriv f y < slope f x y

Strict concave functions, anti-monotonicity of derivative

theorem StrictConcaveOn.strictAntiOn_derivWithin {S : Set ℝ} {f : ℝ → ℝ} (hfc : StrictConcaveOn ℝ S f) (hfd : DifferentiableOn ℝ f S) : StrictAntiOn (derivWithin f S) S

theorem StrictConcaveOn.strictAntiOn_deriv {S : Set ℝ} {f : ℝ → ℝ} (hfc : StrictConcaveOn ℝ S f) (hfd : ∀ x ∈ S, DifferentiableAt ℝ f x) : StrictAntiOn (deriv f) S