# mathlib3documentation

analysis.calculus.deriv.slope

# Derivative as the limit of the slope #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we relate the derivative of a function with its definition from a standard undergraduate course as the limit of the slope (f y - f x) / (y - x) as y tends to 𝓝[≠] x. Since we are talking about functions taking values in a normed space instead of the base field, we use slope f x y = (y - x)⁻¹ • (f y - f x) instead of division.

We also prove some estimates on the upper/lower limits of the slope in terms of the derivative.

For a more detailed overview of one-dimensional derivatives in mathlib, see the module docstring of analysis/calculus/deriv/basic.

## Keywords #

derivative, slope

theorem has_deriv_at_filter_iff_tendsto_slope {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} {L : filter 𝕜} :
x L filter.tendsto (slope f x) (L (nhds f')

If the domain has dimension one, then Fréchet derivative is equivalent to the classical definition with a limit. In this version we have to take the limit along the subset -{x}, because for y=x the slope equals zero due to the convention 0⁻¹=0.

theorem has_deriv_within_at_iff_tendsto_slope {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} {s : set 𝕜} :
s x filter.tendsto (slope f x) (s \ {x})) (nhds f')
theorem has_deriv_within_at_iff_tendsto_slope' {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} {s : set 𝕜} (hs : x s) :
s x filter.tendsto (slope f x) s) (nhds f')
theorem has_deriv_at_iff_tendsto_slope {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} :
f' x filter.tendsto (slope f x) {x}) (nhds f')

### Upper estimates on liminf and limsup #

theorem has_deriv_within_at.limsup_slope_le {f : } {f' : } {s : set } {x r : } (hf : s x) (hr : f' < r) :
∀ᶠ (z : ) in (s \ {x}), x z < r
theorem has_deriv_within_at.limsup_slope_le' {f : } {f' : } {s : set } {x r : } (hf : s x) (hs : x s) (hr : f' < r) :
∀ᶠ (z : ) in s, x z < r
theorem has_deriv_within_at.liminf_right_slope_le {f : } {f' x r : } (hf : (set.Ici x) x) (hr : f' < r) :
∃ᶠ (z : ) in (set.Ioi x), x z < r
theorem has_deriv_within_at.limsup_norm_slope_le {E : Type u} [ E] {f : E} {f' : E} {s : set } {x r : } (hf : s x) (hr : f' < r) :
∀ᶠ (z : ) in s, z - x⁻¹ * f z - f x < r

If f has derivative f' within s at x, then for any r > ‖f'‖ the ratio ‖f z - f x‖ / ‖z - x‖ is less than r in some neighborhood of x within s. In other words, the limit superior of this ratio as z tends to x along s is less than or equal to ‖f'‖.

theorem has_deriv_within_at.limsup_slope_norm_le {E : Type u} [ E] {f : E} {f' : E} {s : set } {x r : } (hf : s x) (hr : f' < r) :
∀ᶠ (z : ) in s, z - x⁻¹ * (f z - f x) < r

If f has derivative f' within s at x, then for any r > ‖f'‖ the ratio (‖f z‖ - ‖f x‖) / ‖z - x‖ is less than r in some neighborhood of x within s. In other words, the limit superior of this ratio as z tends to x along s is less than or equal to ‖f'‖.

This lemma is a weaker version of has_deriv_within_at.limsup_norm_slope_le where ‖f z‖ - ‖f x‖ is replaced by ‖f z - f x‖.

theorem has_deriv_within_at.liminf_right_norm_slope_le {E : Type u} [ E] {f : E} {f' : E} {x r : } (hf : (set.Ici x) x) (hr : f' < r) :
∃ᶠ (z : ) in (set.Ioi x), z - x⁻¹ * f z - f x < r

If f has derivative f' within (x, +∞) at x, then for any r > ‖f'‖ the ratio ‖f z - f x‖ / ‖z - x‖ is frequently less than r as z → x+0. In other words, the limit inferior of this ratio as z tends to x+0 is less than or equal to ‖f'‖. See also has_deriv_within_at.limsup_norm_slope_le for a stronger version using limit superior and any set s.

theorem has_deriv_within_at.liminf_right_slope_norm_le {E : Type u} [ E] {f : E} {f' : E} {x r : } (hf : (set.Ici x) x) (hr : f' < r) :
∃ᶠ (z : ) in (set.Ioi x), (z - x)⁻¹ * (f z - f x) < r

If f has derivative f' within (x, +∞) at x, then for any r > ‖f'‖ the ratio (‖f z‖ - ‖f x‖) / (z - x) is frequently less than r as z → x+0. In other words, the limit inferior of this ratio as z tends to x+0 is less than or equal to ‖f'‖.

• has_deriv_within_at.limsup_norm_slope_le for a stronger version using limit superior and any set s;
• has_deriv_within_at.liminf_right_norm_slope_le for a stronger version using ‖f z - f x‖ instead of ‖f z‖ - ‖f x‖.