Differential calculus

DefinitionDifferentials (linear tangent functions)#

If f has a derivative at x, then fderiv 𝕜 f x is such a derivative. Otherwise, it is set to 0.

fderiv.{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) (x : E) : E →L[𝕜] F
Sources
Mathlibfderiv
Uses 2 · Used by 26
Statement usesContinuous linear map · Metric space
Used byLiouville’s Theorem and the Construction of Transcendental Numbers · L’Hopital’s Rule · The Mean Value Theorem (Freek Wiedijk's 100 theorems) · Cauchy integral formula · Principle of isolated zeros · Characterization of convexity · Leibniz formula (Analysis) · Local extrema · Mean value theorem (Differentiability) · Rolle's theorem · Schwartz space · Regularization by convolution · Darboux's theorem (analysis) · Fermat's theorem (stationary points) · Akra–Bazzi theorem · Chain rule · Directional derivative · Gradient vector · Taylor's theorem with integral form for remainder (Differential calculus) · Cauchy formulas · Holomorphic stability under uniform convergence · Derivative of a composition of functions (Single Variable Real Analysis) · Higher-order derivatives of functions · Leibniz formula (Single Variable Real Analysis) · Antiderivative of a continuous function · Taylor's theorem with integral form for remainder (Taylor-like theorems)

DefinitionDirectional derivative#

Line derivative of f at the point x in the direction v, if it exists. Zero otherwise.

If the line derivative exists (i.e., ∃ f', HasLineDerivAt 𝕜 f f' x v), then f (x + t v) = f x + t lineDeriv 𝕜 f x v + o (t) when t tends to 0.

lineDeriv.{u_1, u_2, u_3} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {F : Type u_2}
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [_root_.Module 𝕜 E]
  (f : E → F) (x v : E) : F
Sources
MathliblineDeriv
Uses 2 · Used by 1
Statement usesDifferentials (linear tangent functions) · Normed vector space over a normed field
Used byRademacher's theorem

DefinitionGradient vector#

Gradient of f at the point x, if it exists. Zero otherwise. Denoted as ∇ within the Gradient namespace.

If the derivative exists (i.e., ∃ f', HasGradientAt f f' x), then f x' = f x + ⟨f', x' - x⟩ + o (x' - x) where x' converges to x.

gradient.{u_1, u_2} {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F]
  [InnerProductSpace 𝕜 F] [CompleteSpace F] (f : F → 𝕜) (x : F) : F
Sources
Mathlibgradient
Uses 2
Statement usesDifferentials (linear tangent functions) · Fréchet-Riesz representation of the dual of a Hilbert space

TheoremChain rule#

Mathlib states this as fderiv_comp.

fderiv_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} (x : E) [T2Space G] {g : F → G} (hg : DifferentiableAt 𝕜 g (f x))
  (hf : DifferentiableAt 𝕜 f x) : fderiv 𝕜 (g ∘ f) x = fderiv 𝕜 g (f x) ∘SL fderiv 𝕜 f x
Sources
Mathlibfderiv_comp
Uses 6
Statement usesDifferentiable function between normed vector spaces · Differentials (linear tangent functions) · Hausdorff space · Normed vector space over a normed field · Topological module
Proof usesDerivative of a composition of functions (Analysis)

DefinitionDifferentiable functions#

Differentiable 𝕜 f means that f is differentiable at any point.

Differentiable.{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) : Prop
Sources
MathlibDifferentiable
Uses 1 · Used by 6
Statement usesDifferentiable function between normed vector spaces
Used byLiouville theorem · \(\C\) is algebraically closed · Rademacher's theorem · Taylor's theorem with integral form for remainder (Differential calculus) · Cauchy formulas · Differentiability of the sum of a series of functions

TheoremPartial derivatives commute#

If a function is differentiable, and has two derivatives at x, then the second derivative is symmetric.

