Documentation

Mathlib.Analysis.Calculus.MeanValue

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 : ContinuousOn f (Set.Icc a b)) (hf' : xSet.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' : xSet.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) (bound : xSet.Ico a b, f 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 : ContinuousOn f (Set.Icc a b)) (hf' : xSet.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 : xSet.Ico a b, f 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 : ContinuousOn f (Set.Icc a b)) {B : } {B' : } (ha : f a B a) (hB : ContinuousOn B (Set.Icc a b)) (hB' : xSet.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) (bound : xSet.Ico a b, ∀ (r : ), B' x < r∃ᶠ (z : ) in nhdsWithin x (Set.Ioi x), slope f x z < 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 : ContinuousOn f (Set.Icc a b)) (hf' : xSet.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' : xSet.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) (bound : xSet.Ico a b, f 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 : ContinuousOn f (Set.Icc a b)) (hf' : xSet.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 : xSet.Ico a b, f 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 : ContinuousOn f (Set.Icc a b)) (hf' : xSet.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' : xSet.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) (bound : xSet.Ico a b, f' 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_3} [NormedAddCommGroup E] {f : E} {f' : } (hf : ContinuousOn f (Set.Icc a b)) (hf' : xSet.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' : xSet.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) (bound : xSet.Ico a b, f 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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {a : } {b : } {f' : E} (hf : ContinuousOn f (Set.Icc a b)) (hf' : xSet.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' : xSet.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) (bound : xSet.Ico a b, f 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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {a : } {b : } {f' : E} (hf : ContinuousOn f (Set.Icc a b)) (hf' : xSet.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 : xSet.Ico a b, f 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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {a : } {b : } {f' : E} (hf : ContinuousOn f (Set.Icc a b)) (hf' : xSet.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' : xSet.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) (bound : xSet.Ico a b, f' 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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {a : } {b : } {f' : E} (hf : ContinuousOn f (Set.Icc a b)) (hf' : xSet.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 : xSet.Ico a b, f' 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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {a : } {b : } {f' : E} {C : } (hf : ContinuousOn f (Set.Icc a b)) (hf' : xSet.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) (bound : xSet.Ico a b, f' 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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {a : } {b : } {f' : E} {C : } (hf : xSet.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x) (bound : xSet.Ico a b, f' 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), 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 : xSet.Ico a b, derivWithin 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), 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 : xSet.Icc 0 1, HasDerivWithinAt f (f' x) (Set.Icc 0 1) x) (bound : xSet.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 : xSet.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 : xSet.Ico a b, HasDerivWithinAt f 0 (Set.Ici x) x) (x : ) :
x Set.Icc a bf 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 : xSet.Ico a b, derivWithin f (Set.Icc a b) x = 0) (x : ) :
x Set.Icc a bf 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 : xSet.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) (derivg : xSet.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 bf 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 bf 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 : EG} {C : } {s : Set E} {x : E} {y : E} {f' : EE →L[𝕜] G} (hf : xs, HasFDerivWithinAt f (f' x) s x) (bound : xs, 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 : EG} {s : Set E} {f' : EE →L[𝕜] G} {C : NNReal} (hf : xs, HasFDerivWithinAt f (f' x) s x) (bound : xs, f' x‖₊ C) (hs : Convex 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' : EE →L[𝕜] G} (hs : Convex s) {f : EG} (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} [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {x : E} {f' : EE →L[𝕜] G} (hs : Convex s) {f : EG} (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} [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : EG} {C : } {s : Set E} {x : E} {y : E} (hf : DifferentiableOn 𝕜 f s) (bound : xs, 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 : EG} {s : Set E} {C : NNReal} (hf : DifferentiableOn 𝕜 f s) (bound : xs, fderivWithin 𝕜 f s x‖₊ C) (hs : Convex 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 : EG} {C : } {s : Set E} {x : E} {y : E} (hf : xs, DifferentiableAt 𝕜 f x) (bound : xs, 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 : EG} {s : Set E} {C : NNReal} (hf : xs, DifferentiableAt 𝕜 f x) (bound : xs, fderiv 𝕜 f x‖₊ C) (hs : Convex 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 : EG} {C : NNReal} (hf : Differentiable 𝕜 f) (bound : ∀ (x : E), fderiv 𝕜 f x‖₊ C) :

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 : EG} {C : } {s : Set E} {x : E} {y : E} {f' : EE →L[𝕜] G} {φ : E →L[𝕜] G} (hf : xs, HasFDerivWithinAt f (f' x) s x) (bound : xs, 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 : EG} {C : } {s : Set E} {x : E} {y : E} {φ : E →L[𝕜] G} (hf : DifferentiableOn 𝕜 f s) (bound : xs, 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 : EG} {C : } {s : Set E} {x : E} {y : E} {φ : E →L[𝕜] G} (hf : xs, DifferentiableAt 𝕜 f x) (bound : xs, 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 : EG} {s : Set E} {x : E} {y : E} (hs : Convex s) (hf : DifferentiableOn 𝕜 f s) (hf' : xs, 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 : EG} (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 : EG} {g : EG} {s : Set E} {x : E} (hs : Convex s) (hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s) (hs' : UniqueDiffOn 𝕜 s) (hf' : xs, 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 : EG} {g : EG} (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 : xs, HasDerivWithinAt f (f' x) s x) (bound : xs, 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 : xs, HasDerivWithinAt f (f' x) s x) (bound : xs, f' x‖₊ C) :

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 : xs, 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 : xs, derivWithin f s x‖₊ C) :

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 : xs, DifferentiableAt 𝕜 f x) (bound : xs, 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 : xs, DifferentiableAt 𝕜 f x) (bound : xs, deriv f x‖₊ C) (hs : Convex 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) :

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' : xSet.Ioo a b, HasDerivAt f (f' x) x) (g : ) (g' : ) (hgc : ContinuousOn g (Set.Icc a b)) (hgg' : xSet.Ioo a b, HasDerivAt g (g' x) x) :
∃ 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' : xSet.Ioo a b, HasDerivAt f (f' x) x) (hgg' : xSet.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 ∈ 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' : xSet.Ioo a b, HasDerivAt f (f' x) x) :
∃ 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 ∈ 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 ∈ 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 ∈ 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 : } (hf'_gt : xinterior D, C < deriv f x) (x : ) :
x DyD, x < yC * (y - x) < f y - f x

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

theorem mul_sub_lt_image_sub_of_lt_deriv {f : } (hf : Differentiable f) {C : } (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 : } (hf'_ge : xinterior D, C deriv f x) (x : ) :
x DyD, x yC * (y - x) f y - f x

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

theorem mul_sub_le_image_sub_of_le_deriv {f : } (hf : Differentiable f) {C : } (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 : } (lt_hf' : xinterior 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 : } (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 : } (le_hf' : xinterior 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 : } (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 strictMonoOn_of_deriv_pos {D : Set } (hD : Convex D) {f : } (hf : ContinuousOn f D) (hf' : xinterior D, 0 < deriv 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 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) :

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 strictMonoOn_of_hasDerivWithinAt_pos {D : Set } (hD : Convex D) {f : } {f' : } (hf : ContinuousOn f D) (hf' : xinterior D, HasDerivWithinAt f (f' x) (interior D) x) (hf'₀ : xinterior D, 0 < 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 strictly positive, then f is a strictly monotone function on D.

@[deprecated strictMonoOn_of_hasDerivWithinAt_pos]
theorem StrictMonoOn_of_hasDerivWithinAt_pos {D : Set } (hD : Convex D) {f : } {f' : } (hf : ContinuousOn f D) (hf' : xinterior D, HasDerivWithinAt f (f' x) (interior D) x) (hf'₀ : xinterior D, 0 < f' x) :

Alias of strictMonoOn_of_hasDerivWithinAt_pos.


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 strictly positive, then f is a strictly monotone function on D.

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

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

theorem monotoneOn_of_deriv_nonneg {D : Set } (hD : Convex D) {f : } (hf : ContinuousOn f D) (hf' : DifferentiableOn f (interior D)) (hf'_nonneg : xinterior D, 0 deriv 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 nonnegative, then f is a monotone function on D.

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

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

theorem monotoneOn_of_hasDerivWithinAt_nonneg {D : Set } (hD : Convex D) {f : } {f' : } (hf : ContinuousOn f D) (hf' : xinterior D, HasDerivWithinAt f (f' x) (interior D) x) (hf'₀ : xinterior D, 0 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 nonnegative, then f is a monotone function on D.

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

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

theorem strictAntiOn_of_deriv_neg {D : Set } (hD : Convex D) {f : } (hf : ContinuousOn f D) (hf' : xinterior D, deriv f x < 0) :

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

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

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

theorem strictAntiOn_of_hasDerivWithinAt_neg {D : Set } (hD : Convex D) {f : } {f' : } (hf : ContinuousOn f D) (hf' : xinterior D, HasDerivWithinAt f (f' x) (interior D) x) (hf'₀ : xinterior D, f' x < 0) :

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

@[deprecated strictAntiOn_of_hasDerivWithinAt_neg]
theorem StrictAntiOn_of_hasDerivWithinAt_pos {D : Set } (hD : Convex D) {f : } {f' : } (hf : ContinuousOn f D) (hf' : xinterior D, HasDerivWithinAt f (f' x) (interior D) x) (hf'₀ : xinterior D, f' x < 0) :

Alias of strictAntiOn_of_hasDerivWithinAt_neg.


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 strictly positive, then f is a strictly monotone function on D.

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

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

@[deprecated strictAnti_of_hasDerivAt_neg]
theorem strictAnti_of_hasDerivAt_pos {f : } {f' : } (hf : ∀ (x : ), HasDerivAt f (f' x) x) (hf' : ∀ (x : ), f' x < 0) :

Alias of strictAnti_of_hasDerivAt_neg.


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

theorem antitoneOn_of_deriv_nonpos {D : Set } (hD : Convex D) {f : } (hf : ContinuousOn f D) (hf' : DifferentiableOn f (interior D)) (hf'_nonpos : xinterior D, deriv f x 0) :

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

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

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

theorem antitoneOn_of_hasDerivWithinAt_nonpos {D : Set } (hD : Convex D) {f : } {f' : } (hf : ContinuousOn f D) (hf' : xinterior D, HasDerivWithinAt f (f' x) (interior D) x) (hf'₀ : xinterior D, f' x 0) :

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

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

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

Functions f : E → ℝ #

theorem domain_mvt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {s : Set E} {x : E} {y : E} {f' : EE →L[] } (hf : xs, HasFDerivWithinAt f (f' x) s x) (hs : Convex s) (xs : x s) (ys : y s) :
∃ 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 : GH} {f' : GG →L[𝕜] H} {x : G} (hder : ∀ᶠ (y : G) in nhds x, HasFDerivAt f (f' y) y) (hcont : ContinuousAt f' 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.