# 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` #

source
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`.

source
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`.

source
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
source
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
source
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)
source
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)
source
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'`.

source
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'`.

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

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

source
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'`.

source
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'`.

source
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`.

source
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`.

source
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`.

source
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`.

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

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

source
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`.

source
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`.

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

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

source
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 `ℝ`.

source
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 `ℝ`.

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

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

source
theorem ConvexOn.slope_mono {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {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}`.

source
theorem ConvexOn.monotoneOn_slope_gt {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} {x : 𝕜} (hfc : ConvexOn 𝕜 s f) (hxs : x ∈ s) :
MonotoneOn (slope f x) {y : 𝕜 | y ∈ s ∧ x < y}
source
theorem ConvexOn.monotoneOn_slope_lt {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} {x : 𝕜} (hfc : ConvexOn 𝕜 s f) (hxs : x ∈ s) :
MonotoneOn (slope f x) {y : 𝕜 | y ∈ s ∧ y < x}
source
theorem ConcaveOn.slope_anti {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {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}`.

source
theorem ConcaveOn.antitoneOn_slope_gt {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} {x : 𝕜} (hfc : ConcaveOn 𝕜 s f) (hxs : x ∈ s) :
AntitoneOn (slope f x) {y : 𝕜 | y ∈ s ∧ x < y}
source
theorem ConcaveOn.antitoneOn_slope_lt {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} {x : 𝕜} (hfc : ConcaveOn 𝕜 s f) (hxs : x ∈ s) :
AntitoneOn (slope f x) {y : 𝕜 | y ∈ s ∧ y < x}
source
theorem bddBelow_slope_lt_of_mem_interior {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} {x : 𝕜} [TopologicalSpace 𝕜] [OrderTopology 𝕜] (hfc : ConvexOn 𝕜 s f) (hxs : x ∈ interior s) :
BddBelow (slope f x '' {y : 𝕜 | y ∈ s ∧ x < y})
source
theorem bddAbove_slope_gt_of_mem_interior {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} {x : 𝕜} [TopologicalSpace 𝕜] [OrderTopology 𝕜] (hfc : ConvexOn 𝕜 s f) (hxs : x ∈ interior s) :
BddAbove (slope f x '' {y : 𝕜 | y ∈ s ∧ y < x})

### Left and right derivative of a convex function in the interior of the set #

source
theorem ConvexOn.hasDerivWithinAt_sInf_slope_of_mem_interior {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hfc : ConvexOn ℝ S f) (hxs : x ∈ interior S) :
HasDerivWithinAt f (sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y})) (Set.Ioi x) x
source
theorem ConvexOn.hasDerivWithinAt_sSup_slope_of_mem_interior {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hfc : ConvexOn ℝ S f) (hxs : x ∈ interior S) :
HasDerivWithinAt f (sSup (slope f x '' {y : ℝ | y ∈ S ∧ y < x})) (Set.Iio x) x
source
theorem ConvexOn.differentiableWithinAt_Ioi_of_mem_interior {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hfc : ConvexOn ℝ S f) (hxs : x ∈ interior S) :
DifferentiableWithinAt ℝ f (Set.Ioi x) x
source
theorem ConvexOn.differentiableWithinAt_Iio_of_mem_interior {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hfc : ConvexOn ℝ S f) (hxs : x ∈ interior S) :
DifferentiableWithinAt ℝ f (Set.Iio x) x
source
theorem ConvexOn.hasDerivWithinAt_rightDeriv_of_mem_interior {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hfc : ConvexOn ℝ S f) (hxs : x ∈ interior S) :
HasDerivWithinAt f (derivWithin f (Set.Ioi x) x) (Set.Ioi x) x
source
theorem ConvexOn.hasDerivWithinAt_leftDeriv_of_mem_interior {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hfc : ConvexOn ℝ S f) (hxs : x ∈ interior S) :
HasDerivWithinAt f (derivWithin f (Set.Iio x) x) (Set.Iio x) x
source
theorem ConvexOn.rightDeriv_eq_sInf_slope_of_mem_interior {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hfc : ConvexOn ℝ S f) (hxs : x ∈ interior S) :
derivWithin f (Set.Ioi x) x = sInf (slope f x '' {y : ℝ | y ∈ S ∧ x < y})
source
theorem ConvexOn.leftDeriv_eq_sSup_slope_of_mem_interior {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hfc : ConvexOn ℝ S f) (hxs : x ∈ interior S) :
derivWithin f (Set.Iio x) x = sSup (slope f x '' {y : ℝ | y ∈ S ∧ y < x})
source
theorem ConvexOn.monotoneOn_rightDeriv {S : Set ℝ} {f : ℝ → ℝ} (hfc : ConvexOn ℝ S f) :
MonotoneOn (fun (x : ℝ) => derivWithin f (Set.Ioi x) x) (interior S)
source
theorem ConvexOn.monotoneOn_leftDeriv {S : Set ℝ} {f : ℝ → ℝ} (hfc : ConvexOn ℝ S f) :
MonotoneOn (fun (x : ℝ) => derivWithin f (Set.Iio x) x) (interior S)
source
theorem ConvexOn.leftDeriv_le_rightDeriv_of_mem_interior {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hfc : ConvexOn ℝ S f) (hxs : x ∈ interior S) :
derivWithin f (Set.Iio x) x ≤ derivWithin f (Set.Ioi x) x

