Documentation

Mathlib.Analysis.Convex.Deriv

Convexity of functions and derivatives #

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

Main results #

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)) :

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)) :

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 : wSet.Ioo x y, deriv f w 0) :
aSet.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)) :
aSet.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 : wSet.Ioo x y, deriv f w 0) :
aSet.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)) :
aSet.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)) :

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)) :

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 : xinterior D, 0 deriv^[2] f x) :

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 : xinterior D, deriv^[2] f x 0) :

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' : xinterior D, HasDerivWithinAt f (f' x) (interior D) x) (hf'' : xinterior D, HasDerivWithinAt f' (f'' x) (interior D) x) (hf''₀ : xinterior D, 0 f'' x) :

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' : xinterior D, HasDerivWithinAt f (f' x) (interior D) x) (hf'' : xinterior D, HasDerivWithinAt f' (f'' x) (interior D) x) (hf''₀ : xinterior D, f'' x 0) :

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'' : xinterior D, 0 < deriv^[2] f x) :

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'' : xinterior D, deriv^[2] f x < 0) :

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 : xD, 0 deriv^[2] f x) :

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 : xD, deriv^[2] f x 0) :

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'' : xD, 0 < deriv^[2] f x) :

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'' : xD, deriv^[2] f x < 0) :

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).

theorem ConvexOn.slope_mono {𝕜 : Type u_1} [LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜𝕜} {x : 𝕜} (hfc : ConvexOn 𝕜 s f) (hx : x s) :
MonotoneOn (slope f x) (s \ {x})

If f : 𝕜 → 𝕜 is convex on s, then for any point x ∈ s the slope of the secant line of f through x is monotone on s \ {x}.

theorem ConcaveOn.slope_anti {𝕜 : Type u_1} [LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜𝕜} {x : 𝕜} (hfc : ConcaveOn 𝕜 s f) (hx : x s) :
AntitoneOn (slope f x) (s \ {x})

If f : 𝕜 → 𝕜 is concave on s, then for any point x ∈ s the slope of the secant line of f through x is antitone on s \ {x}.

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) :

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) :

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) :

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 : xS, DifferentiableAt f x) :

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 #

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 : xS, DifferentiableAt f x) :

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) :
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) :
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_deriv {S : Set } {f : } (hfc : ConcaveOn S f) (hfd : xS, DifferentiableAt f x) :

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_deriv {S : Set } {f : } (hfc : StrictConcaveOn S f) (hfd : xS, DifferentiableAt f x) :