mathlib documentation

analysis.calculus.mean_value

The mean value inequality and equalities

In this file we prove the following facts:

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 𝓝[set.Ioi x] 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 bhas_deriv_within_at B (B' x) (set.Ioi x) x) (bound : ∀ (x : ), x set.Ico a bf x = B xf' x < B' x) ⦃x :  :
x set.Icc a 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 : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ), x set.Ico a b∀ (r : ), f' x < r(∃ᶠ (z : ) in 𝓝[set.Ioi x] 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 bf x = B xf' x < B' x) ⦃x :  :
x set.Icc a 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 : 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 bhas_deriv_within_at B (B' x) (set.Ioi x) x) (bound : ∀ (x : ), x set.Ico a b∀ (r : ), B' x < r(∃ᶠ (z : ) in 𝓝[set.Ioi x] x, (z - x)⁻¹ * (f z - f x) < r)) ⦃x :  :
x set.Icc a 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 : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ), x set.Ico a bhas_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 bhas_deriv_within_at B (B' x) (set.Ioi x) x) (bound : ∀ (x : ), x set.Ico a bf x = B xf' x < B' x) ⦃x :  :
x set.Icc a 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 : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ), x set.Ico a bhas_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 bf x = B xf' x < B' x) ⦃x :  :
x set.Icc a 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 : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ), x set.Ico a bhas_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 bhas_deriv_within_at B (B' x) (set.Ioi x) x) (bound : ∀ (x : ), x set.Ico a bf' x B' x) ⦃x :  :
x set.Icc a 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} [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 𝓝[set.Ioi x] 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 bhas_deriv_within_at B (B' x) (set.Ioi x) x) (bound : ∀ (x : ), x set.Ico a bf x = B xf' x < B' x) ⦃x :  :
x set.Icc a 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} [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 bhas_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 bhas_deriv_within_at B (B' x) (set.Ioi x) x) (bound : ∀ (x : ), x set.Ico a bf x = B xf' x < B' x) ⦃x :  :
x set.Icc a 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} [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 bhas_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 bf x = B xf' x < B' x) ⦃x :  :
x set.Icc a 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} [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 bhas_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 bhas_deriv_within_at B (B' x) (set.Ioi x) x) (bound : ∀ (x : ), x set.Ico a bf' x B' x) ⦃x :  :
x set.Icc a 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} [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 bhas_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 bf' x B' x) ⦃x :  :
x set.Icc a 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} [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 bhas_deriv_within_at f (f' x) (set.Ioi x) x) (bound : ∀ (x : ), x set.Ico a bf' x C) (x : ) :
x set.Icc a bf 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} [normed_group E] [normed_space E] {f : → E} {a b : } {f' : → E} {C : } (hf : ∀ (x : ), x set.Icc a bhas_deriv_within_at f (f' x) (set.Icc a b) x) (bound : ∀ (x : ), x set.Ico a bf' x C) (x : ) :
x set.Icc a bf 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} [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 bderiv_within f (set.Icc a b) x C) (x : ) :
x set.Icc a bf 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} [normed_group E] [normed_space E] {f f' : → E} {C : } :
(∀ (x : ), x set.Icc 0 1has_deriv_within_at f (f' x) (set.Icc 0 1) x)(∀ (x : ), x set.Ico 0 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} [normed_group E] [normed_space E] {f : → E} {C : } :
differentiable_on f (set.Icc 0 1)(∀ (x : ), x set.Ico 0 1deriv_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

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 shas_fderiv_within_at f (f' x) s x)(∀ (x : E), x sf' x C)convex sx sy sf 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_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} {f' : E → (E →L[] F)} :
(∀ (x : E), x shas_fderiv_within_at f (f' x) s x)(∀ (x : E), x sf' x C)convex slipschitz_on_with (nnreal.of_real C) f 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.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 sfderiv_within f s x C)convex sx sy sf 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_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} :
differentiable_on f s(∀ (x : E), x sfderiv_within f s x C)convex slipschitz_on_with (nnreal.of_real C) f 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} [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 sdifferentiable_at f x)(∀ (x : E), x sfderiv f x C)convex sx sy sf 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_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 : E), x sdifferentiable_at f x)(∀ (x : E), x sfderiv f x C)convex slipschitz_on_with (nnreal.of_real C) f 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} [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 shas_fderiv_within_at f (f' x) s x)(∀ (x : E), x sf' x - φ C)convex sx sy sf 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} [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 sfderiv_within f s x - φ C)convex sx sy sf 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} [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 sdifferentiable_at f x)(∀ (x : E), x sfderiv f x - φ C)convex sx sy sf 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} [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 sfderiv_within f s x = 0) {x y : E} :
x sy sf 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} [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

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 shas_deriv_within_at f (f' x) s x)(∀ (x : ), x sf' x C)convex sx sy sf 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_norm_has_deriv_within_le {F : Type u_2} [normed_group F] [normed_space F] {f f' : → F} {C : } {s : set } :
convex s(∀ (x : ), x shas_deriv_within_at f (f' x) s x)(∀ (x : ), x sf' x C)lipschitz_on_with (nnreal.of_real C) f 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 {F : Type u_2} [normed_group F] [normed_space F] {f : → F} {C : } {s : set } {x y : } :
differentiable_on f s(∀ (x : ), x sderiv_within f s x C)convex sx sy sf 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_norm_deriv_within_le {F : Type u_2} [normed_group F] [normed_space F] {f : → F} {C : } {s : set } :
convex sdifferentiable_on f s(∀ (x : ), x sderiv_within f s x C)lipschitz_on_with (nnreal.of_real C) f 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 {F : Type u_2} [normed_group F] [normed_space F] {f : → F} {C : } {s : set } {x y : } :
(∀ (x : ), x sdifferentiable_at f x)(∀ (x : ), x sderiv f x C)convex sx sy sf 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_norm_deriv_le {F : Type u_2} [normed_group F] [normed_space F] {f : → F} {C : } {s : set } :
(∀ (x : ), x sdifferentiable_at f x)(∀ (x : ), x sderiv f x C)convex slipschitz_on_with (nnreal.of_real C) f 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.

Functions [a, b] → ℝ.

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 bhas_deriv_at f (f' x) x) (g g' : ) :
continuous_on g (set.Icc a b)(∀ (x : ), x set.Ioo a bhas_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.

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 bhas_deriv_at f (f' x) x)(∀ (x : ), x set.Ioo a bhas_deriv_at g (g' x) x)filter.tendsto f (𝓝[set.Ioi a] a) (𝓝 lfa)filter.tendsto g (𝓝[set.Ioi a] a) (𝓝 lga)filter.tendsto f (𝓝[set.Iio b] b) (𝓝 lfb)filter.tendsto g (𝓝[set.Iio b] b) (𝓝 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.

theorem exists_has_deriv_at_eq_slope (f f' : ) {a b : } :
a < bcontinuous_on f (set.Icc a b)(∀ (x : ), x set.Ioo a bhas_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

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.

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 (𝓝[set.Ioi a] a) (𝓝 lfa)filter.tendsto g (𝓝[set.Ioi a] a) (𝓝 lga)filter.tendsto f (𝓝[set.Iio b] b) (𝓝 lfb)filter.tendsto g (𝓝[set.Iio b] b) (𝓝 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.

theorem exists_deriv_eq_slope (f : ) {a b : } :
a < bcontinuous_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.

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 DC < deriv f x) (x y : ) :
x Dy Dx < 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 : differentiable f) {C : } (hf'_gt : ∀ (x : ), C < deriv f x) ⦃x y :  :
x < yC * (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 : convex D) {f : } (hf : continuous_on f D) (hf' : differentiable_on f (interior D)) {C : } (hf'_ge : ∀ (x : ), x interior DC deriv f x) (x y : ) :
x Dy Dx 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 : differentiable f) {C : } (hf'_ge : ∀ (x : ), C deriv f x) ⦃x y :  :
x yC * (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 : convex D) {f : } (hf : continuous_on f D) (hf' : differentiable_on f (interior D)) {C : } (lt_hf' : ∀ (x : ), x interior Dderiv f x < C) (x y : ) :
x Dy Dx < 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 : differentiable f) {C : } (lt_hf' : ∀ (x : ), deriv f x < C) ⦃x y :  :
x < yf 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 : convex D) {f : } (hf : continuous_on f D) (hf' : differentiable_on f (interior D)) {C : } (le_hf' : ∀ (x : ), x interior Dderiv f x C) (x y : ) :
x Dy Dx 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 : differentiable f) {C : } (le_hf' : ∀ (x : ), deriv f x C) ⦃x y :  :
x yf 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_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 D0 < deriv f x) (x y : ) :
x Dy Dx < yf 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.

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.

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 D0 deriv f x) (x y : ) :
x Dy Dx yf 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.

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.

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 Dderiv f x < 0) (x y : ) :
x Dy Dx < yf 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.

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

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

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 Dderiv f x 0) (x y : ) :
x Dy Dx yf 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.

theorem antimono_of_deriv_nonpos {f : } (hf : differentiable f) (hf' : ∀ (x : ), deriv f x 0) ⦃x y :  :
x yf y f x

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

theorem convex_on_of_deriv_mono {D : set } (hD : convex D) {f : } :
continuous_on f Ddifferentiable_on f (interior D)(∀ (x y : ), x interior Dy interior Dx yderiv 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.

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 .

theorem convex_on_of_deriv2_nonneg {D : set } (hD : convex D) {f : } :
continuous_on f Ddifferentiable_on f (interior D)differentiable_on (deriv f) (interior D)(∀ (x : ), x interior D0 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.

theorem convex_on_univ_of_deriv2_nonneg {f : } :
differentiable fdifferentiable (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 → ℝ

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 shas_fderiv_within_at f (f' x) s x)convex sx sy 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.

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 shas_fderiv_within_at f (f' x) s x)continuous_on f' ss 𝓝 xhas_strict_fderiv_at f (f' x) x

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