# mathlibdocumentation

analysis.calculus.mean_value

# The mean value inequality and equalities #

In this file we prove the following facts:

• convex.norm_image_sub_le_of_norm_deriv_le : if f is differentiable on a convex set s and the norm of its derivative is bounded by C, then f is Lipschitz continuous on s with constant C; also a variant in which what is bounded by C is the norm of the difference of the derivative from a fixed linear map. This lemma and its versions are formulated using is_R_or_C, so they work both for real and complex derivatives.

• image_le_of*, image_norm_le_of_* : several similar lemmas deducing f x ≤ B x or ∥f x∥ ≤ B x from upper estimates on f' or ∥f'∥, respectively. These lemmas differ by their assumptions:

• of_liminf_* lemmas assume that limit inferior of some ratio is less than B' x;
• of_deriv_right_*, of_norm_deriv_right_* lemmas assume that the right derivative or its norm is less than B' x;
• of_*_lt_* lemmas assume a strict inequality whenever f x = B x or ∥f x∥ = B x;
• of_*_le_* lemmas assume a non-strict inequality everywhere on [a, b);
• name of a lemma ends with ' if (1) it assumes that B is continuous on [a, b] and has a right derivative at every point of [a, b), and (2) the lemma has a counterpart assuming that B is differentiable everywhere on ℝ
• norm_image_sub_le_*_segment : if derivative of f on [a, b] is bounded above by a constant C, then ∥f x - f a∥ ≤ C * ∥x - a∥; several versions deal with right derivative and derivative within [a, b] (has_deriv_within_at or deriv_within).

• convex.is_const_of_fderiv_within_eq_zero : if a function has derivative 0 on a convex set s, then it is a constant on s.

• exists_ratio_has_deriv_at_eq_ratio_slope and exists_ratio_deriv_eq_ratio_slope : Cauchy's Mean Value Theorem.

• exists_has_deriv_at_eq_slope and exists_deriv_eq_slope : Lagrange's Mean Value Theorem.

• domain_mvt : Lagrange's Mean Value Theorem, applied to a segment in a convex domain.

