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 RCLike, 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.

• 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 ∈ 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 ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) (bound : ∀ 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 ∈ 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 ∈ 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 ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) (bound : ∀ 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 ∈ 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 ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) (bound : ∀ 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 ∈ 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 ∈ 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 ∈ 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 ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) (bound : ∀ 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 ∈ 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 ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) (bound : ∀ 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 ∈ 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 ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) (bound : ∀ 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 ∈ 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 ∈ 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 ∈ 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 ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) (bound : ∀ 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 ∈ 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 ∈ 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 ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) (bound : ∀ 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 ∈ Set.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x) (bound : ∀ 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 ∈ 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 f' : ℝ → E} {C : ℝ} (hf : ∀ x ∈ Set.Icc 0 1, HasDerivWithinAt f (f' x) (Set.Icc 0 1) x) (bound : ∀ 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 ∈ 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 ∈ 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 ∈ 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' g : ℝ → E} (derivf : ∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) (derivg : ∀ 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 [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [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.

@[instance 100]

instance Convex.instPathConnectedSpace {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] : PathConnectedSpace 𝕜

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} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {C : ℝ} {s : Set E} {x y : E} {f' : E → E →L[𝕜] G} (hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (bound : ∀ 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} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {s : Set E} {f' : E → E →L[𝕜] G} {C : NNReal} (hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (bound : ∀ 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} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [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 ∈ 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} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [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), ∃ 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} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {C : ℝ} {s : Set E} {x y : E} (hf : DifferentiableOn 𝕜 f s) (bound : ∀ 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} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {s : Set E} {C : NNReal} (hf : DifferentiableOn 𝕜 f s) (bound : ∀ 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} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {C : ℝ} {s : Set E} {x y : E} (hf : ∀ x ∈ s, DifferentiableAt 𝕜 f x) (bound : ∀ 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} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {s : Set E} {C : NNReal} (hf : ∀ x ∈ s, DifferentiableAt 𝕜 f x) (bound : ∀ 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} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [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} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {C : ℝ} {s : Set E} {x y : E} {f' : E → E →L[𝕜] G} {φ : E →L[𝕜] G} (hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (bound : ∀ 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} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {C : ℝ} {s : Set E} {x y : E} {φ : E →L[𝕜] G} (hf : DifferentiableOn 𝕜 f s) (bound : ∀ 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} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {C : ℝ} {s : Set E} {x y : E} {φ : E →L[𝕜] G} (hf : ∀ x ∈ s, DifferentiableAt 𝕜 f x) (bound : ∀ 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} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {s : Set E} {x y : E} (hs : Convex ℝ s) (hf : DifferentiableOn 𝕜 f s) (hf' : ∀ 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} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [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 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} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f g : E → G} {s : Set E} {x : E} (hs : Convex ℝ s) (hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s) (hs' : UniqueDiffOn 𝕜 s) (hf' : Set.EqOn (fderivWithin 𝕜 f s) (fderivWithin 𝕜 g s) s) (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 IsOpen.isOpen_inter_preimage_of_fderiv_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {s : Set E} (hs : IsOpen s) (hf : DifferentiableOn 𝕜 f s) (hf' : Set.EqOn (fderiv 𝕜 f) 0 s) (t : Set G) : IsOpen (s ∩ f ⁻¹' t)

If f has zero derivative on an open set, then f is locally constant on s.

theorem isLocallyConstant_of_fderiv_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} (h₁ : Differentiable 𝕜 f) (h₂ : ∀ (x : E), fderiv 𝕜 f x = 0) : IsLocallyConstant f

theorem IsOpen.exists_is_const_of_fderiv_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {s : Set E} (hs : IsOpen s) (hs' : IsPreconnected s) (hf : DifferentiableOn 𝕜 f s) (hf' : Set.EqOn (fderiv 𝕜 f) 0 s) : ∃ (a : G), ∀ x ∈ s, f x = a

If f has zero derivative on a connected open set, then f is constant on s.

