Differentiability

DefinitionDerivative at a point#

f has the derivative f' at the point x.

That is, f x' = f x + (x' - x) • f' + o(x' - x) where x' converges to x.

HasDerivAt.{u, v} {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F]
  [_root_.Module 𝕜 F] [TopologicalSpace F] [ContinuousSMul 𝕜 F] (f : 𝕜 → F) (f' : F) (x : 𝕜) : Prop
Sources
MathlibHasDerivAt
Uses 3 · Used by 27
Statement usesContinuous linear map · Metric space · Topological module
Used byEuler’s Summation of 1 + (1/2)^2 + (1/3)^2 + …. · The Area of a Circle · L’Hopital’s Rule · The Mean Value Theorem (Freek Wiedijk's 100 theorems) · Liouville theorem · Mean value theorem (Differentiability) · Local existence of integral curves · Uniqueness of integral curves · Darboux's theorem (analysis) · Fermat's theorem (stationary points) · Rademacher's theorem · Mellin inversion theorem · Morera's theorem · Euler's theorem on homogeneous functions · Change of variables to polar co-ordinates · Differentiability of integrals with respect to parameters · Partial derivatives commute · Taylor's theorem with integral form for remainder (Differential calculus) · Grönwall lemma · Log · Holomorphic stability under uniform convergence · Derivative of a composition of functions (Single Variable Real Analysis) · Leibniz formula (Single Variable Real Analysis) · Antiderivative of a continuous function · Change of variable · Integration by parts · Taylor's theorem with Lagrange form for remainder

TheoremDerivative of a composition of functions (Single Variable Real Analysis)#

Mathlib states this as deriv_comp.

deriv_comp.{u, u_1} {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) {𝕜' : Type u_1}
  [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'}
  (hh₂ : DifferentiableAt 𝕜' h₂ (h x)) (hh : DifferentiableAt 𝕜 h x) :
  deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x
Sources
Mathlibderiv_comp
Uses 6
Statement usesAssociative algebra over a commutative ring · Differentiable function between normed vector spaces · Differentials (linear tangent functions) · Normed vector space over a normed field
Proof usesDerivative at a point · Finite set

TheoremDerivative of the inverse of a function (Single Variable Real Analysis)#

If f (g y) = y for y in some neighborhood of a, g is continuous at a, and f has an invertible derivative f' at g a in the strict sense, then g has the derivative f'⁻¹ at a in the strict sense.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

HasStrictDerivAt.of_local_left_inverse.{u} {𝕜 : Type u} [NontriviallyNormedField 𝕜] {f g : 𝕜 → 𝕜}
  {f' a : 𝕜} (hg : ContinuousAt g a) (hf : HasStrictDerivAt f f' (g a)) (hf' : f' ≠ 0)
  (hfg : ∀ᶠ (y : 𝕜) in nhds a, f (g y) = y) : HasStrictDerivAt g f'⁻¹ a
Sources
MathlibHasStrictDerivAt.of_local_left_inverse
Uses 5 · Used by 1
Statement usesContinuous linear map · Finite set · Normed vector space over a normed field · Topological module
Proof usesTopological ring
Used byStirling’s Formula

DefinitionHigher-order derivatives of functions#

The n-th iterated derivative of a function from 𝕜 to F, as a function from 𝕜 to F.

iteratedDeriv.{u_1, u_2} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2}
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (x : 𝕜) : F
Sources
MathlibiteratedDeriv
Uses 4 · Used by 1
Statement usesDifferentials (linear tangent functions) · Finite set · Multilinear map · Normed vector space over a normed field
Used byLiouville theorem

TheoremLeibniz formula (Single Variable Real Analysis)#

Mathlib states this as deriv_mul.

deriv_mul.{u, u_3} {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [NormedRing 𝔸]
  [NormedAlgebra 𝕜 𝔸] {c d : 𝕜 → 𝔸} (hc : DifferentiableAt 𝕜 c x) (hd : DifferentiableAt 𝕜 d x) :
  deriv (c * d) x = deriv c x * d x + c x * deriv d x
Sources
Mathlibderiv_mul
Uses 7
Statement usesAssociative algebra over a commutative ring · Differentiable function between normed vector spaces · Differentials (linear tangent functions) · Normed vector space over a normed field
Proof usesDerivative at a point · Finite set · Topological ring

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.