# 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} [NormedSpace π F] {f : π β F} {f' : F} {x : π} {L : Filter π} :

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} [NormedSpace π F] {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} [NormedSpace π F] {f : π β F} {f' : F} {x : π} {s : Set π} (hs : x β s) :
theorem hasDerivAt_iff_tendsto_slope {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} :
theorem hasDerivAt_iff_tendsto_slope_zero {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} :
HasDerivAt f f' x β Filter.Tendsto (fun (t : π) => β’ (f (x + t) - f x)) (nhdsWithin 0 {0}αΆ) (nhds f')
theorem HasDerivAt.tendsto_slope_zero {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} :
HasDerivAt f f' x β Filter.Tendsto (fun (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} [NormedSpace π F] {f : π β F} {f' : F} {x : π} [PartialOrder π] (h : HasDerivAt f f' x) :
Filter.Tendsto (fun (t : π) => β’ (f (x + t) - f x)) (nhdsWithin 0 ()) (nhds f')
theorem HasDerivAt.tendsto_slope_zero_left {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} [PartialOrder π] (h : HasDerivAt f f' x) :
Filter.Tendsto (fun (t : π) => β’ (f (x + t) - f x)) (nhdsWithin 0 ()) (nhds f')
theorem range_derivWithin_subset_closure_span_image {π : Type u} [] {F : Type v} [NormedSpace π F] (f : π β F) {s : Set π} {t : Set π} (h : s β closure (s β© t)) :
Set.range () β closure β(Submodule.span π (f '' 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} [NormedSpace π F] (f : π β F) {t : Set π} (h : ) :
Set.range () β closure β(Submodule.span π (f '' t))

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} [NormedSpace π F] (f : π β F) (s : Set π) :
theorem isSeparable_range_deriv {π : Type u} [] {F : Type v} [NormedSpace π F] (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β.