One-dimensional derivatives #

This file defines the derivative of a function f : 𝕜 → F where 𝕜 is a normed field and F is a normed space over this field. The derivative of such a function f at a point x is given by an element f' : F.

The theory is developed analogously to the Fréchet derivatives. We first introduce predicates defined in terms of the corresponding predicates for Fréchet derivatives:

HasDerivAtFilter f f' x L states that the function f has the derivative f' at the point x as x goes along the filter L.
HasDerivWithinAt f f' s x states that the function f has the derivative f' at the point x within the subset s.
HasDerivAt f f' x states that the function f has the derivative f' at the point x.
HasStrictDerivAt f f' x states that the function f has the derivative f' at the point x in the sense of strict differentiability, i.e., f y - f z = (y - z) • f' + o (y - z) as y, z → x.

For the last two notions we also define a functional version:

derivWithin f s x is a derivative of f at x within s. If the derivative does not exist, then derivWithin f s x equals zero.
deriv f x is a derivative of f at x. If the derivative does not exist, then deriv f x equals zero.

The theorems fderivWithin_derivWithin and fderiv_deriv show that the one-dimensional derivatives coincide with the general Fréchet derivatives.

We also show the existence and compute the derivatives of:

constants
the identity function
linear maps (in Linear.lean)
addition (in Add.lean)
sum of finitely many functions (in Add.lean)
negation (in Add.lean)
subtraction (in Add.lean)
star (in Star.lean)
multiplication of two functions in 𝕜 → 𝕜 (in Mul.lean)
multiplication of a function in 𝕜 → 𝕜 and of a function in 𝕜 → E (in Mul.lean)
powers of a function (in Pow.lean and ZPow.lean)
inverse x → x⁻¹ (in Inv.lean)
division (in Inv.lean)
composition of a function in 𝕜 → F with a function in 𝕜 → 𝕜 (in Comp.lean)
composition of a function in F → E with a function in 𝕜 → F (in Comp.lean)
inverse function (assuming that it exists; the inverse function theorem is in Inverse.lean)
polynomials (in Polynomial.lean)

For most binary operations we also define const_op and op_const theorems for the cases when the first or second argument is a constant. This makes writing chains of HasDerivAt's easier, and they more frequently lead to the desired result.

We set up the simplifier so that it can compute the derivative of simple functions. For instance,

example (x : ℝ) :
    deriv (fun x ↦ cos (sin x) * exp x) x = (cos (sin x) - sin (sin x) * cos x) * exp x := by
  simp; ring

The relationship between the derivative of a function and its definition from a standard undergraduate course as the limit of the slope (f y - f x) / (y - x) as y tends to 𝓝[≠] x is developed in the file Slope.lean.

Implementation notes #

Most of the theorems are direct restatements of the corresponding theorems for Fréchet derivatives.

The strategy to construct simp lemmas that give the simplifier the possibility to compute derivatives is the same as the one for differentiability statements, as explained in FDeriv/Basic.lean. See the explanations there.

One-dimensional derivatives #

Implementation notes #

Congruence properties of derivatives #

Derivative of the identity #

Derivative of constant functions #

Continuity of a function admitting a derivative #