• convex.image_sub_lt_mul_sub_of_deriv_lt, convex.mul_sub_lt_image_sub_of_lt_deriv, convex.image_sub_le_mul_sub_of_deriv_le, convex.mul_sub_le_image_sub_of_le_deriv, if ∀ x, C (</≤/>/≥) (f' x), then C * (y - x) (</≤/>/≥) (f y - f x) whenever x < y.

• convex.monotone_on_of_deriv_nonneg, convex.antitone_on_of_deriv_nonpos, convex.strict_mono_of_deriv_pos, convex.strict_anti_of_deriv_neg : if the derivative of a function is non-negative/non-positive/positive/negative, then the function is monotone/antitone/strictly monotone/strictly monotonically decreasing.

• convex_on_of_deriv_monotone_on, convex_on_of_deriv2_nonneg : if the derivative of a function is increasing or its second derivative is nonnegative, then the original function is convex.

• strict_fderiv_of_cont_diff : a C^1 function over the reals is strictly differentiable. (This is a corollary of the mean value inequality.)

### One-dimensional fencing inequalities #

theorem image_le_of_liminf_slope_right_lt_deriv_boundary' {f f' : } {a b : } (hf : (set.Icc a b)) (hf' : ∀ (x : ), x b∀ (r : ), f' x < r(∃ᶠ (z : ) in (set.Ioi x), x z < r)) {B B' : } (ha : f a B a) (hB : (set.Icc a b)) (hB' : ∀ (x : ), x b (B' x) (set.Ici x) x) (bound : ∀ (x : ), x bf x = B xf' x < B' x) ⦃x :  :
x bf x B x

General fencing theorem for continuous functions with an estimate on the derivative. Let f and B be continuous functions on [a, b] such that

• f a ≤ B a;
• B has right derivative B' at every point of [a, b);
• for each x ∈ [a, b) the right-side limit inferior of (f z - f x) / (z - x) is bounded above by a function f';
• we have f' x < B' x whenever f x = B x.

Then f x ≤ B x everywhere on [a, b].

theorem image_le_of_liminf_slope_right_lt_deriv_boundary {f f' : } {a b : } (hf : (set.Icc a b)) (hf' : ∀ (x : ), x b∀ (r : ), f' x < r(∃ᶠ (z : ) in (set.Ioi x), x z < r)) {B B' : } (ha : f a B a) (hB : ∀ (x : ), (B' x) x) (bound : ∀ (x : ), x bf x = B xf' x < B' x) ⦃x :  :
x bf x B x

General fencing theorem for continuous functions with an estimate on the derivative. Let f and B be continuous functions on [a, b] such that

• f a ≤ B a;
• B has derivative B' everywhere on ℝ;
• for each x ∈ [a, b) the right-side limit inferior of (f z - f x) / (z - x) is bounded above by a function f';
• we have f' x < B' x whenever f x = B x.

Then f x ≤ B x everywhere on [a, b].

theorem image_le_of_liminf_slope_right_le_deriv_boundary {f : } {a b : } (hf : (set.Icc a b)) {B B' : } (ha : f a B a) (hB : (set.Icc a b)) (hB' : ∀ (x : ), x b (B' x) (set.Ici x) x) (bound : ∀ (x : ), x b∀ (r : ), B' x < r(∃ᶠ (z : ) in (set.Ioi x), x z < r)) ⦃x :  :
x bf x B x

General fencing theorem for continuous functions with an estimate on the derivative. Let f and B be continuous functions on [a, b] such that

• f a ≤ B a;
• B has right derivative B' at every point of [a, b);
• for each x ∈ [a, b) the right-side limit inferior of (f z - f x) / (z - x) is bounded above by B'.

Then f x ≤ B x everywhere on [a, b].

theorem image_le_of_deriv_right_lt_deriv_boundary' {f f' : } {a b : } (hf : (set.Icc a b)) (hf' : ∀ (x : ), x b (f' x) (set.Ici x) x) {B B' : } (ha : f a B a) (hB : (set.Icc a b)) (hB' : ∀ (x : ), x b (B' x) (set.Ici x) x) (bound : ∀ (x : ), x bf x = B xf' x < B' x) ⦃x :  :
x bf x B x

General fencing theorem for continuous functions with an estimate on the derivative. Let f and B be continuous functions on [a, b] such that

• f a ≤ B a;
• B has right derivative B' at every point of [a, b);
• f has right derivative f' at every point of [a, b);
• we have f' x < B' x whenever f x = B x.

Then f x ≤ B x everywhere on [a, b].

theorem image_le_of_deriv_right_lt_deriv_boundary {f f' : } {a b : } (hf : (set.Icc a b)) (hf' : ∀ (x : ), x b (f' x) (set.Ici x) x) {B B' : } (ha : f a B a) (hB : ∀ (x : ), (B' x) x) (bound : ∀ (x : ), x bf x = B xf' x < B' x) ⦃x :  :
x bf x B x

General fencing theorem for continuous functions with an estimate on the derivative. Let f and B be continuous functions on [a, b] such that

• f a ≤ B a;
• B has derivative B' everywhere on ℝ;
• f has right derivative f' at every point of [a, b);
• we have f' x < B' x whenever f x = B x.

Then f x ≤ B x everywhere on [a, b].

theorem image_le_of_deriv_right_le_deriv_boundary {f f' : } {a b : } (hf : (set.Icc a b)) (hf' : ∀ (x : ), x b (f' x) (set.Ici x) x) {B B' : } (ha : f a B a) (hB : (set.Icc a b)) (hB' : ∀ (x : ), x b (B' x) (set.Ici x) x) (bound : ∀ (x : ), x bf' x B' x) ⦃x :  :
x bf x B x

General fencing theorem for continuous functions with an estimate on the derivative. Let f and B be continuous functions on [a, b] such that

• f a ≤ B a;
• B has derivative B' everywhere on ℝ;
• f has right derivative f' at every point of [a, b);
• we have f' x ≤ B' x on [a, b).

Then f x ≤ B x everywhere on [a, b].

### Vector-valued functions f : ℝ → E#

theorem image_norm_le_of_liminf_right_slope_norm_lt_deriv_boundary {a b : } {E : Type u_1} {f : → E} {f' : } (hf : (set.Icc a b)) (hf' : ∀ (x : ), x b∀ (r : ), f' x < r(∃ᶠ (z : ) in (set.Ioi x), slope x z < r)) {B B' : } (ha : f a B a) (hB : (set.Icc a b)) (hB' : ∀ (x : ), x b (B' x) (set.Ici x) x) (bound : ∀ (x : ), x bf x = B xf' x < B' x) ⦃x :  :
x bf x B x

General fencing theorem for continuous functions with an estimate on the derivative. Let f and B be continuous functions on [a, b] such that

• ∥f a∥ ≤ B a;
• B has right derivative at every point of [a, b);
• for each x ∈ [a, b) the right-side limit inferior of (∥f z∥ - ∥f x∥) / (z - x) is bounded above by a function f';
• we have f' x < B' x whenever ∥f x∥ = B x.

Then ∥f x∥ ≤ B x everywhere on [a, b].

theorem image_norm_le_of_norm_deriv_right_lt_deriv_boundary' {E : Type u_1} [ E] {f : → E} {a b : } {f' : → E} (hf : (set.Icc a b)) (hf' : ∀ (x : ), x b (f' x) (set.Ici x) x) {B B' : } (ha : f a B a) (hB : (set.Icc a b)) (hB' : ∀ (x : ), x b (B' x) (set.Ici x) x) (bound : ∀ (x : ), x bf x = B xf' x < B' x) ⦃x :  :
x bf x B x

General fencing theorem for continuous functions with an estimate on the norm of the derivative. Let f and B be continuous functions on [a, b] such that

• ∥f a∥ ≤ B a;
• f and B have right derivatives f' and B' respectively at every point of [a, b);
• the norm of f' is strictly less than B' whenever ∥f x∥ = B x.

Then ∥f x∥ ≤ B x everywhere on [a, b]. We use one-sided derivatives in the assumptions to make this theorem work for piecewise differentiable functions.

theorem image_norm_le_of_norm_deriv_right_lt_deriv_boundary {E : Type u_1} [ E] {f : → E} {a b : } {f' : → E} (hf : (set.Icc a b)) (hf' : ∀ (x : ), x b (f' x) (set.Ici x) x) {B B' : } (ha : f a B a) (hB : ∀ (x : ), (B' x) x) (bound : ∀ (x : ), x bf x = B xf' x < B' x) ⦃x :  :
x bf x B x

General fencing theorem for continuous functions with an estimate on the norm of the derivative. Let f and B be continuous functions on [a, b] such that

• ∥f a∥ ≤ B a;
• f has right derivative f' at every point of [a, b);
• B has derivative B' everywhere on ℝ;
• the norm of f' is strictly less than B' whenever ∥f x∥ = B x.

Then ∥f x∥ ≤ B x everywhere on [a, b]. We use one-sided derivatives in the assumptions to make this theorem work for piecewise differentiable functions.

theorem image_norm_le_of_norm_deriv_right_le_deriv_boundary' {E : Type u_1} [ E] {f : → E} {a b : } {f' : → E} (hf : (set.Icc a b)) (hf' : ∀ (x : ), x b (f' x) (set.Ici x) x) {B B' : } (ha : f a B a) (hB : (set.Icc a b)) (hB' : ∀ (x : ), x b (B' x) (set.Ici x) x) (bound : ∀ (x : ), x bf' x B' x) ⦃x :  :
x bf x B x

General fencing theorem for continuous functions with an estimate on the norm of the derivative. Let f and B be continuous functions on [a, b] such that

• ∥f a∥ ≤ B a;
• f and B have right derivatives f' and B' respectively at every point of [a, b);
• we have ∥f' x∥ ≤ B x everywhere on [a, b).

Then ∥f x∥ ≤ B x everywhere on [a, b]. We use one-sided derivatives in the assumptions to make this theorem work for piecewise differentiable functions.

theorem image_norm_le_of_norm_deriv_right_le_deriv_boundary {E : Type u_1} [ E] {f : → E} {a b : } {f' : → E} (hf : (set.Icc a b)) (hf' : ∀ (x : ), x b (f' x) (set.Ici x) x) {B B' : } (ha : f a B a) (hB : ∀ (x : ), (B' x) x) (bound : ∀ (x : ), x bf' x B' x) ⦃x :  :
x bf x B x

General fencing theorem for continuous functions with an estimate on the norm of the derivative. Let f and B be continuous functions on [a, b] such that

• ∥f a∥ ≤ B a;
• f has right derivative f' at every point of [a, b);
• B has derivative B' everywhere on ℝ;
• we have ∥f' x∥ ≤ B x everywhere on [a, b).

Then ∥f x∥ ≤ B x everywhere on [a, b]. We use one-sided derivatives in the assumptions to make this theorem work for piecewise differentiable functions.

theorem norm_image_sub_le_of_norm_deriv_right_le_segment {E : Type u_1} [ E] {f : → E} {a b : } {f' : → E} {C : } (hf : (set.Icc a b)) (hf' : ∀ (x : ), x b (f' x) (set.Ici x) x) (bound : ∀ (x : ), x bf' x C) (x : ) (H : x b) :
f x - f a C * (x - a)

A function on [a, b] with the norm of the right derivative bounded by C satisfies ∥f x - f a∥ ≤ C * (x - a).

theorem norm_image_sub_le_of_norm_deriv_le_segment' {E : Type u_1} [ E] {f : → E} {a b : } {f' : → E} {C : } (hf : ∀ (x : ), x b (f' x) (set.Icc a b) x) (bound : ∀ (x : ), x bf' x C) (x : ) (H : x b) :
f x - f a C * (x - a)

A function on [a, b] with the norm of the derivative within [a, b] bounded by C satisfies ∥f x - f a∥ ≤ C * (x - a), has_deriv_within_at version.

theorem norm_image_sub_le_of_norm_deriv_le_segment {E : Type u_1} [ E] {f : → E} {a b C : } (hf : (set.Icc a b)) (bound : ∀ (x : ), x b (set.Icc a b) x C) (x : ) (H : x b) :
f x - f a C * (x - a)

A function on [a, b] with the norm of the derivative within [a, b] bounded by C satisfies ∥f x - f a∥ ≤ C * (x - a), deriv_within version.

theorem norm_image_sub_le_of_norm_deriv_le_segment_01' {E : Type u_1} [ E] {f f' : → E} {C : } (hf : ∀ (x : ), x 1 (f' x) (set.Icc 0 1) x) (bound : ∀ (x : ), x 1f' x C) :
f 1 - f 0 C

A function on [0, 1] with the norm of the derivative within [0, 1] bounded by C satisfies ∥f 1 - f 0∥ ≤ C, has_deriv_within_at version.

theorem norm_image_sub_le_of_norm_deriv_le_segment_01 {E : Type u_1} [ E] {f : → E} {C : } (hf : (set.Icc 0 1)) (bound : ∀ (x : ), x 1 (set.Icc 0 1) x C) :
f 1 - f 0 C

A function on [0, 1] with the norm of the derivative within [0, 1] bounded by C satisfies ∥f 1 - f 0∥ ≤ C, deriv_within version.

theorem constant_of_has_deriv_right_zero {E : Type u_1} [ E] {f : → E} {a b : } (hcont : (set.Icc a b)) (hderiv : ∀ (x : ), x b (set.Ici x) x) (x : ) (H : x b) :
f x = f a
theorem constant_of_deriv_within_zero {E : Type u_1} [ E] {f : → E} {a b : } (hdiff : (set.Icc a b)) (hderiv : ∀ (x : ), x b (set.Icc a b) x = 0) (x : ) (H : x b) :
f x = f a
theorem eq_of_has_deriv_right_eq {E : Type u_1} [ E] {f : → E} {a b : } {f' g : → E} (derivf : ∀ (x : ), x b (f' x) (set.Ici x) x) (derivg : ∀ (x : ), x b (f' x) (set.Ici x) x) (fcont : (set.Icc a b)) (gcont : (set.Icc a b)) (hi : f a = g a) (y : ) (H : y b) :
f y = g y

If two continuous functions on [a, b] have the same right derivative and are equal at a, then they are equal everywhere on [a, b].

theorem eq_of_deriv_within_eq {E : Type u_1} [ E] {f : → E} {a b : } {g : → E} (fdiff : (set.Icc a b)) (gdiff : (set.Icc a b)) (hderiv : set.eq_on (set.Icc a b)) (set.Icc a b)) (set.Ico a b)) (hi : f a = g a) (y : ) (H : y b) :
f y = g y

If two differentiable functions on [a, b] have the same derivative within [a, b] everywhere on [a, b) and are equal at a, then they are equal everywhere on [a, b].

### Vector-valued functions f : E → G#

Theorems in this section work both for real and complex differentiable functions. We use assumptions [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 G] to achieve this result. For the domain E we also assume [normed_space ℝ E] to have a notion of a convex set.

theorem convex.norm_image_sub_le_of_norm_has_fderiv_within_le {E : Type u_1} [ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [ E] [ G] {f : E → G} {C : } {s : set E} {x y : E} {f' : E → (E →L[𝕜] G)} (hf : ∀ (x : E), x s (f' x) s x) (bound : ∀ (x : E), x sf' x C) (hs : s) (xs : x s) (ys : y s) :
f y - f x C * y - x

The mean value theorem on a convex set: if the derivative of a function is bounded by C, then the function is C-Lipschitz. Version with has_fderiv_within.

theorem convex.lipschitz_on_with_of_nnnorm_has_fderiv_within_le {E : Type u_1} [ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [ E] [ G] {f : E → G} {s : set E} {f' : E → (E →L[𝕜] G)} {C : nnreal} (hf : ∀ (x : E), x s (f' x) s x) (bound : ∀ (x : E), x sf' x∥₊ C) (hs : s) :
s

The mean value theorem on a convex set: if the derivative of a function is bounded by C on s, then the function is C-Lipschitz on s. Version with has_fderiv_within and lipschitz_on_with.

theorem convex.exists_nhds_within_lipschitz_on_with_of_has_fderiv_within_at_of_nnnorm_lt {E : Type u_1} [ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [ E] [ G] {s : set E} {x : E} {f' : E → (E →L[𝕜] G)} (hs : s) {f : E → G} (hder : ∀ᶠ (y : E) in s, (f' y) s y) (hcont : x) (K : nnreal) (hK : f' x∥₊ < K) :
∃ (t : set E) (H : t s), t

Let s be a convex set in a real normed vector space E, let f : E → G be a function differentiable within s in a neighborhood of x : E with derivative f'. Suppose that f' is continuous within s at x. Then for any number K : ℝ≥0 larger than ∥f' x∥₊, f is K-Lipschitz on some neighborhood of x within s. See also convex.exists_nhds_within_lipschitz_on_with_of_has_fderiv_within_at for a version that claims existence of K instead of an explicit estimate.

theorem convex.exists_nhds_within_lipschitz_on_with_of_has_fderiv_within_at {E : Type u_1} [ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [ E] [ G] {s : set E} {x : E} {f' : E → (E →L[𝕜] G)} (hs : s) {f : E → G} (hder : ∀ᶠ (y : E) in s, (f' y) s y) (hcont : x) :
∃ (K : nnreal) (t : set E) (H : t s), t

Let s be a convex set in a real normed vector space E, let f : E → G be a function differentiable within s in a neighborhood of x : E with derivative f'. Suppose that f' is continuous within s at x. Then for any number K : ℝ≥0 larger than ∥f' x∥₊, f is Lipschitz on some neighborhood of x within s. See also convex.exists_nhds_within_lipschitz_on_with_of_has_fderiv_within_at_of_nnnorm_lt for a version with an explicit estimate on the Lipschitz constant.

theorem convex.norm_image_sub_le_of_norm_fderiv_within_le {E : Type u_1} [ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [ E] [ G] {f : E → G} {C : } {s : set E} {x y : E} (hf : s) (bound : ∀ (x : E), x s s x C) (hs : s) (xs : x s) (ys : y s) :
f y - f x C * y - x

The mean value theorem on a convex set: if the derivative of a function within this set is bounded by C, then the function is C-Lipschitz. Version with fderiv_within.

theorem convex.lipschitz_on_with_of_nnnorm_fderiv_within_le {E : Type u_1} [ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [ E] [ G] {f : E → G} {s : set E} {C : nnreal} (hf : s) (bound : ∀ (x : E), x s s x∥₊ C) (hs : s) :
s

The mean value theorem on a convex set: if the derivative of a function is bounded by C on s, then the function is C-Lipschitz on s. Version with fderiv_within and lipschitz_on_with.

theorem convex.norm_image_sub_le_of_norm_fderiv_le {E : Type u_1} [ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [ E] [ G] {f : E → G} {C : } {s : set E} {x y : E} (hf : ∀ (x : E), x s x) (bound : ∀ (x : E), x s f x C) (hs : s) (xs : x s) (ys : y s) :
f y - f x C * y - x

The mean value theorem on a convex set: if the derivative of a function is bounded by C, then the function is C-Lipschitz. Version with fderiv.

theorem convex.lipschitz_on_with_of_nnnorm_fderiv_le {E : Type u_1} [ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [ E] [ G] {f : E → G} {s : set E} {C : nnreal} (hf : ∀ (x : E), x s x) (bound : ∀ (x : E), x s f x∥₊ C) (hs : s) :
s

The mean value theorem on a convex set: if the derivative of a function is bounded by C on s, then the function is C-Lipschitz on s. Version with fderiv and lipschitz_on_with.

theorem convex.norm_image_sub_le_of_norm_has_fderiv_within_le' {E : Type u_1} [ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [ E] [ G] {f : E → G} {C : } {s : set E} {x y : E} {f' : E → (E →L[𝕜] G)} {φ : E →L[𝕜] G} (hf : ∀ (x : E), x s (f' x) s x) (bound : ∀ (x : E), x sf' x - φ C) (hs : s) (xs : x s) (ys : y s) :
f y - f x - φ (y - x) C * y - x

Variant of the mean value inequality on a convex set, using a bound on the difference between the derivative and a fixed linear map, rather than a bound on the derivative itself. Version with has_fderiv_within.

theorem convex.norm_image_sub_le_of_norm_fderiv_within_le' {E : Type u_1} [ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [ E] [ G] {f : E → G} {C : } {s : set E} {x y : E} {φ : E →L[𝕜] G} (hf : s) (bound : ∀ (x : E), x s s x - φ C) (hs : s) (xs : x s) (ys : y s) :
f y - f x - φ (y - x) C * y - x

Variant of the mean value inequality on a convex set. Version with fderiv_within.

theorem convex.norm_image_sub_le_of_norm_fderiv_le' {E : Type u_1} [ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [ E] [ G] {f : E → G} {C : } {s : set E} {x y : E} {φ : E →L[𝕜] G} (hf : ∀ (x : E), x s x) (bound : ∀ (x : E), x s f x - φ C) (hs : s) (xs : x s) (ys : y s) :
f y - f x - φ (y - x) C * y - x

Variant of the mean value inequality on a convex set. Version with fderiv.

theorem convex.is_const_of_fderiv_within_eq_zero {E : Type u_1} [ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [ E] [ G] {f : E → G} {s : set E} {x y : E} (hs : s) (hf : s) (hf' : ∀ (x : E), x s s x = 0) (hx : x s) (hy : y s) :
f x = f y

If a function has zero Fréchet derivative at every point of a convex set, then it is a constant on this set.

theorem is_const_of_fderiv_eq_zero {E : Type u_1} [ E] {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [ E] [ G] {f : E → G} (hf : f) (hf' : ∀ (x : E), f x = 0) (x y : E) :
f x = f y
theorem convex.norm_image_sub_le_of_norm_has_deriv_within_le {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [ G] {f f' : 𝕜 → G} {s : set 𝕜} {x y : 𝕜} {C : } (hf : ∀ (x : 𝕜), x s (f' x) s x) (bound : ∀ (x : 𝕜), x sf' x C) (hs : s) (xs : x s) (ys : y s) :
f y - f x C * y - x

The mean value theorem on a convex set in dimension 1: if the derivative of a function is bounded by C, then the function is C-Lipschitz. Version with has_deriv_within.

theorem convex.lipschitz_on_with_of_nnnorm_has_deriv_within_le {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [ G] {f f' : 𝕜 → G} {s : set 𝕜} {C : nnreal} (hs : s) (hf : ∀ (x : 𝕜), x s (f' x) s x) (bound : ∀ (x : 𝕜), x sf' x∥₊ C) :
s

The mean value theorem on a convex set in dimension 1: if the derivative of a function is bounded by C on s, then the function is C-Lipschitz on s. Version with has_deriv_within and lipschitz_on_with.

theorem convex.norm_image_sub_le_of_norm_deriv_within_le {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [ G] {f : 𝕜 → G} {s : set 𝕜} {x y : 𝕜} {C : } (hf : s) (bound : ∀ (x : 𝕜), x s s x C) (hs : s) (xs : x s) (ys : y s) :
f y - f x C * y - x

The mean value theorem on a convex set in dimension 1: if the derivative of a function within this set is bounded by C, then the function is C-Lipschitz. Version with deriv_within

theorem convex.lipschitz_on_with_of_nnnorm_deriv_within_le {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [ G] {f : 𝕜 → G} {s : set 𝕜} {C : nnreal} (hs : s) (hf : s) (bound : ∀ (x : 𝕜), x s s x∥₊ C) :
s

The mean value theorem on a convex set in dimension 1: if the derivative of a function is bounded by C on s, then the function is C-Lipschitz on s. Version with deriv_within and lipschitz_on_with.

theorem convex.norm_image_sub_le_of_norm_deriv_le {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [ G] {f : 𝕜 → G} {s : set 𝕜} {x y : 𝕜} {C : } (hf : ∀ (x : 𝕜), x s x) (bound : ∀ (x : 𝕜), x s x C) (hs : s) (xs : x s) (ys : y s) :
f y - f x C * y - x

The mean value theorem on a convex set in dimension 1: if the derivative of a function is bounded by C, then the function is C-Lipschitz. Version with deriv.

theorem convex.lipschitz_on_with_of_nnnorm_deriv_le {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [ G] {f : 𝕜 → G} {s : set 𝕜} {C : nnreal} (hf : ∀ (x : 𝕜), x s x) (bound : ∀ (x : 𝕜), x s x∥₊ C) (hs : s) :
s

The mean value theorem on a convex set in dimension 1: if the derivative of a function is bounded by C on s, then the function is C-Lipschitz on s. Version with deriv and lipschitz_on_with.

theorem lipschitz_with_of_nnnorm_deriv_le {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [ G] {f : 𝕜 → G} {C : nnreal} (hf : f) (bound : ∀ (x : 𝕜), x∥₊ C) :

The mean value theorem set in dimension 1: if the derivative of a function is bounded by C, then the function is C-Lipschitz. Version with deriv and lipschitz_with.

theorem is_const_of_deriv_eq_zero {𝕜 : Type u_3} {G : Type u_4} [is_R_or_C 𝕜] [ G] {f : 𝕜 → G} (hf : f) (hf' : ∀ (x : 𝕜), x = 0) (x y : 𝕜) :
f x = f y

If f : 𝕜 → G, 𝕜 = R or 𝕜 = ℂ, is differentiable everywhere and its derivative equal zero, then it is a constant function.

### Functions [a, b] → ℝ. #

theorem exists_ratio_has_deriv_at_eq_ratio_slope (f f' : ) {a b : } (hab : a < b) (hfc : (set.Icc a b)) (hff' : ∀ (x : ), x b (f' x) x) (g g' : ) (hgc : (set.Icc a b)) (hgg' : ∀ (x : ), x b (g' x) x) :
∃ (c : ) (H : c b), (g b - g a) * f' c = (f b - f a) * g' c

Cauchy's Mean Value Theorem, has_deriv_at version.

theorem exists_ratio_has_deriv_at_eq_ratio_slope' (f f' : ) {a b : } (hab : a < b) (g g' : ) {lfa lga lfb lgb : } (hff' : ∀ (x : ), x b (f' x) x) (hgg' : ∀ (x : ), x b (g' x) x) (hfa : (set.Ioi a)) (nhds lfa)) (hga : (set.Ioi a)) (nhds lga)) (hfb : (set.Iio b)) (nhds lfb)) (hgb : (set.Iio b)) (nhds lgb)) :
∃ (c : ) (H : c b), (lgb - lga) * f' c = (lfb - lfa) * g' c

Cauchy's Mean Value Theorem, extended has_deriv_at version.

theorem exists_has_deriv_at_eq_slope (f f' : ) {a b : } (hab : a < b) (hfc : (set.Icc a b)) (hff' : ∀ (x : ), x b (f' x) x) :
∃ (c : ) (H : c b), f' c = (f b - f a) / (b - a)

Lagrange's Mean Value Theorem, has_deriv_at version

theorem exists_ratio_deriv_eq_ratio_slope (f : ) {a b : } (hab : a < b) (hfc : (set.Icc a b)) (hfd : (set.Ioo a b)) (g : ) (hgc : (set.Icc a b)) (hgd : (set.Ioo a b)) :
∃ (c : ) (H : c b), (g b - g a) * c = (f b - f a) * c

Cauchy's Mean Value Theorem, deriv version.

theorem exists_ratio_deriv_eq_ratio_slope' (f : ) {a b : } (hab : a < b) (g : ) {lfa lga lfb lgb : } (hdf : (set.Ioo a b)) (hdg : (set.Ioo a b)) (hfa : (set.Ioi a)) (nhds lfa)) (hga : (set.Ioi a)) (nhds lga)) (hfb : (set.Iio b)) (nhds lfb)) (hgb : (set.Iio b)) (nhds lgb)) :
∃ (c : ) (H : c b), (lgb - lga) * c = (lfb - lfa) * c

Cauchy's Mean Value Theorem, extended deriv version.

theorem exists_deriv_eq_slope (f : ) {a b : } (hab : a < b) (hfc : (set.Icc a b)) (hfd : (set.Ioo a b)) :
∃ (c : ) (H : c b), c = (f b - f a) / (b - a)

Lagrange's Mean Value Theorem, deriv version.

theorem convex.mul_sub_lt_image_sub_of_lt_deriv {D : set } (hD : D) {f : } (hf : D) (hf' : (interior D)) {C : } (hf'_gt : ∀ (x : ), x C < x) (x : ) (H : x D) (y : ) (H_1 : y D) :
x < yC * (y - x) < f y - f x

Let f be a function continuous on a convex (or, equivalently, connected) subset D of the real line. If f is differentiable on the interior of D and C < f', then f grows faster than C * x on D, i.e., C * (y - x) < f y - f x whenever x, y ∈ D, x < y.

theorem mul_sub_lt_image_sub_of_lt_deriv {f : } (hf : f) {C : } (hf'_gt : ∀ (x : ), C < x) ⦃x y : (hxy : x < y) :
C * (y - x) < f y - f x

Let f : ℝ → ℝ be a differentiable function. If C < f', then f grows faster than C * x, i.e., C * (y - x) < f y - f x whenever x < y.

theorem convex.mul_sub_le_image_sub_of_le_deriv {D : set } (hD : D) {f : } (hf : D) (hf' : (interior D)) {C : } (hf'_ge : ∀ (x : ), x C x) (x : ) (H : x D) (y : ) (H_1 : y D) :
x yC * (y - x) f y - f x

Let f be a function continuous on a convex (or, equivalently, connected) subset D of the real line. If f is differentiable on the interior of D and C ≤ f', then f grows at least as fast as C * x on D, i.e., C * (y - x) ≤ f y - f x whenever x, y ∈ D, x ≤ y.

theorem mul_sub_le_image_sub_of_le_deriv {f : } (hf : f) {C : } (hf'_ge : ∀ (x : ), C x) ⦃x y : (hxy : x y) :
C * (y - x) f y - f x

Let f : ℝ → ℝ be a differentiable function. If C ≤ f', then f grows at least as fast as C * x, i.e., C * (y - x) ≤ f y - f x whenever x ≤ y.

theorem convex.image_sub_lt_mul_sub_of_deriv_lt {D : set } (hD : D) {f : } (hf : D) (hf' : (interior D)) {C : } (lt_hf' : ∀ (x : ), x x < C) (x : ) (H : x D) (y : ) (H_1 : y D) :
x < yf y - f x < C * (y - x)

Let f be a function continuous on a convex (or, equivalently, connected) subset D of the real line. If f is differentiable on the interior of D and f' < C, then f grows slower than C * x on D, i.e., f y - f x < C * (y - x) whenever x, y ∈ D, x < y.

theorem image_sub_lt_mul_sub_of_deriv_lt {f : } (hf : f) {C : } (lt_hf' : ∀ (x : ), x < C) ⦃x y : (hxy : x < y) :
f y - f x < C * (y - x)

Let f : ℝ → ℝ be a differentiable function. If f' < C, then f grows slower than C * x on D, i.e., f y - f x < C * (y - x) whenever x < y.

theorem convex.image_sub_le_mul_sub_of_deriv_le {D : set } (hD : D) {f : } (hf : D) (hf' : (interior D)) {C : } (le_hf' : ∀ (x : ), x x C) (x : ) (H : x D) (y : ) (H_1 : y D) :
x yf y - f x C * (y - x)

Let f be a function continuous on a convex (or, equivalently, connected) subset D of the real line. If f is differentiable on the interior of D and f' ≤ C, then f grows at most as fast as C * x on D, i.e., f y - f x ≤ C * (y - x) whenever x, y ∈ D, x ≤ y.

theorem image_sub_le_mul_sub_of_deriv_le {f : } (hf : f) {C : } (le_hf' : ∀ (x : ), x C) ⦃x y : (hxy : x y) :
f y - f x C * (y - x)

Let f : ℝ → ℝ be a differentiable function. If f' ≤ C, then f grows at most as fast as C * x, i.e., f y - f x ≤ C * (y - x) whenever x ≤ y.

theorem convex.strict_mono_on_of_deriv_pos {D : set } (hD : D) {f : } (hf : D) (hf' : ∀ (x : ), x 0 < x) :

Let f be a function continuous on a convex (or, equivalently, connected) subset D of the real line. If f is differentiable on the interior of D and f' is positive, then f is a strictly monotone function on D. Note that we don't require differentiability explicitly as it already implied by the derivative being strictly positive.

theorem strict_mono_of_deriv_pos {f : } (hf' : ∀ (x : ), 0 < x) :

Let f : ℝ → ℝ be a differentiable function. If f' is positive, then f is a strictly monotone function. Note that we don't require differentiability explicitly as it already implied by the derivative being strictly positive.

theorem convex.monotone_on_of_deriv_nonneg {D : set } (hD : D) {f : } (hf : D) (hf' : (interior D)) (hf'_nonneg : ∀ (x : ), x 0 x) :
D

Let f be a function continuous on a convex (or, equivalently, connected) subset D of the real line. If f is differentiable on the interior of D and f' is nonnegative, then f is a monotone function on D.

theorem monotone_of_deriv_nonneg {f : } (hf : f) (hf' : ∀ (x : ), 0 x) :

Let f : ℝ → ℝ be a differentiable function. If f' is nonnegative, then f is a monotone function.

theorem convex.strict_anti_on_of_deriv_neg {D : set } (hD : D) {f : } (hf : D) (hf' : ∀ (x : ), x x < 0) :

Let f be a function continuous on a convex (or, equivalently, connected) subset D of the real line. If f is differentiable on the interior of D and f' is negative, then f is a strictly antitone function on D.

theorem strict_anti_of_deriv_neg {f : } (hf' : ∀ (x : ), x < 0) :

Let f : ℝ → ℝ be a differentiable function. If f' is negative, then f is a strictly antitone function. Note that we don't require differentiability explicitly as it already implied by the derivative being strictly negative.

theorem convex.antitone_on_of_deriv_nonpos {D : set } (hD : D) {f : } (hf : D) (hf' : (interior D)) (hf'_nonpos : ∀ (x : ), x x 0) :
D

Let f be a function continuous on a convex (or, equivalently, connected) subset D of the real line. If f is differentiable on the interior of D and f' is nonpositive, then f is an antitone function on D.

theorem antitone_of_deriv_nonpos {f : } (hf : f) (hf' : ∀ (x : ), x 0) :

Let f : ℝ → ℝ be a differentiable function. If f' is nonpositive, then f is an antitone function.

theorem monotone_on.convex_on_of_deriv {D : set } (hD : D) {f : } (hf : D) (hf' : (interior D)) (hf'_mono : monotone_on (deriv f) (interior 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 antitone_on.concave_on_of_deriv {D : set } (hD : D) {f : } (hf : D) (hf' : (interior D)) (h_anti : antitone_on (deriv f) (interior 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 strict_mono_on.exists_slope_lt_deriv_aux {x y : } {f : } (hf : (set.Icc x y)) (hxy : x < y) (hf'_mono : (set.Ioo x y)) (h : ∀ (w : ), w y w 0) :
∃ (a : ) (H : a y), (f y - f x) / (y - x) < a
theorem strict_mono_on.exists_slope_lt_deriv {x y : } {f : } (hf : (set.Icc x y)) (hxy : x < y) (hf'_mono : (set.Ioo x y)) :
∃ (a : ) (H : a y), (f y - f x) / (y - x) < a
theorem strict_mono_on.exists_deriv_lt_slope_aux {x y : } {f : } (hf : (set.Icc x y)) (hxy : x < y) (hf'_mono : (set.Ioo x y)) (h : ∀ (w : ), w y w 0) :
∃ (a : ) (H : a y), a < (f y - f x) / (y - x)
theorem strict_mono_on.exists_deriv_lt_slope {x y : } {f : } (hf : (set.Icc x y)) (hxy : x < y) (hf'_mono : (set.Ioo x y)) :
∃ (a : ) (H : a y), a < (f y - f x) / (y - x)
theorem strict_mono_on.strict_convex_on_of_deriv {D : set } (hD : D) {f : } (hf : D) (hf' : (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 strict_anti_on.strict_concave_on_of_deriv {D : set } (hD : D) {f : } (hf : D) (h_anti : (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.convex_on_univ_of_deriv {f : } (hf : f) (hf'_mono : monotone (deriv f)) :

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

theorem antitone.concave_on_univ_of_deriv {f : } (hf : f) (hf'_anti : antitone (deriv f)) :

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

theorem strict_mono.strict_convex_on_univ_of_deriv {f : } (hf : continuous f) (hf'_mono : strict_mono (deriv 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 strict_anti.strict_concave_on_univ_of_deriv {f : } (hf : continuous f) (hf'_anti : strict_anti (deriv 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 convex_on_of_deriv2_nonneg {D : set } (hD : D) {f : } (hf : D) (hf' : (interior D)) (hf'' : (interior D)) (hf''_nonneg : ∀ (x : ), x 0 deriv^[2] f x) :
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 concave_on_of_deriv2_nonpos {D : set } (hD : D) {f : } (hf : D) (hf' : (interior D)) (hf'' : (interior D)) (hf''_nonpos : ∀ (x : ), x deriv^[2] f x 0) :
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 strict_convex_on_of_deriv2_pos {D : set } (hD : D) {f : } (hf : D) (hf'' : ∀ (x : ), x 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 strict_concave_on_of_deriv2_neg {D : set } (hD : D) {f : } (hf : D) (hf'' : ∀ (x : ), x 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 convex_on_of_deriv2_nonneg' {D : set } (hD : D) {f : } (hf' : D) (hf'' : D) (hf''_nonneg : ∀ (x : ), x D0 deriv^[2] f x) :
f

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

theorem concave_on_of_deriv2_nonpos' {D : set } (hD : D) {f : } (hf' : D) (hf'' : D) (hf''_nonpos : ∀ (x : ), x Dderiv^[2] f x 0) :
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 strict_convex_on_of_deriv2_pos' {D : set } (hD : D) {f : } (hf : D) (hf'' : ∀ (x : ), x D0 < 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 strict_concave_on_of_deriv2_neg' {D : set } (hD : D) {f : } (hf : D) (hf'' : ∀ (x : ), x Dderiv^[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 convex_on_univ_of_deriv2_nonneg {f : } (hf' : f) (hf'' : (deriv f)) (hf''_nonneg : ∀ (x : ), 0 deriv^[2] f x) :

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

theorem concave_on_univ_of_deriv2_nonpos {f : } (hf' : f) (hf'' : (deriv f)) (hf''_nonpos : ∀ (x : ), deriv^[2] f x 0) :

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

theorem strict_convex_on_univ_of_deriv2_pos {f : } (hf : continuous f) (hf'' : ∀ (x : ), 0 < deriv^[2] f x) :

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 strict_concave_on_univ_of_deriv2_neg {f : } (hf : continuous f) (hf'' : ∀ (x : ), deriv^[2] f x < 0) :

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.

### Functions f : E → ℝ#

theorem domain_mvt {E : Type u_1} [ E] {f : E → } {s : set E} {x y : E} {f' : E → (E →L[] )} (hf : ∀ (x : E), x s (f' x) s x) (hs : s) (xs : x s) (ys : y s) :
∃ (z : E) (H : z x y), f y - f x = (f' z) (y - x)

Lagrange's Mean Value Theorem, applied to convex domains.

### Vector-valued functions f : E → F. Strict differentiability. #

A C^1 function is strictly differentiable, when the field is ℝ or ℂ. This follows from the mean value inequality on balls, which is a particular case of the above results after restricting the scalars to ℝ. Note that it does not make sense to talk of a convex set over ℂ, but balls make sense and are enough. Many formulations of the mean value inequality could be generalized to balls over ℝ or ℂ. For now, we only include the ones that we need.

theorem has_strict_fderiv_at_of_has_fderiv_at_of_continuous_at {𝕜 : Type u_3} [is_R_or_C 𝕜] {G : Type u_4} [ G] {H : Type u_5} [ H] {f : G → H} {f' : G → (G →L[𝕜] H)} {x : G} (hder : ∀ᶠ (y : G) in nhds x, (f' y) y) (hcont : x) :
(f' x) x

Over the reals or the complexes, a continuously differentiable function is strictly differentiable.

theorem has_strict_deriv_at_of_has_deriv_at_of_continuous_at {𝕜 : Type u_3} [is_R_or_C 𝕜] {G : Type u_4} [ G] {f f' : 𝕜 → G} {x : 𝕜} (hder : ∀ᶠ (y : 𝕜) in nhds x, (f' y) y) (hcont : x) :
(f' x) x

Over the reals or the complexes, a continuously differentiable function is strictly differentiable.