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 IsROrC, 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] (HasDerivWithinAt or derivWithin).

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

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

• exists_hasDerivAt_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.monotoneOn_of_deriv_nonneg, Convex.antitoneOn_of_deriv_nonpos, Convex.strictMono_of_deriv_pos, Convex.strictAnti_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.

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

• hasStrictFDerivAt_of_hasFDerivAt_of_continuousAt : 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 : ContinuousOn f (Set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ Set.Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in nhdsWithin x (Set.Ioi x), slope f x z < r) {B : ℝ → ℝ} {B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : ContinuousOn B (Set.Icc a b)) (hB' : ∀ (x : ℝ), x ∈ Set.Ico a b → HasDerivWithinAt B (B' x) (Set.Ici 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].

theorem image_le_of_liminf_slope_right_lt_deriv_boundary {f : ℝ → ℝ} {f' : ℝ → ℝ} {a : ℝ} {b : ℝ} (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ Set.Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in nhdsWithin x (Set.Ioi x), slope f x z < r) {B : ℝ → ℝ} {B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : ∀ (x : ℝ), HasDerivAt 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].

theorem image_le_of_liminf_slope_right_le_deriv_boundary {f : ℝ → ℝ} {a : ℝ} {b : ℝ} (hf : ContinuousOn f (Set.Icc a b)) {B : ℝ → ℝ} {B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : ContinuousOn B (Set.Icc a b)) (hB' : ∀ (x : ℝ), x ∈ Set.Ico a b → HasDerivWithinAt B (B' x) (Set.Ici x) x) (bound : ∀ (x : ℝ), x ∈ Set.Ico a b → ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in nhdsWithin x (Set.Ioi x), slope f x z < 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].

