# Documentation

Mathlib.Analysis.Calculus.Deriv.Slope

# Derivative as the limit of the slope #

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 hasDerivAtFilter_iff_tendsto_slope {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} {L : } :
HasDerivAtFilter f f' 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 hasDerivWithinAt_iff_tendsto_slope {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} {s : Set 𝕜} :
HasDerivWithinAt f f' s x Filter.Tendsto (slope f x) (nhdsWithin x (s \ {x})) (nhds f')
theorem hasDerivWithinAt_iff_tendsto_slope' {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} {s : Set 𝕜} (hs : ¬x s) :
theorem hasDerivAt_iff_tendsto_slope {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} :
theorem hasDerivAt_iff_tendsto_slope_zero {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} :
HasDerivAt f f' x Filter.Tendsto (fun t => t⁻¹ (f (x + t) - f x)) (nhdsWithin 0 {0}) (nhds f')
theorem HasDerivAt.tendsto_slope_zero {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} :
HasDerivAt f f' xFilter.Tendsto (fun t => t⁻¹ (f (x + t) - f x)) (nhdsWithin 0 {0}) (nhds f')

Alias of the forward direction of hasDerivAt_iff_tendsto_slope_zero.

theorem HasDerivAt.tendsto_slope_zero_right {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} [] (h : HasDerivAt f f' x) :
Filter.Tendsto (fun t => t⁻¹ (f (x + t) - f x)) (nhdsWithin 0 ()) (nhds f')
theorem HasDerivAt.tendsto_slope_zero_left {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} [] (h : HasDerivAt f f' x) :
Filter.Tendsto (fun t => t⁻¹ (f (x + t) - f x)) (nhdsWithin 0 ()) (nhds f')
theorem range_derivWithin_subset_closure_span_image {𝕜 : Type u} {F : Type v} [] (f : 𝕜F) {s : Set 𝕜} {t : Set 𝕜} (h : s closure (s t)) :

Given a set t such that s ∩ t is dense in s, then the range of derivWithin f s is contained in the closure of the submodule spanned by the image of t.

theorem range_deriv_subset_closure_span_image {𝕜 : Type u} {F : Type v} [] (f : 𝕜F) {t : Set 𝕜} (h : ) :

Given a dense set t, then the range of deriv f is contained in the closure of the submodule spanned by the image of t.

theorem isSeparable_range_derivWithin {𝕜 : Type u} {F : Type v} [] (f : 𝕜F) (s : Set 𝕜) :
theorem isSeparable_range_deriv {𝕜 : Type u} {F : Type v} [] (f : 𝕜F) :

### Upper estimates on liminf and limsup #

theorem HasDerivWithinAt.limsup_slope_le {f : } {f' : } {s : } {x : } {r : } (hf : HasDerivWithinAt f f' s x) (hr : f' < r) :
∀ᶠ (z : ) in nhdsWithin x (s \ {x}), slope f x z < r
theorem HasDerivWithinAt.limsup_slope_le' {f : } {f' : } {s : } {x : } {r : } (hf : HasDerivWithinAt f f' s x) (hs : ¬x s) (hr : f' < r) :
∀ᶠ (z : ) in , slope f x z < r
theorem HasDerivWithinAt.liminf_right_slope_le {f : } {f' : } {x : } {r : } (hf : HasDerivWithinAt f f' () x) (hr : f' < r) :
∃ᶠ (z : ) in nhdsWithin x (), slope f x z < r
theorem HasDerivWithinAt.limsup_norm_slope_le {E : Type u} [] {f : E} {f' : E} {s : } {x : } {r : } (hf : HasDerivWithinAt f f' s x) (hr : f' < r) :
∀ᶠ (z : ) in , 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 HasDerivWithinAt.limsup_slope_norm_le {E : Type u} [] {f : E} {f' : E} {s : } {x : } {r : } (hf : HasDerivWithinAt f f' s x) (hr : f' < r) :
∀ᶠ (z : ) in , 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 HasDerivWithinAt.limsup_norm_slope_le where ‖f z‖ - ‖f x‖ is replaced by ‖f z - f x‖.

theorem HasDerivWithinAt.liminf_right_norm_slope_le {E : Type u} [] {f : E} {f' : E} {x : } {r : } (hf : HasDerivWithinAt f f' () x) (hr : f' < r) :
∃ᶠ (z : ) in nhdsWithin 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 HasDerivWithinAt.limsup_norm_slope_le for a stronger version using limit superior and any set s.

theorem HasDerivWithinAt.liminf_right_slope_norm_le {E : Type u} [] {f : E} {f' : E} {x : } {r : } (hf : HasDerivWithinAt f f' () x) (hr : f' < r) :
∃ᶠ (z : ) in nhdsWithin 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'‖.

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