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 Mathlib/Analysis/Calculus/Deriv/Basic.lean.

Keywords

derivative, slope

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

theorem HasDerivAt.nonneg_of_monotoneOn_of_mem_nhds {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [OrderTopology 𝕜] {g : 𝕜 → 𝕜} {g' : 𝕜} (hd : HasDerivAt g g' x) {s : Set 𝕜} (hg : MonotoneOn g s) (hs : s ∈ nhds x) : 0 ≤ g'