5.2. Further details🔗

5.2.1. Local issues🔗

Differentiation is a local operation and this is reflected in Mathlib's API. For example the Differentiable definition comes in four flavours:

DifferentiableAt: asks whether a function is differentiable at a single point
Differentiable: asks whether a function is differentiable everywhere
DifferentiableWithinAt: asks whether a function is differentiable at a point within a subset
DifferentiableOn: asks whether a function is differentiable everywhere within a subset

In addition HasDerivAt and deriv have variants HasDerivWithinAt and derivWithin.

5.2.2. Coefficients🔗

Mathlib's theory of differential calculus supports quite general coefficients including the reals, the complex numbers, and the p-adic numbers. For example here is the statement that deriv and HasDerivAt are mutually compatible for a map of the p-adics:

example (p : ℕ) [Fact p.Prime] (f : ℚ_[p] → ℚ_[p])
    (h : Differentiable ℚ_[p] f) (x : ℚ_[p]) :
    HasDerivAt f (deriv f x) x :=
  (h x).hasDerivAt

5.2.3. Differentiability classes🔗

The definitions ContDiffAt, ContDiff, ContDiffWithinAt, ContDiffOn can be used to express continuous differentiability to any order. Note that these definitions consume an order parameter of type WithTop ℕ∞ and this allows discussion of all finite orders as well as the smooth and analytic orders:

open scoped ContDiff
variable (k : ℕ)
ContDiff ℝ (↑k) f : Prop#check ContDiff ℝ k f -- k-times continuously differentiable
ContDiff ℝ ∞ f : Prop#check ContDiff ℝ ∞ f -- smooth
ContDiff ℝ ω f : Prop#check ContDiff ℝ ω f -- analytic

5.2.4. Fréchet derivatives🔗

Mathlib has support for multivariable differential calculus via the Fréchet derivative, providing an extensive theory of differential calculus for maps between any two normed spaces (not necessarily finite-dimensional). The ContDiff and Differentiable definitions (and their API) apply quite generally but for general domains one needs to use:

HasFDerivAt rather than HasDerivAt
HasFDerivWithinAt rather than HasDerivWithinAt
fderiv rather than deriv
fderivWithin rather than derivWithin