### Convex functions, derivative at left endpoint of secant #

source
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`.

source
theorem ConvexOn.rightDeriv_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`.

source
theorem ConvexOn.rightDeriv_le_slope_of_mem_interior {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hfc : ConvexOn ℝ S f) {y : ℝ} (hxs : x ∈ interior S) (hys : y ∈ S) (hxy : x < y) :
derivWithin f (Set.Ioi x) x ≤ slope f x y
source
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.

source
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`.

source
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`.

source
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 #

source
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`.

source
theorem ConvexOn.slope_le_leftDeriv {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`.

source
theorem ConvexOn.slope_le_leftDeriv_of_mem_interior {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ} (hfc : ConvexOn ℝ S f) (hys : x ∈ S) (hxs : y ∈ interior S) (hxy : x < y) :
slope f x y ≤ derivWithin f (Set.Iio y) y
source
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.

source
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`.

source
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`.

source
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 #

source
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`.

source
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`.

source
theorem ConvexOn.isMinOn_of_leftDeriv_nonpos_of_rightDeriv_nonneg {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) (hf_ld : derivWithin f (Set.Iio x) x ≤ 0) (hf_rd : 0 ≤ derivWithin f (Set.Ioi x) x) :
IsMinOn f S x
source
theorem ConvexOn.isMinOn_of_rightDeriv_eq_zero {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) (hf_rd : derivWithin f (Set.Ioi x) x = 0) :
IsMinOn f S x
source
theorem ConvexOn.isMinOn_of_leftDeriv_eq_zero {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) (hf_ld : derivWithin f (Set.Iio x) x = 0) :
IsMinOn f S x

### Strict convex functions, derivative at left endpoint of secant #

source
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`.

source
theorem StrictConvexOn.rightDeriv_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
source
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.

source
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
source
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`.

source
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 #

source
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`.

source
theorem StrictConvexOn.slope_lt_leftDeriv {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
source
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.

source
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
source
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`.

source
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 #

source
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`.

source
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 #

source
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'
source
theorem ConcaveOn.slope_le_rightDeriv {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
source
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'
source
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
source
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'
source
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 #

source
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
source
theorem ConcaveOn.leftDeriv_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
source
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
source
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
source
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
source
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 #

source
theorem ConcaveOn.antitoneOn_derivWithin {S : Set ℝ} {f : ℝ → ℝ} (hfc : ConcaveOn ℝ S f) (hfd : DifferentiableOn ℝ f S) :
AntitoneOn (derivWithin f S) S
source
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 #

source
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'
source
theorem StrictConcaveOn.slope_lt_rightDeriv {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
source
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'
source
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
source
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'
source
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 #

source
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
source
theorem StrictConcaveOn.leftDeriv_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
source
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
source
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
source
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
source
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 #

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