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

source

theorem has_deriv_at_filter_iff_tendsto_slope {𝕜 : Type u} [nontrivially_normed_field 𝕜] {F : Type v} [normed_add_comm_group F] [normed_space 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {L : filter 𝕜} :

has_deriv_at_filter f f' x L ↔ filter.tendsto (slope f x) (L ⊓ filter.principal {x}ᶜ) (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.

source

theorem has_deriv_within_at_iff_tendsto_slope {𝕜 : Type u} [nontrivially_normed_field 𝕜] {F : Type v} [normed_add_comm_group F] [normed_space 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : set 𝕜} :

has_deriv_within_at f f' s x ↔ filter.tendsto (slope f x) (nhds_within x (s \ {x})) (nhds f')

source

theorem has_deriv_within_at_iff_tendsto_slope' {𝕜 : Type u} [nontrivially_normed_field 𝕜] {F : Type v} [normed_add_comm_group F] [normed_space 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : set 𝕜} (hs : x ∉ s) :

has_deriv_within_at f f' s x ↔ filter.tendsto (slope f x) (nhds_within x s) (nhds f')

source

theorem has_deriv_at_iff_tendsto_slope {𝕜 : Type u} [nontrivially_normed_field 𝕜] {F : Type v} [normed_add_comm_group F] [normed_space 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} :

has_deriv_at f f' x ↔ filter.tendsto (slope f x) (nhds_within x {x}ᶜ) (nhds f')

Upper estimates on liminf and limsup #

source

theorem has_deriv_within_at.limsup_slope_le {f : ℝ → ℝ} {f' : ℝ} {s : set ℝ} {x r : ℝ} (hf : has_deriv_within_at f f' s x) (hr : f' < r) :

∀ᶠ (z : ℝ) in nhds_within x (s \ {x}), slope f x z < r

source

theorem has_deriv_within_at.limsup_slope_le' {f : ℝ → ℝ} {f' : ℝ} {s : set ℝ} {x r : ℝ} (hf : has_deriv_within_at f f' s x) (hs : x ∉ s) (hr : f' < r) :

∀ᶠ (z : ℝ) in nhds_within x s, slope f x z < r

source

theorem has_deriv_within_at.liminf_right_slope_le {f : ℝ → ℝ} {f' x r : ℝ} (hf : has_deriv_within_at f f' (set.Ici x) x) (hr : f' < r) :

∃ᶠ (z : ℝ) in nhds_within x (set.Ioi x), slope f x z < r

source

theorem has_deriv_within_at.limsup_norm_slope_le {E : Type u} [normed_add_comm_group E] [normed_space ℝ E] {f : ℝ → E} {f' : E} {s : set ℝ} {x r : ℝ} (hf : has_deriv_within_at f f' s x) (hr : ‖f'‖ < r) :

∀ᶠ (z : ℝ) in nhds_within x 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'‖.

source

theorem has_deriv_within_at.limsup_slope_norm_le {E : Type u} [normed_add_comm_group E] [normed_space ℝ E] {f : ℝ → E} {f' : E} {s : set ℝ} {x r : ℝ} (hf : has_deriv_within_at f f' s x) (hr : ‖f'‖ < r) :

∀ᶠ (z : ℝ) in nhds_within x 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‖.

source

theorem has_deriv_within_at.liminf_right_norm_slope_le {E : Type u} [normed_add_comm_group E] [normed_space ℝ E] {f : ℝ → E} {f' : E} {x r : ℝ} (hf : has_deriv_within_at f f' (set.Ici x) x) (hr : ‖f'‖ < r) :

∃ᶠ (z : ℝ) in nhds_within x (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.

source

theorem has_deriv_within_at.liminf_right_slope_norm_le {E : Type u} [normed_add_comm_group E] [normed_space ℝ E] {f : ℝ → E} {f' : E} {x r : ℝ} (hf : has_deriv_within_at f f' (set.Ici x) x) (hr : ‖f'‖ < r) :

∃ᶠ (z : ℝ) in nhds_within x (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'‖.