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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {L : Filter 𝕜} : HasDerivAtFilter 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.

theorem hasDerivWithinAt_iff_tendsto_slope {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜} (hs : x ∉ s) : HasDerivWithinAt f f' s x ↔ Filter.Tendsto (slope f x) (nhdsWithin x s) (nhds f')

theorem hasDerivAt_iff_tendsto_slope {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} : HasDerivAt f f' x ↔ Filter.Tendsto (slope f x) (nhdsWithin x {x}ᶜ) (nhds f')

theorem hasDerivAt_iff_tendsto_slope_left_right {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} [LinearOrder 𝕜] : HasDerivAt f f' x ↔ Filter.Tendsto (slope f x) (nhdsWithin x (Set.Iio x)) (nhds f') ∧ Filter.Tendsto (slope f x) (nhdsWithin x (Set.Ioi x)) (nhds f')

theorem hasDerivAt_iff_tendsto_slope_zero {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} : HasDerivAt f f' x → Filter.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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} [Preorder 𝕜] (h : HasDerivAt f f' x) : Filter.Tendsto (fun (t : 𝕜) => t⁻¹ • (f (x + t) - f x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds f')

theorem HasDerivAt.tendsto_slope_zero_left {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} [Preorder 𝕜] (h : HasDerivAt f f' x) : Filter.Tendsto (fun (t : 𝕜) => t⁻¹ • (f (x + t) - f x)) (nhdsWithin 0 (Set.Iio 0)) (nhds f')

theorem range_derivWithin_subset_closure_span_image {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : 𝕜 → F) {s t : Set 𝕜} (h : s ⊆ closure (s ∩ t)) : Set.range (derivWithin f s) ⊆ 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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : 𝕜 → F) {t : Set 𝕜} (h : Dense t) : Set.range (deriv f) ⊆ 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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace.SeparableSpace 𝕜] (f : 𝕜 → F) (s : Set 𝕜) : TopologicalSpace.IsSeparable (Set.range (derivWithin f s))

theorem isSeparable_range_deriv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace.SeparableSpace 𝕜] (f : 𝕜 → F) : TopologicalSpace.IsSeparable (Set.range (deriv f))

theorem HasDerivAt.continuousAt_div {𝕜 : Type u} [NontriviallyNormedField 𝕜] [DecidableEq 𝕜] {f : 𝕜 → 𝕜} {c a : 𝕜} (hf : HasDerivAt f a c) : ContinuousAt (Function.update (fun (x : 𝕜) => (f x - f c) / (x - c)) c a) c

theorem HasDerivWithinAt.nonneg_of_monotoneOn {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [OrderTopology 𝕜] {g : 𝕜 → 𝕜} {g' : 𝕜} (hx : AccPt x (Filter.principal s)) (hd : HasDerivWithinAt g g' s x) (hg : MonotoneOn g s) : 0 ≤ g'

If a monotone function has a derivative within a set at a non-isolated point, then this derivative is nonnegative.

theorem MonotoneOn.derivWithin_nonneg {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [OrderTopology 𝕜] {g : 𝕜 → 𝕜} (hg : MonotoneOn g s) : 0 ≤ derivWithin g s x

The derivative within a set of a monotone function is nonnegative.

theorem HasDerivAt.nonneg_of_monotone {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [OrderTopology 𝕜] {g : 𝕜 → 𝕜} {g' : 𝕜} (hd : HasDerivAt g g' x) (hg : Monotone g) : 0 ≤ g'

If a monotone function has a derivative, then this derivative is nonnegative.

theorem Monotone.deriv_nonneg {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [OrderTopology 𝕜] {g : 𝕜 → 𝕜} (hg : Monotone g) : 0 ≤ deriv g x

The derivative of a monotone function is nonnegative.

theorem HasDerivWithinAt.nonpos_of_antitoneOn {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [OrderTopology 𝕜] {g : 𝕜 → 𝕜} {g' : 𝕜} (hx : AccPt x (Filter.principal s)) (hd : HasDerivWithinAt g g' s x) (hg : AntitoneOn g s) : g' ≤ 0

If an antitone function has a derivative within a set at a non-isolated point, then this derivative is nonpositive.

theorem AntitoneOn.derivWithin_nonpos {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [OrderTopology 𝕜] {g : 𝕜 → 𝕜} (hg : AntitoneOn g s) : derivWithin g s x ≤ 0

The derivative within a set of an antitone function is nonpositive.

theorem HasDerivAt.nonpos_of_antitone {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [OrderTopology 𝕜] {g : 𝕜 → 𝕜} {g' : 𝕜} (hd : HasDerivAt g g' x) (hg : Antitone g) : g' ≤ 0

If an antitone function has a derivative, then this derivative is nonpositive.

theorem Antitone.deriv_nonpos {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [OrderTopology 𝕜] {g : 𝕜 → 𝕜} (hg : Antitone g) : deriv g x ≤ 0

The derivative of an antitone function is nonpositive.

Upper estimates on liminf and limsup

theorem HasDerivWithinAt.limsup_slope_le {f : ℝ → ℝ} {f' : ℝ} {s : Set ℝ} {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 : Set ℝ} {x r : ℝ} (hf : HasDerivWithinAt f f' s x) (hs : x ∉ s) (hr : f' < r) : ∀ᶠ (z : ℝ) in nhdsWithin x s, slope f x z < r

theorem HasDerivWithinAt.liminf_right_slope_le {f : ℝ → ℝ} {f' x r : ℝ} (hf : HasDerivWithinAt f f' (Set.Ici x) x) (hr : f' < r) : ∃ᶠ (z : ℝ) in nhdsWithin x (Set.Ioi x), slope f x z < r

theorem HasDerivWithinAt.limsup_norm_slope_le {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {f' : E} {s : Set ℝ} {x r : ℝ} (hf : HasDerivWithinAt f f' s x) (hr : ‖f'‖ < r) : ∀ᶠ (z : ℝ) in nhdsWithin 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'‖.

theorem HasDerivWithinAt.limsup_slope_norm_le {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {f' : E} {s : Set ℝ} {x r : ℝ} (hf : HasDerivWithinAt f f' s x) (hr : ‖f'‖ < r) : ∀ᶠ (z : ℝ) in nhdsWithin 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 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} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {f' : E} {x r : ℝ} (hf : HasDerivWithinAt f f' (Set.Ici x) x) (hr : ‖f'‖ < r) : ∃ᶠ (z : ℝ) in nhdsWithin 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 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} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {f' : E} {x r : ℝ} (hf : HasDerivWithinAt f f' (Set.Ici x) x) (hr : ‖f'‖ < r) : ∃ᶠ (z : ℝ) in nhdsWithin 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

• 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‖.