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.
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.mono_of_deriv_nonneg, convex.antimono_of_deriv_nonpos, convex.strict_mono_of_deriv_pos, convex.strict_antimono_of_deriv_neg : if the derivative of a function is non-negative/non-positive/positive/negative, then the function is monotone/monotonically decreasing/strictly monotone/strictly monotonically decreasing.
convex_on_of_deriv_mono, 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 : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ set.Ico a b → ∀ (r : ℝ), f' x < r → (∃ᶠ (z : ℝ) in nhds_within x (set.Ioi x), (z - x)⁻¹ * (f z - f x) < r)) {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : continuous_on B (set.Icc a b)) (hB' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at B (B' x) (set.Ioi x) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → f x = B x → f' x < B' x) ⦃x : ℝ⦄ :

x ∈ set.Icc a b → f 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].

source

theorem image_le_of_liminf_slope_right_lt_deriv_boundary {f f' : ℝ → ℝ} {a b : ℝ} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ set.Ico a b → ∀ (r : ℝ), f' x < r → (∃ᶠ (z : ℝ) in nhds_within x (set.Ioi x), (z - x)⁻¹ * (f z - f x) < r)) {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : ∀ (x : ℝ), has_deriv_at B (B' x) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → f x = B x → f' x < B' x) ⦃x : ℝ⦄ :

x ∈ set.Icc a b → f 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].

source

theorem image_le_of_liminf_slope_right_le_deriv_boundary {f : ℝ → ℝ} {a b : ℝ} (hf : continuous_on f (set.Icc a b)) {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : continuous_on B (set.Icc a b)) (hB' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at B (B' x) (set.Ioi x) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → ∀ (r : ℝ), B' x < r → (∃ᶠ (z : ℝ) in nhds_within x (set.Ioi x), (z - x)⁻¹ * (f z - f x) < r)) ⦃x : ℝ⦄ :

x ∈ set.Icc a b → f 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].

source

theorem image_le_of_deriv_right_lt_deriv_boundary' {f f' : ℝ → ℝ} {a b : ℝ} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at f (f' x) (set.Ioi x) x) {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : continuous_on B (set.Icc a b)) (hB' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at B (B' x) (set.Ioi x) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → f x = B x → f' x < B' x) ⦃x : ℝ⦄ :

x ∈ set.Icc a b → f 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].

source

theorem image_le_of_deriv_right_lt_deriv_boundary {f f' : ℝ → ℝ} {a b : ℝ} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at f (f' x) (set.Ioi x) x) {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : ∀ (x : ℝ), has_deriv_at B (B' x) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → f x = B x → f' x < B' x) ⦃x : ℝ⦄ :

x ∈ set.Icc a b → f 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].

source

theorem image_le_of_deriv_right_le_deriv_boundary {f f' : ℝ → ℝ} {a b : ℝ} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at f (f' x) (set.Ioi x) x) {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : continuous_on B (set.Icc a b)) (hB' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at B (B' x) (set.Ioi x) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → f' x ≤ B' x) ⦃x : ℝ⦄ :