theorem IsOpen.is_const_of_fderiv_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {s : Set E} (hs : IsOpen s) (hs' : IsPreconnected s) (hf : DifferentiableOn 𝕜 f s) (hf' : Set.EqOn (fderiv 𝕜 f) 0 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) : f x = f y

theorem IsOpen.exists_eq_add_of_fderiv_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f g : E → G} {s : Set E} (hs : IsOpen s) (hs' : IsPreconnected s) (hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s) (hf' : Set.EqOn (fderiv 𝕜 f) (fderiv 𝕜 g) s) : ∃ (a : G), Set.EqOn f (fun (x : E) => g x + a) s

theorem IsOpen.eqOn_of_fderiv_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f g : E → G} {s : Set E} {x : E} (hs : IsOpen s) (hs' : IsPreconnected s) (hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s) (hf' : ∀ x ∈ s, fderiv 𝕜 f x = fderiv 𝕜 g 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 connected open 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} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {E : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f 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.isLittleO_pow_succ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {s : Set E} {f' : E → E →L[𝕜] G} {x₀ : E} {n : ℕ} (hs : Convex ℝ s) (hx₀s : x₀ ∈ s) (hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf' : f' =o[nhdsWithin x₀ s] fun (x : E) => ‖x - x₀‖ ^ n) : (fun (x : E) => f x - f x₀) =o[nhdsWithin x₀ s] fun (x : E) => ‖x - x₀‖ ^ (n + 1)

theorem Convex.isLittleO_pow_succ_real {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f f' : ℝ → E} {x₀ : ℝ} {n : ℕ} {s : Set ℝ} (hs : Convex ℝ s) (hx₀s : x₀ ∈ s) (hff' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) (hf' : f' =o[nhdsWithin x₀ s] fun (x : ℝ) => (x - x₀) ^ n) : (fun (x : ℝ) => f x - f x₀) =o[nhdsWithin x₀ s] fun (x : ℝ) => (x - x₀) ^ (n + 1)

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

theorem IsOpen.isOpen_inter_preimage_of_deriv_eq_zero {𝕜 : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : 𝕜 → G} {s : Set 𝕜} (hs : IsOpen s) (hf : DifferentiableOn 𝕜 f s) (hf' : Set.EqOn (deriv f) 0 s) (t : Set G) : IsOpen (s ∩ f ⁻¹' t)

theorem IsOpen.exists_is_const_of_deriv_eq_zero {𝕜 : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : 𝕜 → G} {s : Set 𝕜} (hs : IsOpen s) (hs' : IsPreconnected s) (hf : DifferentiableOn 𝕜 f s) (hf' : Set.EqOn (deriv f) 0 s) : ∃ (a : G), ∀ x ∈ s, f x = a

theorem IsOpen.is_const_of_deriv_eq_zero {𝕜 : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : 𝕜 → G} {s : Set 𝕜} (hs : IsOpen s) (hs' : IsPreconnected s) (hf : DifferentiableOn 𝕜 f s) (hf' : Set.EqOn (deriv f) 0 s) {x y : 𝕜} (hx : x ∈ s) (hy : y ∈ s) : f x = f y

theorem IsOpen.exists_eq_add_of_deriv_eq {𝕜 : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set 𝕜} {f g : 𝕜 → G} (hs : IsOpen s) (hs' : IsPreconnected s) (hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s) (hf' : Set.EqOn (deriv f) (deriv g) s) : ∃ (a : G), Set.EqOn f (fun (x : 𝕜) => g x + a) s

theorem IsOpen.eqOn_of_deriv_eq {𝕜 : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set 𝕜} {x : 𝕜} {f g : 𝕜 → G} (hs : IsOpen s) (hs' : IsPreconnected s) (hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s) (hf' : Set.EqOn (deriv f) (deriv g) s) (hx : x ∈ s) (hfgx : f x = g x) : Set.EqOn f g s

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} [RCLike 𝕜] {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} [RCLike 𝕜] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f 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.