theorem image_le_of_deriv_right_lt_deriv_boundary' {f : ℝ → ℝ} {f' : ℝ → ℝ} {a : ℝ} {b : ℝ} (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ Set.Ico a b → HasDerivWithinAt f (f' x) (Set.Ici x) x) {B : ℝ → ℝ} {B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : ContinuousOn B (Set.Icc a b)) (hB' : ∀ (x : ℝ), x ∈ Set.Ico a b → HasDerivWithinAt B (B' x) (Set.Ici 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].

theorem image_le_of_deriv_right_lt_deriv_boundary {f : ℝ → ℝ} {f' : ℝ → ℝ} {a : ℝ} {b : ℝ} (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ Set.Ico a b → HasDerivWithinAt f (f' x) (Set.Ici x) x) {B : ℝ → ℝ} {B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : ∀ (x : ℝ), HasDerivAt 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].

theorem image_le_of_deriv_right_le_deriv_boundary {f : ℝ → ℝ} {f' : ℝ → ℝ} {a : ℝ} {b : ℝ} (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ Set.Ico a b → HasDerivWithinAt f (f' x) (Set.Ici x) x) {B : ℝ → ℝ} {B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : ContinuousOn B (Set.Icc a b)) (hB' : ∀ (x : ℝ), x ∈ Set.Ico a b → HasDerivWithinAt B (B' x) (Set.Ici 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

theorem image_norm_le_of_liminf_right_slope_norm_lt_deriv_boundary {a : ℝ} {b : ℝ} {E : Type u_3} [NormedAddCommGroup E] {f : ℝ → E} {f' : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ Set.Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in nhdsWithin x (Set.Ioi x), slope (norm ∘ f) x z < r) {B : ℝ → ℝ} {B' : ℝ → ℝ} (ha : ‖f a‖ ≤ B a) (hB : ContinuousOn B (Set.Icc a b)) (hB' : ∀ (x : ℝ), x ∈ Set.Ico a b → HasDerivWithinAt B (B' x) (Set.Ici 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].

theorem image_norm_le_of_norm_deriv_right_lt_deriv_boundary' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a : ℝ} {b : ℝ} {f' : ℝ → E} (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ Set.Ico a b → HasDerivWithinAt f (f' x) (Set.Ici x) x) {B : ℝ → ℝ} {B' : ℝ → ℝ} (ha : ‖f a‖ ≤ B a) (hB : ContinuousOn B (Set.Icc a b)) (hB' : ∀ (x : ℝ), x ∈ Set.Ico a b → HasDerivWithinAt B (B' x) (Set.Ici 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.

theorem image_norm_le_of_norm_deriv_right_lt_deriv_boundary {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a : ℝ} {b : ℝ} {f' : ℝ → E} (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ Set.Ico a b → HasDerivWithinAt f (f' x) (Set.Ici x) x) {B : ℝ → ℝ} {B' : ℝ → ℝ} (ha : ‖f a‖ ≤ B a) (hB : ∀ (x : ℝ), HasDerivAt 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.

theorem image_norm_le_of_norm_deriv_right_le_deriv_boundary' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a : ℝ} {b : ℝ} {f' : ℝ → E} (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ Set.Ico a b → HasDerivWithinAt f (f' x) (Set.Ici x) x) {B : ℝ → ℝ} {B' : ℝ → ℝ} (ha : ‖f a‖ ≤ B a) (hB : ContinuousOn B (Set.Icc a b)) (hB' : ∀ (x : ℝ), x ∈ Set.Ico a b → HasDerivWithinAt B (B' x) (Set.Ici 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.

theorem image_norm_le_of_norm_deriv_right_le_deriv_boundary {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a : ℝ} {b : ℝ} {f' : ℝ → E} (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ Set.Ico a b → HasDerivWithinAt f (f' x) (Set.Ici x) x) {B : ℝ → ℝ} {B' : ℝ → ℝ} (ha : ‖f a‖ ≤ B a) (hB : ∀ (x : ℝ), HasDerivAt 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.

theorem norm_image_sub_le_of_norm_deriv_right_le_segment {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a : ℝ} {b : ℝ} {f' : ℝ → E} {C : ℝ} (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ Set.Ico a b → HasDerivWithinAt f (f' x) (Set.Ici 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).

theorem norm_image_sub_le_of_norm_deriv_le_segment' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a : ℝ} {b : ℝ} {f' : ℝ → E} {C : ℝ} (hf : ∀ (x : ℝ), x ∈ Set.Icc a b → HasDerivWithinAt 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), HasDerivWithinAt version.

theorem norm_image_sub_le_of_norm_deriv_le_segment {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a : ℝ} {b : ℝ} {C : ℝ} (hf : DifferentiableOn ℝ f (Set.Icc a b)) (bound : ∀ (x : ℝ), x ∈ Set.Ico a b → ‖derivWithin 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), derivWithin version.

theorem norm_image_sub_le_of_norm_deriv_le_segment_01' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {f' : ℝ → E} {C : ℝ} (hf : ∀ (x : ℝ), x ∈ Set.Icc 0 1 → HasDerivWithinAt f (f' x) (Set.Icc 0 1) x) (bound : ∀ (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, HasDerivWithinAt version.

theorem norm_image_sub_le_of_norm_deriv_le_segment_01 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {C : ℝ} (hf : DifferentiableOn ℝ f (Set.Icc 0 1)) (bound : ∀ (x : ℝ), x ∈ Set.Ico 0 1 → ‖derivWithin 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, derivWithin version.

theorem constant_of_has_deriv_right_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a : ℝ} {b : ℝ} (hcont : ContinuousOn f (Set.Icc a b)) (hderiv : ∀ (x : ℝ), x ∈ Set.Ico a b → HasDerivWithinAt f 0 (Set.Ici x) x) (x : ℝ) : x ∈ Set.Icc a b → f x = f a

theorem constant_of_derivWithin_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a : ℝ} {b : ℝ} (hdiff : DifferentiableOn ℝ f (Set.Icc a b)) (hderiv : ∀ (x : ℝ), x ∈ Set.Ico a b → derivWithin f (Set.Icc a b) x = 0) (x : ℝ) : x ∈ Set.Icc a b → f x = f a

theorem eq_of_has_deriv_right_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a : ℝ} {b : ℝ} {f' : ℝ → E} {g : ℝ → E} (derivf : ∀ (x : ℝ), x ∈ Set.Ico a b → HasDerivWithinAt f (f' x) (Set.Ici x) x) (derivg : ∀ (x : ℝ), x ∈ Set.Ico a b → HasDerivWithinAt g (f' x) (Set.Ici x) x) (fcont : ContinuousOn f (Set.Icc a b)) (gcont : ContinuousOn g (Set.Icc a b)) (hi : f a = g a) (y : ℝ) : y ∈ Set.Icc a 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_derivWithin_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a : ℝ} {b : ℝ} {g : ℝ → E} (fdiff : DifferentiableOn ℝ f (Set.Icc a b)) (gdiff : DifferentiableOn ℝ g (Set.Icc a b)) (hderiv : Set.EqOn (derivWithin f (Set.Icc a b)) (derivWithin g (Set.Icc a b)) (Set.Ico a b)) (hi : f a = g a) (y : ℝ) : y ∈ Set.Icc a 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 [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 G] to achieve this result. For the domain E we also assume [NormedSpace ℝ E] to have a notion of a Convex set.

theorem Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {C : ℝ} {s : Set E} {x : E} {y : E} {f' : E → E →L[𝕜] G} (hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x) (bound : ∀ (x : E), x ∈ s → ‖f' x‖ ≤ C) (hs : Convex ℝ 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 HasFDerivWithinAt.

theorem Convex.lipschitzOnWith_of_nnnorm_hasFDerivWithin_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {s : Set E} {f' : E → E →L[𝕜] G} {C : NNReal} (hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x) (bound : ∀ (x : E), x ∈ s → ‖f' x‖₊ ≤ C) (hs : Convex ℝ s) : LipschitzOnWith 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 HasFDerivWithinAt and LipschitzOnWith.

theorem Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {x : E} {f' : E → E →L[𝕜] G} (hs : Convex ℝ s) {f : E → G} (hder : ∀ᶠ (y : E) in nhdsWithin x s, HasFDerivWithinAt f (f' y) s y) (hcont : ContinuousWithinAt f' s x) (K : NNReal) (hK : ‖f' x‖₊ < K) : ∃ t, t ∈ nhdsWithin x s ∧ LipschitzOnWith K f 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_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt for a version that claims existence of K instead of an explicit estimate.

theorem Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {x : E} {f' : E → E →L[𝕜] G} (hs : Convex ℝ s) {f : E → G} (hder : ∀ᶠ (y : E) in nhdsWithin x s, HasFDerivWithinAt f (f' y) s y) (hcont : ContinuousWithinAt f' s x) : ∃ K t, t ∈ nhdsWithin x s ∧ LipschitzOnWith K f 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_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt for a version with an explicit estimate on the Lipschitz constant.

theorem Convex.norm_image_sub_le_of_norm_fderivWithin_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {C : ℝ} {s : Set E} {x : E} {y : E} (hf : DifferentiableOn 𝕜 f s) (bound : ∀ (x : E), x ∈ s → ‖fderivWithin 𝕜 f s x‖ ≤ C) (hs : Convex ℝ 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 fderivWithin.

theorem Convex.lipschitzOnWith_of_nnnorm_fderivWithin_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {s : Set E} {C : NNReal} (hf : DifferentiableOn 𝕜 f s) (bound : ∀ (x : E), x ∈ s → ‖fderivWithin 𝕜 f s x‖₊ ≤ C) (hs : Convex ℝ s) : LipschitzOnWith 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 fderivWithin and LipschitzOnWith.

theorem Convex.norm_image_sub_le_of_norm_fderiv_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {C : ℝ} {s : Set E} {x : E} {y : E} (hf : ∀ (x : E), x ∈ s → DifferentiableAt 𝕜 f x) (bound : ∀ (x : E), x ∈ s → ‖fderiv 𝕜 f x‖ ≤ C) (hs : Convex ℝ 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.lipschitzOnWith_of_nnnorm_fderiv_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {s : Set E} {C : NNReal} (hf : ∀ (x : E), x ∈ s → DifferentiableAt 𝕜 f x) (bound : ∀ (x : E), x ∈ s → ‖fderiv 𝕜 f x‖₊ ≤ C) (hs : Convex ℝ s) : LipschitzOnWith 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 LipschitzOnWith.

theorem lipschitzWith_of_nnnorm_fderiv_le {𝕜 : Type u_3} {G : Type u_4} [IsROrC 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {E : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : E → G} {C : NNReal} (hf : Differentiable 𝕜 f) (bound : ∀ (x : E), ‖fderiv 𝕜 f x‖₊ ≤ C) : LipschitzWith C f

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

theorem Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {C : ℝ} {s : Set E} {x : E} {y : E} {f' : E → E →L[𝕜] G} {φ : E →L[𝕜] G} (hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x) (bound : ∀ (x : E), x ∈ s → ‖f' x - φ‖ ≤ C) (hs : Convex ℝ 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 HasFDerivWithinAt.

theorem Convex.norm_image_sub_le_of_norm_fderivWithin_le' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {C : ℝ} {s : Set E} {x : E} {y : E} {φ : E →L[𝕜] G} (hf : DifferentiableOn 𝕜 f s) (bound : ∀ (x : E), x ∈ s → ‖fderivWithin 𝕜 f s x - φ‖ ≤ C) (hs : Convex ℝ 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 fderivWithin.

theorem Convex.norm_image_sub_le_of_norm_fderiv_le' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {C : ℝ} {s : Set E} {x : E} {y : E} {φ : E →L[𝕜] G} (hf : ∀ (x : E), x ∈ s → DifferentiableAt 𝕜 f x) (bound : ∀ (x : E), x ∈ s → ‖fderiv 𝕜 f x - φ‖ ≤ C) (hs : Convex ℝ 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_fderivWithin_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {s : Set E} {x : E} {y : E} (hs : Convex ℝ s) (hf : DifferentiableOn 𝕜 f s) (hf' : ∀ (x : E), x ∈ s → fderivWithin 𝕜 f 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 {𝕜 : Type u_3} {G : Type u_4} [IsROrC 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {E : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : E → G} (hf : Differentiable 𝕜 f) (hf' : ∀ (x : E), fderiv 𝕜 f x = 0) (x : E) (y : E) : f x = f y

theorem Convex.eqOn_of_fderivWithin_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {g : E → G} {s : Set E} {x : E} (hs : Convex ℝ s) (hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s) (hs' : UniqueDiffOn 𝕜 s) (hf' : ∀ (x : E), x ∈ s → fderivWithin 𝕜 f s x = fderivWithin 𝕜 g s x) (hx : x ∈ s) (hfgx : f x = g x) : Set.EqOn f g s

If two functions have equal Fréchet derivatives at every point of a convex set, and are equal at one point in that set, then they are equal on that set.

theorem eq_of_fderiv_eq {𝕜 : Type u_3} {G : Type u_4} [IsROrC 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {E : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : E → G} {g : E → G} (hf : Differentiable 𝕜 f) (hg : Differentiable 𝕜 g) (hf' : ∀ (x : E), fderiv 𝕜 f x = fderiv 𝕜 g x) (x : E) (hfgx : f x = g x) : f = g

theorem Convex.norm_image_sub_le_of_norm_hasDerivWithin_le {𝕜 : Type u_3} {G : Type u_4} [IsROrC 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : 𝕜 → G} {f' : 𝕜 → G} {s : Set 𝕜} {x : 𝕜} {y : 𝕜} {C : ℝ} (hf : ∀ (x : 𝕜), x ∈ s → HasDerivWithinAt f (f' x) s x) (bound : ∀ (x : 𝕜), x ∈ s → ‖f' x‖ ≤ C) (hs : Convex ℝ 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 HasDerivWithinAt.

theorem Convex.lipschitzOnWith_of_nnnorm_hasDerivWithin_le {𝕜 : Type u_3} {G : Type u_4} [IsROrC 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : 𝕜 → G} {f' : 𝕜 → G} {s : Set 𝕜} {C : NNReal} (hs : Convex ℝ s) (hf : ∀ (x : 𝕜), x ∈ s → HasDerivWithinAt f (f' x) s x) (bound : ∀ (x : 𝕜), x ∈ s → ‖f' x‖₊ ≤ C) : LipschitzOnWith 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 HasDerivWithinAt and LipschitzOnWith.

theorem Convex.norm_image_sub_le_of_norm_derivWithin_le {𝕜 : Type u_3} {G : Type u_4} [IsROrC 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : 𝕜 → G} {s : Set 𝕜} {x : 𝕜} {y : 𝕜} {C : ℝ} (hf : DifferentiableOn 𝕜 f s) (bound : ∀ (x : 𝕜), x ∈ s → ‖derivWithin f s x‖ ≤ C) (hs : Convex ℝ 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 derivWithin

theorem Convex.lipschitzOnWith_of_nnnorm_derivWithin_le {𝕜 : Type u_3} {G : Type u_4} [IsROrC 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : 𝕜 → G} {s : Set 𝕜} {C : NNReal} (hs : Convex ℝ s) (hf : DifferentiableOn 𝕜 f s) (bound : ∀ (x : 𝕜), x ∈ s → ‖derivWithin f s x‖₊ ≤ C) : LipschitzOnWith 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 derivWithin and LipschitzOnWith.

theorem Convex.norm_image_sub_le_of_norm_deriv_le {𝕜 : Type u_3} {G : Type u_4} [IsROrC 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : 𝕜 → G} {s : Set 𝕜} {x : 𝕜} {y : 𝕜} {C : ℝ} (hf : ∀ (x : 𝕜), x ∈ s → DifferentiableAt 𝕜 f x) (bound : ∀ (x : 𝕜), x ∈ s → ‖deriv f x‖ ≤ C) (hs : Convex ℝ 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.lipschitzOnWith_of_nnnorm_deriv_le {𝕜 : Type u_3} {G : Type u_4} [IsROrC 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : 𝕜 → G} {s : Set 𝕜} {C : NNReal} (hf : ∀ (x : 𝕜), x ∈ s → DifferentiableAt 𝕜 f x) (bound : ∀ (x : 𝕜), x ∈ s → ‖deriv f x‖₊ ≤ C) (hs : Convex ℝ s) : LipschitzOnWith 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 LipschitzOnWith.

theorem lipschitzWith_of_nnnorm_deriv_le {𝕜 : Type u_3} {G : Type u_4} [IsROrC 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : 𝕜 → G} {C : NNReal} (hf : Differentiable 𝕜 f) (bound : ∀ (x : 𝕜), ‖deriv f x‖₊ ≤ C) : LipschitzWith C f

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

theorem is_const_of_deriv_eq_zero {𝕜 : Type u_3} {G : Type u_4} [IsROrC 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : 𝕜 → G} (hf : Differentiable 𝕜 f) (hf' : ∀ (x : 𝕜), deriv f 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_hasDerivAt_eq_ratio_slope (f : ℝ → ℝ) (f' : ℝ → ℝ) {a : ℝ} {b : ℝ} (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hff' : ∀ (x : ℝ), x ∈ Set.Ioo a b → HasDerivAt f (f' x) x) (g : ℝ → ℝ) (g' : ℝ → ℝ) (hgc : ContinuousOn g (Set.Icc a b)) (hgg' : ∀ (x : ℝ), x ∈ Set.Ioo a b → HasDerivAt g (g' x) x) : ∃ c, c ∈ Set.Ioo a b ∧ (g b - g a) * f' c = (f b - f a) * g' c

Cauchy's Mean Value Theorem, HasDerivAt version.

theorem exists_ratio_hasDerivAt_eq_ratio_slope' (f : ℝ → ℝ) (f' : ℝ → ℝ) {a : ℝ} {b : ℝ} (hab : a < b) (g : ℝ → ℝ) (g' : ℝ → ℝ) {lfa : ℝ} {lga : ℝ} {lfb : ℝ} {lgb : ℝ} (hff' : ∀ (x : ℝ), x ∈ Set.Ioo a b → HasDerivAt f (f' x) x) (hgg' : ∀ (x : ℝ), x ∈ Set.Ioo a b → HasDerivAt g (g' x) x) (hfa : Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds lfa)) (hga : Filter.Tendsto g (nhdsWithin a (Set.Ioi a)) (nhds lga)) (hfb : Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds lfb)) (hgb : Filter.Tendsto g (nhdsWithin b (Set.Iio b)) (nhds lgb)) : ∃ c, c ∈ Set.Ioo a b ∧ (lgb - lga) * f' c = (lfb - lfa) * g' c

Cauchy's Mean Value Theorem, extended HasDerivAt version.

theorem exists_hasDerivAt_eq_slope (f : ℝ → ℝ) (f' : ℝ → ℝ) {a : ℝ} {b : ℝ} (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hff' : ∀ (x : ℝ), x ∈ Set.Ioo a b → HasDerivAt f (f' x) x) : ∃ c, c ∈ Set.Ioo a b ∧ f' c = (f b - f a) / (b - a)

Lagrange's Mean Value Theorem, HasDerivAt version

theorem exists_ratio_deriv_eq_ratio_slope (f : ℝ → ℝ) {a : ℝ} {b : ℝ} (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hfd : DifferentiableOn ℝ f (Set.Ioo a b)) (g : ℝ → ℝ) (hgc : ContinuousOn g (Set.Icc a b)) (hgd : DifferentiableOn ℝ g (Set.Ioo a b)) : ∃ c, 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 : ℝ} (hdf : DifferentiableOn ℝ f (Set.Ioo a b)) (hdg : DifferentiableOn ℝ g (Set.Ioo a b)) (hfa : Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds lfa)) (hga : Filter.Tendsto g (nhdsWithin a (Set.Ioi a)) (nhds lga)) (hfb : Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds lfb)) (hgb : Filter.Tendsto g (nhdsWithin b (Set.Iio b)) (nhds lgb)) : ∃ c, 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 : ℝ} (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hfd : DifferentiableOn ℝ f (Set.Ioo a b)) : ∃ c, 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 : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D)) {C : (fun x => ℝ) 1} (hf'_gt : ∀ (x : ℝ), x ∈ interior D → C < deriv f x) (x : ℝ) : x ∈ D → ∀ (y : ℝ), 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.

theorem mul_sub_lt_image_sub_of_lt_deriv {f : ℝ → ℝ} (hf : Differentiable ℝ f) {C : (fun x => ℝ) 1} (hf'_gt : ∀ (x : ℝ), C < deriv f 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 : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D)) {C : (fun x => ℝ) 1} (hf'_ge : ∀ (x : ℝ), x ∈ interior D → C ≤ deriv f x) (x : ℝ) : x ∈ D → ∀ (y : ℝ), 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.

theorem mul_sub_le_image_sub_of_le_deriv {f : ℝ → ℝ} (hf : Differentiable ℝ f) {C : (fun x => ℝ) 1} (hf'_ge : ∀ (x : ℝ), C ≤ deriv f 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 : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D)) {C : (fun x => ℝ) 1} (lt_hf' : ∀ (x : ℝ), x ∈ interior D → deriv f x < C) (x : ℝ) (hx : x ∈ D) (y : ℝ) (hy : y ∈ D) (hxy : 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.

theorem image_sub_lt_mul_sub_of_deriv_lt {f : ℝ → ℝ} (hf : Differentiable ℝ f) {C : (fun x => ℝ) 1} (lt_hf' : ∀ (x : ℝ), deriv f 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 : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D)) {C : (fun x => ℝ) 1} (le_hf' : ∀ (x : ℝ), x ∈ interior D → deriv f x ≤ C) (x : ℝ) (hx : x ∈ D) (y : ℝ) (hy : y ∈ D) (hxy : 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.

theorem image_sub_le_mul_sub_of_deriv_le {f : ℝ → ℝ} (hf : Differentiable ℝ f) {C : (fun x => ℝ) 1} (le_hf' : ∀ (x : ℝ), deriv f 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.strictMonoOn_of_deriv_pos {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : ∀ (x : ℝ), x ∈ interior D → 0 < deriv f x) : StrictMonoOn f 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 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 strictMono_of_deriv_pos {f : ℝ → ℝ} (hf' : ∀ (x : ℝ), 0 < deriv f x) : StrictMono f

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.monotoneOn_of_deriv_nonneg {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D)) (hf'_nonneg : ∀ (x : ℝ), x ∈ interior D → 0 ≤ deriv f x) : MonotoneOn f 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 : Differentiable ℝ f) (hf' : ∀ (x : ℝ), 0 ≤ deriv f x) : Monotone f

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

theorem Convex.strictAntiOn_of_deriv_neg {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : ∀ (x : ℝ), x ∈ interior D → deriv f x < 0) : StrictAntiOn f 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 negative, then f is a strictly antitone function on D.

theorem strictAnti_of_deriv_neg {f : ℝ → ℝ} (hf' : ∀ (x : ℝ), deriv f x < 0) : StrictAnti f

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.antitoneOn_of_deriv_nonpos {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D)) (hf'_nonpos : ∀ (x : ℝ), x ∈ interior D → deriv f x ≤ 0) : AntitoneOn f 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 : Differentiable ℝ f) (hf' : ∀ (x : ℝ), deriv f x ≤ 0) : Antitone f

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

theorem MonotoneOn.convexOn_of_deriv {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D)) (hf'_mono : MonotoneOn (deriv f) (interior D)) : ConvexOn ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ, is differentiable on its interior, and f' is monotone on the interior, then f is convex on D.

theorem AntitoneOn.concaveOn_of_deriv {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D)) (h_anti : AntitoneOn (deriv f) (interior D)) : ConcaveOn ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ, is differentiable on its interior, and f' is antitone on the interior, then f is concave on D.

theorem StrictMonoOn.exists_slope_lt_deriv_aux {x : ℝ} {y : ℝ} {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc x y)) (hxy : x < y) (hf'_mono : StrictMonoOn (deriv f) (Set.Ioo x y)) (h : ∀ (w : ℝ), w ∈ Set.Ioo x y → deriv f w ≠ 0) : ∃ a, a ∈ Set.Ioo x y ∧ (f y - f x) / (y - x) < deriv f a

theorem StrictMonoOn.exists_slope_lt_deriv {x : ℝ} {y : ℝ} {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc x y)) (hxy : x < y) (hf'_mono : StrictMonoOn (deriv f) (Set.Ioo x y)) : ∃ a, a ∈ Set.Ioo x y ∧ (f y - f x) / (y - x) < deriv f a

theorem StrictMonoOn.exists_deriv_lt_slope_aux {x : ℝ} {y : ℝ} {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc x y)) (hxy : x < y) (hf'_mono : StrictMonoOn (deriv f) (Set.Ioo x y)) (h : ∀ (w : ℝ), w ∈ Set.Ioo x y → deriv f w ≠ 0) : ∃ a, a ∈ Set.Ioo x y ∧ deriv f a < (f y - f x) / (y - x)

theorem StrictMonoOn.exists_deriv_lt_slope {x : ℝ} {y : ℝ} {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc x y)) (hxy : x < y) (hf'_mono : StrictMonoOn (deriv f) (Set.Ioo x y)) : ∃ a, a ∈ Set.Ioo x y ∧ deriv f a < (f y - f x) / (y - x)

theorem StrictMonoOn.strictConvexOn_of_deriv {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : StrictMonoOn (deriv f) (interior D)) : StrictConvexOn ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ, and f' is strictly monotone on the interior, then f is strictly convex on D. Note that we don't require differentiability, since it is guaranteed at all but at most one point by the strict monotonicity of f'.

theorem StrictAntiOn.strictConcaveOn_of_deriv {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (h_anti : StrictAntiOn (deriv f) (interior D)) : StrictConcaveOn ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ and f' is strictly antitone on the interior, then f is strictly concave on D. Note that we don't require differentiability, since it is guaranteed at all but at most one point by the strict antitonicity of f'.

theorem Monotone.convexOn_univ_of_deriv {f : ℝ → ℝ} (hf : Differentiable ℝ f) (hf'_mono : Monotone (deriv f)) : ConvexOn ℝ Set.univ f

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

theorem Antitone.concaveOn_univ_of_deriv {f : ℝ → ℝ} (hf : Differentiable ℝ f) (hf'_anti : Antitone (deriv f)) : ConcaveOn ℝ Set.univ f

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

theorem StrictMono.strictConvexOn_univ_of_deriv {f : ℝ → ℝ} (hf : Continuous f) (hf'_mono : StrictMono (deriv f)) : StrictConvexOn ℝ Set.univ f

If a function f is continuous and f' is strictly monotone on ℝ then f is strictly convex. Note that we don't require differentiability, since it is guaranteed at all but at most one point by the strict monotonicity of f'.

theorem StrictAnti.strictConcaveOn_univ_of_deriv {f : ℝ → ℝ} (hf : Continuous f) (hf'_anti : StrictAnti (deriv f)) : StrictConcaveOn ℝ Set.univ f

If a function f is continuous and f' is strictly antitone on ℝ then f is strictly concave. Note that we don't require differentiability, since it is guaranteed at all but at most one point by the strict antitonicity of f'.

theorem convexOn_of_deriv2_nonneg {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D)) (hf'' : DifferentiableOn ℝ (deriv f) (interior D)) (hf''_nonneg : ∀ (x : ℝ), x ∈ interior D → 0 ≤ deriv^[2] f x) : ConvexOn ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ, is twice differentiable on its interior, and f'' is nonnegative on the interior, then f is convex on D.

theorem concaveOn_of_deriv2_nonpos {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D)) (hf'' : DifferentiableOn ℝ (deriv f) (interior D)) (hf''_nonpos : ∀ (x : ℝ), x ∈ interior D → deriv^[2] f x ≤ 0) : ConcaveOn ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ, is twice differentiable on its interior, and f'' is nonpositive on the interior, then f is concave on D.

theorem strictConvexOn_of_deriv2_pos {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf'' : ∀ (x : ℝ), x ∈ interior D → 0 < deriv^[2] f x) : StrictConvexOn ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ and f'' is strictly positive on the interior, then f is strictly convex on D. Note that we don't require twice differentiability explicitly as it is already implied by the second derivative being strictly positive, except at at most one point.

theorem strictConcaveOn_of_deriv2_neg {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf'' : ∀ (x : ℝ), x ∈ interior D → deriv^[2] f x < 0) : StrictConcaveOn ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ and f'' is strictly negative on the interior, then f is strictly concave on D. Note that we don't require twice differentiability explicitly as it already implied by the second derivative being strictly negative, except at at most one point.

theorem convexOn_of_deriv2_nonneg' {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf' : DifferentiableOn ℝ f D) (hf'' : DifferentiableOn ℝ (deriv f) D) (hf''_nonneg : ∀ (x : ℝ), x ∈ D → 0 ≤ deriv^[2] f x) : ConvexOn ℝ D f

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

theorem concaveOn_of_deriv2_nonpos' {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf' : DifferentiableOn ℝ f D) (hf'' : DifferentiableOn ℝ (deriv f) D) (hf''_nonpos : ∀ (x : ℝ), x ∈ D → deriv^[2] f x ≤ 0) : ConcaveOn ℝ D f

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

theorem strictConvexOn_of_deriv2_pos' {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf'' : ∀ (x : ℝ), x ∈ D → 0 < deriv^[2] f x) : StrictConvexOn ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ and f'' is strictly positive on D, then f is strictly convex on D. Note that we don't require twice differentiability explicitly as it is already implied by the second derivative being strictly positive, except at at most one point.

theorem strictConcaveOn_of_deriv2_neg' {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf'' : ∀ (x : ℝ), x ∈ D → deriv^[2] f x < 0) : StrictConcaveOn ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ and f'' is strictly negative on D, then f is strictly concave on D. Note that we don't require twice differentiability explicitly as it is already implied by the second derivative being strictly negative, except at at most one point.

theorem convexOn_univ_of_deriv2_nonneg {f : ℝ → ℝ} (hf' : Differentiable ℝ f) (hf'' : Differentiable ℝ (deriv f)) (hf''_nonneg : ∀ (x : ℝ), 0 ≤ deriv^[2] f x) : ConvexOn ℝ Set.univ f

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

theorem concaveOn_univ_of_deriv2_nonpos {f : ℝ → ℝ} (hf' : Differentiable ℝ f) (hf'' : Differentiable ℝ (deriv f)) (hf''_nonpos : ∀ (x : ℝ), deriv^[2] f x ≤ 0) : ConcaveOn ℝ Set.univ f

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

theorem strictConvexOn_univ_of_deriv2_pos {f : ℝ → ℝ} (hf : Continuous f) (hf'' : ∀ (x : ℝ), 0 < deriv^[2] f x) : StrictConvexOn ℝ Set.univ f

If a function f is continuous on ℝ, and f'' is strictly positive on ℝ, then f is strictly convex on ℝ. Note that we don't require twice differentiability explicitly as it is already implied by the second derivative being strictly positive, except at at most one point.

theorem strictConcaveOn_univ_of_deriv2_neg {f : ℝ → ℝ} (hf : Continuous f) (hf'' : ∀ (x : ℝ), deriv^[2] f x < 0) : StrictConcaveOn ℝ Set.univ f

If a function f is continuous on ℝ, and f'' is strictly negative on ℝ, then f is strictly concave on ℝ. Note that we don't require twice differentiability explicitly as it is already implied by the second derivative being strictly negative, except at at most one point.

Functions f : E → ℝ

theorem domain_mvt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {x : E} {y : E} {f' : E → E →L[ℝ] ℝ} (hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x) (hs : Convex ℝ s) (xs : x ∈ s) (ys : y ∈ s) : ∃ z, 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.

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 hasStrictFDerivAt_of_hasFDerivAt_of_continuousAt {𝕜 : Type u_3} [IsROrC 𝕜] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {H : Type u_5} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {f : G → H} {f' : G → G →L[𝕜] H} {x : G} (hder : ∀ᶠ (y : G) in nhds x, HasFDerivAt f (f' y) y) (hcont : ContinuousAt f' x) : HasStrictFDerivAt f (f' x) x

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

theorem hasStrictDerivAt_of_hasDerivAt_of_continuousAt {𝕜 : Type u_3} [IsROrC 𝕜] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : 𝕜 → G} {f' : 𝕜 → G} {x : 𝕜} (hder : ∀ᶠ (y : 𝕜) in nhds x, HasDerivAt f (f' y) y) (hcont : ContinuousAt f' x) : HasStrictDerivAt f (f' x) x

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