x ∈ set.Icc a b → f 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`

source

theorem image_norm_le_of_liminf_right_slope_norm_lt_deriv_boundary {a b : ℝ} {E : Type u_1} [normed_group E] {f : ℝ → E} {f' : ℝ → ℝ} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ set.Ico a b → ∀ (r : ℝ), f' x < r → (∃ᶠ (z : ℝ) in nhds_within x (set.Ioi x), (z - x)⁻¹ * (∥f z∥ - ∥f x∥) < r)) {B B' : ℝ → ℝ} (ha : ∥f a∥ ≤ B a) (hB : continuous_on B (set.Icc a b)) (hB' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at B (B' x) (set.Ioi x) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → ∥f x∥ = B x → f' x < B' x) ⦃x : ℝ⦄ :

x ∈ set.Icc a b → ∥f 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].

source

theorem image_norm_le_of_norm_deriv_right_lt_deriv_boundary' {E : Type u_1} [normed_group E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at f (f' x) (set.Ioi x) x) {B B' : ℝ → ℝ} (ha : ∥f a∥ ≤ B a) (hB : continuous_on B (set.Icc a b)) (hB' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at B (B' x) (set.Ioi x) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → ∥f x∥ = B x → ∥f' x∥ < B' x) ⦃x : ℝ⦄ :

x ∈ set.Icc a b → ∥f 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.

source

theorem image_norm_le_of_norm_deriv_right_lt_deriv_boundary {E : Type u_1} [normed_group E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at f (f' x) (set.Ioi x) x) {B B' : ℝ → ℝ} (ha : ∥f a∥ ≤ B a) (hB : ∀ (x : ℝ), has_deriv_at B (B' x) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → ∥f x∥ = B x → ∥f' x∥ < B' x) ⦃x : ℝ⦄ :

x ∈ set.Icc a b → ∥f 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.

source

theorem image_norm_le_of_norm_deriv_right_le_deriv_boundary' {E : Type u_1} [normed_group E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at f (f' x) (set.Ioi x) x) {B B' : ℝ → ℝ} (ha : ∥f a∥ ≤ B a) (hB : continuous_on B (set.Icc a b)) (hB' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at B (B' x) (set.Ioi x) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → ∥f' x∥ ≤ B' x) ⦃x : ℝ⦄ :

x ∈ set.Icc a b → ∥f 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.

source

theorem image_norm_le_of_norm_deriv_right_le_deriv_boundary {E : Type u_1} [normed_group E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at f (f' x) (set.Ioi x) x) {B B' : ℝ → ℝ} (ha : ∥f a∥ ≤ B a) (hB : ∀ (x : ℝ), has_deriv_at B (B' x) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → ∥f' x∥ ≤ B' x) ⦃x : ℝ⦄ :

x ∈ set.Icc a b → ∥f 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.

source

theorem norm_image_sub_le_of_norm_deriv_right_le_segment {E : Type u_1} [normed_group E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E} {C : ℝ} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at f (f' x) (set.Ioi x) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → ∥f' x∥ ≤ C) (x : ℝ) :

x ∈ set.Icc a 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).

source

theorem norm_image_sub_le_of_norm_deriv_le_segment' {E : Type u_1} [normed_group E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E} {C : ℝ} (hf : ∀ (x : ℝ), x ∈ set.Icc a b → has_deriv_within_at f (f' x) (set.Icc a b) x) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → ∥f' x∥ ≤ C) (x : ℝ) :

x ∈ set.Icc a 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.

source

theorem norm_image_sub_le_of_norm_deriv_le_segment {E : Type u_1} [normed_group E] [normed_space ℝ E] {f : ℝ → E} {a b C : ℝ} (hf : differentiable_on ℝ f (set.Icc a b)) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → ∥deriv_within f (set.Icc a b) x∥ ≤ C) (x : ℝ) :

x ∈ set.Icc a 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.

source

theorem norm_image_sub_le_of_norm_deriv_le_segment_01' {E : Type u_1} [normed_group E] [normed_space ℝ E] {f f' : ℝ → E} {C : ℝ} :

(∀ (x : ℝ), x ∈ set.Icc 0 1 → has_deriv_within_at f (f' x) (set.Icc 0 1) x) → (∀ (x : ℝ), x ∈ set.Ico 0 1 → ∥f' 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.

source

theorem norm_image_sub_le_of_norm_deriv_le_segment_01 {E : Type u_1} [normed_group E] [normed_space ℝ E] {f : ℝ → E} {C : ℝ} :

differentiable_on ℝ f (set.Icc 0 1) → (∀ (x : ℝ), x ∈ set.Ico 0 1 → ∥deriv_within f (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.

Vector-valued functions `f : E → F`

source

theorem convex.norm_image_sub_le_of_norm_has_fderiv_within_le {E : Type u_1} [normed_group E] [normed_space ℝ E] {F : Type u_2} [normed_group F] [normed_space ℝ F] {f : E → F} {C : ℝ} {s : set E} {x y : E} {f' : E → (E →L[ℝ ] F)} :

(∀ (x : E), x ∈ s → has_fderiv_within_at f (f' x) s x) → (∀ (x : E), x ∈ s → ∥f' x∥ ≤ C) → convex s → x ∈ s → 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.

source

theorem convex.norm_image_sub_le_of_norm_fderiv_within_le {E : Type u_1} [normed_group E] [normed_space ℝ E] {F : Type u_2} [normed_group F] [normed_space ℝ F] {f : E → F} {C : ℝ} {s : set E} {x y : E} :

differentiable_on ℝ f s → (∀ (x : E), x ∈ s → ∥fderiv_within ℝ f s x∥ ≤ C) → convex s → x ∈ s → 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.

source

theorem convex.norm_image_sub_le_of_norm_fderiv_le {E : Type u_1} [normed_group E] [normed_space ℝ E] {F : Type u_2} [normed_group F] [normed_space ℝ F] {f : E → F} {C : ℝ} {s : set E} {x y : E} :

(∀ (x : E), x ∈ s → differentiable_at ℝ f x) → (∀ (x : E), x ∈ s → ∥fderiv ℝ f x∥ ≤ C) → convex s → x ∈ s → 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.

source

theorem convex.norm_image_sub_le_of_norm_has_fderiv_within_le' {E : Type u_1} [normed_group E] [normed_space ℝ E] {F : Type u_2} [normed_group F] [normed_space ℝ F] {f : E → F} {C : ℝ} {s : set E} {x y : E} {f' : E → (E →L[ℝ ] F)} {φ : E →L[ℝ ] F} :

(∀ (x : E), x ∈ s → has_fderiv_within_at f (f' x) s x) → (∀ (x : E), x ∈ s → ∥f' x - φ∥ ≤ C) → convex s → x ∈ s → 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.

source

theorem convex.norm_image_sub_le_of_norm_fderiv_within_le' {E : Type u_1} [normed_group E] [normed_space ℝ E] {F : Type u_2} [normed_group F] [normed_space ℝ F] {f : E → F} {C : ℝ} {s : set E} {x y : E} {φ : E →L[ℝ ] F} :

differentiable_on ℝ f s → (∀ (x : E), x ∈ s → ∥fderiv_within ℝ f s x - φ∥ ≤ C) → convex s → x ∈ s → 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.

source

theorem convex.norm_image_sub_le_of_norm_fderiv_le' {E : Type u_1} [normed_group E] [normed_space ℝ E] {F : Type u_2} [normed_group F] [normed_space ℝ F] {f : E → F} {C : ℝ} {s : set E} {x y : E} {φ : E →L[ℝ ] F} :

(∀ (x : E), x ∈ s → differentiable_at ℝ f x) → (∀ (x : E), x ∈ s → ∥fderiv ℝ f x - φ∥ ≤ C) → convex s → x ∈ s → y ∈ s → ∥f y - f x - ⇑φ (y - x)∥ ≤ C * ∥y - x∥

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

source

theorem convex.is_const_of_fderiv_within_eq_zero {E : Type u_1} [normed_group E] [normed_space ℝ E] {F : Type u_2} [normed_group F] [normed_space ℝ F] {s : set E} (hs : convex s) {f : E → F} (hf : differentiable_on ℝ f s) (hf' : ∀ (x : E), x ∈ s → fderiv_within ℝ f s x = 0) {x y : E} :

x ∈ s → 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.

source

theorem is_const_of_fderiv_eq_zero {E : Type u_1} [normed_group E] [normed_space ℝ E] {F : Type u_2} [normed_group F] [normed_space ℝ F] {f : E → F} (hf : differentiable ℝ f) (hf' : ∀ (x : E), fderiv ℝ f x = 0) (x y : E) :

f x = f y

source

theorem convex.norm_image_sub_le_of_norm_has_deriv_within_le {F : Type u_2} [normed_group F] [normed_space ℝ F] {f f' : ℝ → F} {C : ℝ} {s : set ℝ} {x y : ℝ} :

(∀ (x : ℝ), x ∈ s → has_deriv_within_at f (f' x) s x) → (∀ (x : ℝ), x ∈ s → ∥f' x∥ ≤ C) → convex s → x ∈ s → 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.

source

theorem convex.norm_image_sub_le_of_norm_deriv_within_le {F : Type u_2} [normed_group F] [normed_space ℝ F] {f : ℝ → F} {C : ℝ} {s : set ℝ} {x y : ℝ} :

differentiable_on ℝ f s → (∀ (x : ℝ), x ∈ s → ∥deriv_within f s x∥ ≤ C) → convex s → x ∈ s → 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

source

theorem convex.norm_image_sub_le_of_norm_deriv_le {F : Type u_2} [normed_group F] [normed_space ℝ F] {f : ℝ → F} {C : ℝ} {s : set ℝ} {x y : ℝ} :

(∀ (x : ℝ), x ∈ s → differentiable_at ℝ f x) → (∀ (x : ℝ), x ∈ s → ∥deriv f x∥ ≤ C) → convex s → x ∈ s → 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.

Functions `[a, b] → ℝ`.

source

theorem exists_ratio_has_deriv_at_eq_ratio_slope (f f' : ℝ → ℝ) {a b : ℝ} (hab : a < b) (hfc : continuous_on f (set.Icc a b)) (hff' : ∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_at f (f' x) x) (g g' : ℝ → ℝ) :

continuous_on g (set.Icc a b) → (∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_at g (g' x) x) → (∃ (c : ℝ) (H : c ∈ set.Ioo a b), (g b - g a) * f' c = (f b - f a) * g' c)

Cauchy's Mean Value Theorem, has_deriv_at version.

source

theorem exists_ratio_has_deriv_at_eq_ratio_slope' (f f' : ℝ → ℝ) {a b : ℝ} (hab : a < b) (g g' : ℝ → ℝ) {lfa lga lfb lgb : ℝ} :

(∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_at f (f' x) x) → (∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_at g (g' x) x) → filter.tendsto f (nhds_within a (set.Ioi a)) (nhds lfa) → filter.tendsto g (nhds_within a (set.Ioi a)) (nhds lga) → filter.tendsto f (nhds_within b (set.Iio b)) (nhds lfb) → filter.tendsto g (nhds_within b (set.Iio b)) (nhds lgb) → (∃ (c : ℝ) (H : c ∈ set.Ioo a b), (lgb - lga) * f' c = (lfb - lfa) * g' c)

Cauchy's Mean Value Theorem, extended has_deriv_at version.

source

theorem exists_has_deriv_at_eq_slope (f f' : ℝ → ℝ) {a b : ℝ} :

a < b → continuous_on f (set.Icc a b) → (∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_at f (f' x) x) → (∃ (c : ℝ) (H : c ∈ set.Ioo a b), f' c = (f b - f a) / (b - a))

Lagrange's Mean Value Theorem, has_deriv_at version

source

theorem exists_ratio_deriv_eq_ratio_slope (f : ℝ → ℝ) {a b : ℝ} (hab : a < b) (hfc : continuous_on f (set.Icc a b)) (hfd : differentiable_on ℝ f (set.Ioo a b)) (g : ℝ → ℝ) :

continuous_on g (set.Icc a b) → differentiable_on ℝ g (set.Ioo a b) → (∃ (c : ℝ) (H : c ∈ set.Ioo a b), (g b - g a) * deriv f c = (f b - f a) * deriv g c)

Cauchy's Mean Value Theorem, deriv version.

source

theorem exists_ratio_deriv_eq_ratio_slope' (f : ℝ → ℝ) {a b : ℝ} (hab : a < b) (g : ℝ → ℝ) {lfa lga lfb lgb : ℝ} :

differentiable_on ℝ f (set.Ioo a b) → differentiable_on ℝ g (set.Ioo a b) → filter.tendsto f (nhds_within a (set.Ioi a)) (nhds lfa) → filter.tendsto g (nhds_within a (set.Ioi a)) (nhds lga) → filter.tendsto f (nhds_within b (set.Iio b)) (nhds lfb) → filter.tendsto g (nhds_within b (set.Iio b)) (nhds lgb) → (∃ (c : ℝ) (H : c ∈ set.Ioo a b), (lgb - lga) * deriv f c = (lfb - lfa) * deriv g c)

Cauchy's Mean Value Theorem, extended deriv version.

source

theorem exists_deriv_eq_slope (f : ℝ → ℝ) {a b : ℝ} :

a < b → continuous_on f (set.Icc a b) → differentiable_on ℝ f (set.Ioo a b) → (∃ (c : ℝ) (H : c ∈ set.Ioo a b), deriv f c = (f b - f a) / (b - a))

Lagrange's Mean Value Theorem, deriv version.

source

theorem convex.mul_sub_lt_image_sub_of_lt_deriv {D : set ℝ} (hD : convex D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D)) {C : ℝ} (hf'_gt : ∀ (x : ℝ), x ∈ interior D → C < deriv f x) (x y : ℝ) :

x ∈ D → y ∈ D → x < y → C * (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.

source

theorem mul_sub_lt_image_sub_of_lt_deriv {f : ℝ → ℝ} (hf : differentiable ℝ f) {C : ℝ} (hf'_gt : ∀ (x : ℝ), C < deriv f x) ⦃x y : ℝ⦄ :

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.

source

theorem convex.mul_sub_le_image_sub_of_le_deriv {D : set ℝ} (hD : convex D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D)) {C : ℝ} (hf'_ge : ∀ (x : ℝ), x ∈ interior D → C ≤ deriv f x) (x y : ℝ) :

x ∈ D → y ∈ D → x ≤ y → C * (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.

source

theorem mul_sub_le_image_sub_of_le_deriv {f : ℝ → ℝ} (hf : differentiable ℝ f) {C : ℝ} (hf'_ge : ∀ (x : ℝ), C ≤ deriv f x) ⦃x y : ℝ⦄ :

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.

source

theorem convex.image_sub_lt_mul_sub_of_deriv_lt {D : set ℝ} (hD : convex D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D)) {C : ℝ} (lt_hf' : ∀ (x : ℝ), x ∈ interior D → deriv f x < C) (x y : ℝ) :

x ∈ D → y ∈ D → x < y → f 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.

source

theorem image_sub_lt_mul_sub_of_deriv_lt {f : ℝ → ℝ} (hf : differentiable ℝ f) {C : ℝ} (lt_hf' : ∀ (x : ℝ), deriv f x < C) ⦃x y : ℝ⦄ :

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.

source

theorem convex.image_sub_le_mul_sub_of_deriv_le {D : set ℝ} (hD : convex D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D)) {C : ℝ} (le_hf' : ∀ (x : ℝ), x ∈ interior D → deriv f x ≤ C) (x y : ℝ) :

x ∈ D → y ∈ D → x ≤ y → f 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.

source

theorem image_sub_le_mul_sub_of_deriv_le {f : ℝ → ℝ} (hf : differentiable ℝ f) {C : ℝ} (le_hf' : ∀ (x : ℝ), deriv f x ≤ C) ⦃x y : ℝ⦄ :

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.

source

theorem convex.strict_mono_of_deriv_pos {D : set ℝ} (hD : convex D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D)) (hf'_pos : ∀ (x : ℝ), x ∈ interior D → 0 < deriv f x) (x y : ℝ) :

x ∈ D → y ∈ D → x < y → f x < f y

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 monotonically increasing function on D.

source

theorem strict_mono_of_deriv_pos {f : ℝ → ℝ} :

differentiable ℝ f → (∀ (x : ℝ), 0 < deriv f x) → strict_mono f

Let f : ℝ → ℝ be a differentiable function. If f' is positive, then f is a strictly monotonically increasing function.

source

theorem convex.mono_of_deriv_nonneg {D : set ℝ} (hD : convex D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D)) (hf'_nonneg : ∀ (x : ℝ), x ∈ interior D → 0 ≤ deriv f x) (x y : ℝ) :

x ∈ D → y ∈ D → x ≤ y → f x ≤ f y

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 monotonically increasing function on D.

source

theorem mono_of_deriv_nonneg {f : ℝ → ℝ} :

differentiable ℝ f → (∀ (x : ℝ), 0 ≤ deriv f x) → monotone f

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

source

theorem convex.strict_antimono_of_deriv_neg {D : set ℝ} (hD : convex D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D)) (hf'_neg : ∀ (x : ℝ), x ∈ interior D → deriv f x < 0) (x y : ℝ) :

x ∈ D → y ∈ D → x < y → 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 f' is negative, then f is a strictly monotonically decreasing function on D.

source

theorem strict_antimono_of_deriv_neg {f : ℝ → ℝ} (hf : differentiable ℝ f) (hf' : ∀ (x : ℝ), deriv f x < 0) ⦃x y : ℝ⦄ :

x < y → f y < f x

Let f : ℝ → ℝ be a differentiable function. If f' is negative, then f is a strictly monotonically decreasing function.

source

theorem convex.antimono_of_deriv_nonpos {D : set ℝ} (hD : convex D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D)) (hf'_nonpos : ∀ (x : ℝ), x ∈ interior D → deriv f x ≤ 0) (x y : ℝ) :

x ∈ D → y ∈ D → x ≤ y → 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 f' is nonpositive, then f is a monotonically decreasing function on D.

source

theorem antimono_of_deriv_nonpos {f : ℝ → ℝ} (hf : differentiable ℝ f) (hf' : ∀ (x : ℝ), deriv f x ≤ 0) ⦃x y : ℝ⦄ :

x ≤ y → f y ≤ f x

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

source

theorem convex_on_of_deriv_mono {D : set ℝ} (hD : convex D) {f : ℝ → ℝ} :

continuous_on f D → differentiable_on ℝ f (interior D) → (∀ (x y : ℝ), x ∈ interior D → y ∈ interior D → x ≤ y → deriv f x ≤ deriv f y) → convex_on 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 convex_on_univ_of_deriv_mono {f : ℝ → ℝ} :

differentiable ℝ f → monotone (deriv f) → convex_on set.univ 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 ℝ.

source

theorem convex_on_of_deriv2_nonneg {D : set ℝ} (hD : convex D) {f : ℝ → ℝ} :

continuous_on f D → differentiable_on ℝ f (interior D) → differentiable_on ℝ (deriv f) (interior D) → (∀ (x : ℝ), x ∈ interior D → 0 ≤ deriv ^[2] f x) → convex_on 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 convex_on_univ_of_deriv2_nonneg {f : ℝ → ℝ} :

differentiable ℝ f → differentiable ℝ (deriv f) → (∀ (x : ℝ), 0 ≤ deriv ^[2] f x) → convex_on set.univ f

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

Functions `f : E → ℝ`

source

theorem domain_mvt {E : Type u_1} [normed_group E] [normed_space ℝ E] {f : E → ℝ} {s : set E} {x y : E} {f' : E → (E →L[ℝ ] ℝ)} :

(∀ (x : E), x ∈ s → has_fderiv_within_at f (f' x) s x) → convex s → x ∈ s → y ∈ s → (∃ (z : E) (H : z ∈ segment 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.

source

theorem strict_fderiv_of_cont_diff {E : Type u_1} [normed_group E] [normed_space ℝ E] {F : Type u_2} [normed_group F] [normed_space ℝ F] {f : E → F} {s : set E} {x : E} {f' : E → (E →L[ℝ ] F)} :

(∀ (x : E), x ∈ s → has_fderiv_within_at f (f' x) s x) → continuous_on f' s → s ∈ nhds x → has_strict_fderiv_at f (f' x) x

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

mathlib documentation

analysis.calculus.mean_value

The mean value inequality and equalities

One-dimensional fencing inequalities

Vector-valued functions `f : ℝ → E`

Vector-valued functions `f : E → F`

Functions `[a, b] → ℝ`.

Functions `f : E → ℝ`

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

General documentation

Additional documentation

Library

mathlib documentation

analysis.​calculus.​mean_value

The mean value inequality and equalities

One-dimensional fencing inequalities

Vector-valued functions f : ℝ → E

Vector-valued functions f : E → F

Functions [a, b] → ℝ.

Functions f : E → ℝ

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

General documentation

Additional documentation

Library

analysis.calculus.mean_value

Vector-valued functions `f : ℝ → E`

Vector-valued functions `f : E → F`

Functions `[a, b] → ℝ`.

Functions `f : E → ℝ`

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