Differentiability

DefinitionDifferentiable function between normed vector spaces#

A function f has the continuous linear map f' as derivative at x if f x' = f x + f' (x' - x) + o (x' - x) when x' tends to x.

HasFDerivAt.{u_1, u_2, u_3} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2}
  [AddCommGroup E] [_root_.Module 𝕜 E] [TopologicalSpace E] {F : Type u_3} [AddCommGroup F]
  [_root_.Module 𝕜 F] [TopologicalSpace F] (f : E → F) (f' : E →L[𝕜] F) (x : E) : Prop
Sources
MathlibHasFDerivAt
Uses 2 · Used by 29
Statement usesContinuous linear map · Metric space
Used byFundamental Theorem of Integral Calculus · Liouville’s Theorem and the Construction of Transcendental Numbers · L’Hopital’s Rule · The Mean Value Theorem (Freek Wiedijk's 100 theorems) · Maximum modulus principle · \(C^k\) function · Derivative of a composition of functions (Analysis) · Derivative of the inverse of a function (Analysis) · Leibniz formula (Analysis) · Local extrema · Mean value theorem (Differentiability) · Fundamental theorem of calculus, part 1 · Fundamental theorem of calculus, part 2 · Divergence theorem · Local existence of integral curves · Darboux's theorem (analysis) · Euler's theorem on homogeneous functions · Akra–Bazzi theorem · Whitney embedding theorem · Chain rule · Differentiable functions · Partial derivatives commute · Differentiability with respect to the complex variable · Cauchy formulas · Holomorphic stability under uniform convergence · Derivative of a composition of functions (Single Variable Real Analysis) · Leibniz formula (Single Variable Real Analysis) · Differentiability of the limit of a sequence of functions · Taylor's theorem with integral form for remainder (Taylor-like theorems)

TheoremDerivative of a composition of functions (Analysis)#

The chain rule.

HasFDerivAt.comp.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
  {G : Type u_4} [AddCommGroup G] [TopologicalSpace G] [_root_.Module 𝕜 G] [ContinuousAdd G]
  [ContinuousSMul 𝕜 G] {f : E → F} {f' : E →L[𝕜] F} (x : E) {g : F → G} {g' : F →L[𝕜] G}
  (hg : HasFDerivAt g g' (f x)) (hf : HasFDerivAt f f' x) : HasFDerivAt (g ∘ f) (g' ∘SL f') x
Sources
MathlibHasFDerivAt.comp
Uses 4 · Used by 7
Statement usesDifferentiable function between normed vector spaces · Normed vector space over a normed field · Topological module
Proof usesFinite set
Used byLeibniz formula (Analysis) · Regularization by convolution · Rademacher's theorem · Change of variables to polar co-ordinates · Chain rule · Taylor's theorem with integral form for remainder (Differential calculus) · Cauchy formulas

TheoremDerivative of the inverse of a function (Analysis)#

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

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

HasFDerivAt.of_local_left_inverse.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3}
  [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F]
  [NormedSpace 𝕜 F] {g : E → F} {f : F → E} {f' : F ≃L[𝕜] E} {a : E} (hg : ContinuousAt g a)
  (hf : HasFDerivAt f (↑f') (g a)) (hfg : ∀ᶠ (y : E) in nhds a, f (g y) = y) :
  HasFDerivAt g (↑f'.symm) a
Sources
MathlibHasFDerivAt.of_local_left_inverse
Uses 5
Statement usesDifferentiable function between normed vector spaces · Normed vector space over a normed field
Proof usesFinite set · Induced topology · Topological module

TheoremRolle's theorem#

Rolle's Theorem deriv version

exists_deriv_eq_zero {f : ℝ → ℝ} {a b : ℝ} (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b))
  (hfI : f a = f b) : ∃ c ∈ Set.Ioo a b, deriv f c = 0
Sources
Mathlibexists_deriv_eq_zero
Uses 4 · Used by 1
Statement usesDifferentials (linear tangent functions)
Proof usesExtreme value theorem · Fermat's theorem (stationary points) · Field \(\R\) of real numbers
Used byInsolvability of General Higher Degree Equations (Abel-Ruffini Theorem)

TheoremMean value theorem (Differentiability)#

Cauchy's Mean Value Theorem, deriv version.

exists_ratio_deriv_eq_ratio_slope (f : ℝ → ℝ) {a b : ℝ} (hab : a < b)
  (hfc : ContinuousOn f (Set.Icc a b)) (hfd : DifferentiableOn ℝ f (Set.Ioo a b)) (g : ℝ → ℝ)
  (hgc : ContinuousOn g (Set.Icc a b)) (hgd : DifferentiableOn ℝ g (Set.Ioo a b)) :
  ∃ c ∈ Set.Ioo a b, (g b - g a) * deriv f c = (f b - f a) * deriv g c
Sources
Mathlibexists_ratio_deriv_eq_ratio_slope
Uses 9
Statement usesDifferentials (linear tangent functions) · Holomorphic functions
Proof usesAssociative algebra over a commutative ring · Completeness · Derivative at a point · Differentiable function between normed vector spaces · Finite set · Normed vector space over a normed field · Topological ring

TheoremTaylor's theorem#

This file defines the Taylor polynomial of a real function f : ℝ → E, where E is a normed vector space over ℝ and proves Taylor's theorem, which states that if f is sufficiently smooth, then f can be approximated by the Taylor polynomial up to an explicit error term.

Mathlib covers this with the module Mathlib.Analysis.Calculus.Taylor rather than a single declaration.

Its 23 documented declarations include taylorCoeffWithin, taylorWithin, taylorWithinEval, taylor_within_zero_eval, taylorWithinEval_self, continuousOn_taylorWithinEval, monomial_has_deriv_aux, hasDerivWithinAt_taylorWithinEval, taylorWithinEval_hasDerivAt_Ioo, hasDerivWithinAt_taylorWithinEval_at_Icc, hasDerivAt_taylorWithinEval_succ, taylor_isLittleO, and 11 more.

Sources
MathlibtaylorCoeffWithin · taylorWithin · taylorWithinEval · taylor_within_zero_eval · taylorWithinEval_self · continuousOn_taylorWithinEval · monomial_has_deriv_aux · hasDerivWithinAt_taylorWithinEval · taylorWithinEval_hasDerivAt_Ioo · hasDerivWithinAt_taylorWithinEval_at_Icc · hasDerivAt_taylorWithinEval_succ · taylor_isLittleO

Definition\(C^k\) function#

A function is continuously differentiable up to n if it admits derivatives up to order n, which are continuous. Contrary to the case of definitions in domains (where derivatives might not be unique) we do not need to localize the definition in space or time. The parameter n belongs to ℕ∞ω (accessible in the ContDiff scope), i.e. it can be a natural number, ∞, or ω.

For n = ω, we require the function to be analytic. The precise definition we give (all the derivatives should be analytic) is more involved to work around issues when the space is not complete, but it is equivalent when the space is complete.

ContDiff.{u, uE, uF} (𝕜 : Type u) [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : WithTop ℕ∞)
  (f : E → F) : Prop
Sources
MathlibContDiff
Uses 3 · Used by 9
Statement usesAnalytic function · Differentiable function between normed vector spaces · Norm of a continuous linear map
Used bySchwartz space · Test functions · Regularization by convolution · Product of manifolds · Sphere · Closed interval · Discrete spaces are 0-manifolds · General linear group as a Lie group · Rademacher's theorem

TheoremLeibniz formula (Analysis)#

Mathlib states this as fderiv_mul.

fderiv_mul.{u_1, u_2, u_5} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {𝔸' : Type u_5} [NormedCommRing 𝔸']
  [NormedAlgebra 𝕜 𝔸'] {c d : E → 𝔸'} (hc : DifferentiableAt 𝕜 c x) (hd : DifferentiableAt 𝕜 d x) :
  fderiv 𝕜 (c * d) x = c x • fderiv 𝕜 d x + d x • fderiv 𝕜 c x
Sources
Mathlibfderiv_mul
Uses 9
Statement usesAssociative algebra over a commutative ring · Differentiable function between normed vector spaces · Differentials (linear tangent functions) · Normed vector space over a normed field · Topological ring
Proof usesDerivative of a composition of functions (Analysis) · Hausdorff space · Product of vector spaces · Topology on a normed vector space

TheoremLocal extrema#

Fermat's Theorem: the derivative of a function at a local minimum equals zero.

IsLocalMin.fderiv_eq_zero.{u} {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ}
  {a : E} (h : IsLocalMin f a) : fderiv ℝ f a = 0
Sources
MathlibIsLocalMin.fderiv_eq_zero
Uses 10 · Used by 1
Statement usesDifferentials (linear tangent functions) · Normed vector space over a normed field
Proof usesCluster point · Differentiable function between normed vector spaces · Dual of a normed space · Finite set · Order topology · Ordered ring · Topological module · Topological ring
Used byFermat's theorem (stationary points)

TheoremInverse function theorem (Differentiability)#

If f has an invertible derivative f' at a in the sense of strict differentiability (hf), then the inverse function hf.localInverse f has derivative f'.symm at f a.

HasStrictFDerivAt.to_localInverse.{u_1, u_2, u_3} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F]
  [NormedSpace 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} [CompleteSpace E]
  (hf : HasStrictFDerivAt f (↑f') a) :
  HasStrictFDerivAt (HasStrictFDerivAt.localInverse f f' a hf) (↑f'.symm) (f a)
Sources
MathlibHasStrictFDerivAt.to_localInverse
Uses 3 · Used by 1
Statement usesCompleteness · Continuous linear map · Normed vector space over a normed field
Used byInverse function theorem (Differential calculus)

DefinitionImplicit function theorem#

Implicit function theorem. If f : E → F and g : E → G are two maps strictly differentiable at a, their derivatives f', g' are surjective, and the kernels of these derivatives are complementary subspaces of E, then implicitFunction is the unique (germ of a) map φ : F → G → E such that f (φ y z) = y and g (φ y z) = z.

ImplicitFunctionData.implicitFunction.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1}
  [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [CompleteSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F]
  {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [CompleteSpace G]
  (φ : ImplicitFunctionData 𝕜 E F G) : F → G → E
Sources
MathlibImplicitFunctionData.implicitFunction
Uses 7
Statement usesCompleteness · Continuous linear map · Kernel of a linear map · Normed vector space over a normed field · Product of vector spaces · Range of a linear map · Sum of subspaces

DefinitionAnalytic function#

Given a function f : E → F, we say that f is analytic at x if it admits a convergent power series expansion around x.

AnalyticAt.{u_1, u_2, u_3} (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F)
  (x : E) : Prop
Sources
MathlibAnalyticAt
Uses 2 · Used by 8
Statement usesInfinite sum · Radius of convergence
Used byAnalyticity of holomorphic functions · First Main Theorem of Value Distribution Theory · Principle of analytic continuation · Principle of isolated zeros · Removable singularity · \(C^k\) function · Open mapping theorem (complex analysis) · Differentiability with respect to the complex variable

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.