second_derivative_symmetric.{u_1, u_2, u_3} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
  {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F]
  [NormedSpace 𝕜 F] {f : E → F} [IsRCLikeNormedField 𝕜] {f' : E → E →L[𝕜] F}
  {f'' : E →L[𝕜] E →L[𝕜] F} {x : E} (hf : ∀ (y : E), HasFDerivAt f (f' y) y)
  (hx : HasFDerivAt f' f'' x) (v w : E) : (f'' v) w = (f'' w) v
Sources
Mathlibsecond_derivative_symmetric
Uses 14
Statement usesAssociative algebra over a commutative ring · Completeness · Differentiable function between normed vector spaces · Normed vector space over a normed field
Proof usesCharacteristic zero · Convex subsets · Derivative at a point · Finite set · Hausdorff space · Order topology · The Triangle Inequality · Topological ring · Topology of a metric space · Topology on a normed vector space

TheoremTaylor's theorem with integral form for remainder (Differential calculus)#

Taylor's theorem with remainder in integral form. If f is n + 1 times continuously differentiable, then f (x + y) is given by ∑ k in 0..n, D^k f(x; y,..,y) / k! + 1/n! ∫ t in 0..1, (1 - t) ^ n • D^{n+1}f (x + t • y; y,..,y), where D^k f denotes the iterated derivative of f.

In the case that n = 1, this is a reformulation of the fundamental theorem of calculus, namely f (x + y) = f x + ∫ t in 0..1, D f(x + t • y; y).

map_add_eq_sum_add_integral_iteratedFDeriv.{u_2, u_3} {E : Type u_2} {F : Type u_3}
  [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] {f : E → F}
  {x y : E} {n : ℕ} [CompleteSpace F]
  (hf : ∀ t ∈ Set.Icc 0 1, ContDiffAt ℝ (↑n + 1) f (x + t • y)) :
  f (x + y) =
    (∑ k ∈ Finset.range (n + 1), (↑k.factorial)⁻¹ • (iteratedFDeriv ℝ k f x) fun x => y) +
      (↑n.factorial)⁻¹ •
        ∫ (t : ℝ) in 0..1, (1 - t) ^ n • (iteratedFDeriv ℝ (n + 1) f (x + t • y)) fun x => y
Sources
Mathlibmap_add_eq_sum_add_integral_iteratedFDeriv
Uses 12
Statement usesBochner integral · Carathéodory's theorem (measure theory) · Differentials (linear tangent functions) · Lebesgue measure (Measures and integral calculus) · Radius of convergence
Proof usesCharacteristic p · Characteristic zero · Derivative at a point · Derivative of a composition of functions (Analysis) · Differentiable functions · Fundamental theorem of calculus, part 2 · Topology on a normed vector space

StructureDiffeomorphisms#

A G-diffeomorphism between two charted spaces is a homeomorphism which, when read in the charts, belongs to G. We avoid the word diffeomorph as it is too related to the smooth category, and use structomorph instead.

Structomorph.{u, u_5, u_6} {H : Type u} [TopologicalSpace H] (G : StructureGroupoid H)
  (M : Type u_5) (M' : Type u_6) [TopologicalSpace M] [TopologicalSpace M'] [ChartedSpace H M]
  [ChartedSpace H M'] : Type (max u_5 u_6)
Sources
MathlibStructomorph
Uses 2
Statement usesHomeomorphisms · Limit of a map with respect to filters

TheoremInverse function theorem (Differential calculus)#

Mathlib states this as HasStrictDerivAt.to_localInverse.

HasStrictDerivAt.to_localInverse.{u_1} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
  {f : 𝕜 → 𝕜} {f' a : 𝕜} (hf : HasStrictDerivAt f f' a) (hf' : f' ≠ 0) :
  HasStrictDerivAt (HasStrictDerivAt.localInverse f f' a hf hf') f'⁻¹ (f a)
Sources
MathlibHasStrictDerivAt.to_localInverse
Uses 7
Statement usesCompleteness · Continuous linear map · Finite set · Normed vector space over a normed field · Topological module · Topological ring
Proof usesInverse function theorem (Differentiability)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.