# The Fréchet derivative #

Let E and F be normed spaces, f : E → F, and f' : E →L[𝕜] F a continuous 𝕜-linear map, where 𝕜 is a non-discrete normed field. Then

HasFDerivWithinAt f f' s x

says that f has derivative f' at x, where the domain of interest is restricted to s. We also have

HasFDerivAt f f' x := HasFDerivWithinAt f f' x univ

Finally,

HasStrictFDerivAt f f' x

means that f : E → F has derivative f' : E →L[𝕜] F in the sense of strict differentiability, i.e., f y - f z - f'(y - z) = o(y - z) as y, z → x. This notion is used in the inverse function theorem, and is defined here only to avoid proving theorems like IsBoundedBilinearMap.hasFDerivAt twice: first for HasFDerivAt, then for HasStrictFDerivAt.

## Main results #

In addition to the definition and basic properties of the derivative, the folder Analysis/Calculus/FDeriv/ contains the usual formulas (and existence assertions) for the derivative of

• constants
• the identity
• bounded linear maps (Linear.lean)
• bounded bilinear maps (Bilinear.lean)
• sum of two functions (Add.lean)
• sum of finitely many functions (Add.lean)
• multiplication of a function by a scalar constant (Add.lean)
• negative of a function (Add.lean)
• subtraction of two functions (Add.lean)
• multiplication of a function by a scalar function (Mul.lean)
• multiplication of two scalar functions (Mul.lean)
• composition of functions (the chain rule) (Comp.lean)
• inverse function (Mul.lean) (assuming that it exists; the inverse function theorem is in ../Inverse.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.

One can also interpret the derivative of a function f : 𝕜 → E as an element of E (by identifying a linear function from 𝕜 to E with its value at 1). Results on the Fréchet derivative are translated to this more elementary point of view on the derivative in the file Deriv.lean. The derivative of polynomials is handled there, as it is naturally one-dimensional.

The simplifier is set up to prove automatically that some functions are differentiable, or differentiable at a point (but not differentiable on a set or within a set at a point, as checking automatically that the good domains are mapped one to the other when using composition is not something the simplifier can easily do). This means that one can write example (x : ℝ) : Differentiable ℝ (fun x ↦ sin (exp (3 + x^2)) - 5 * cos x) := by simp. If there are divisions, one needs to supply to the simplifier proofs that the denominators do not vanish, as in

example (x : ℝ) (h : 1 + sin x ≠ 0) : DifferentiableAt ℝ (fun x ↦ exp x / (1 + sin x)) x := by
simp [h]


Of course, these examples only work once exp, cos and sin have been shown to be differentiable, in Analysis.SpecialFunctions.Trigonometric.

The simplifier is not set up to compute the Fréchet derivative of maps (as these are in general complicated multidimensional linear maps), but it will compute one-dimensional derivatives, see Deriv.lean.

## Implementation details #

The derivative is defined in terms of the isLittleO relation, but also characterized in terms of the Tendsto relation.

We also introduce predicates DifferentiableWithinAt 𝕜 f s x (where 𝕜 is the base field, f the function to be differentiated, x the point at which the derivative is asserted to exist, and s the set along which the derivative is defined), as well as DifferentiableAt 𝕜 f x, DifferentiableOn 𝕜 f s and Differentiable 𝕜 f to express the existence of a derivative.

To be able to compute with derivatives, we write fderivWithin 𝕜 f s x and fderiv 𝕜 f x for some choice of a derivative if it exists, and the zero function otherwise. This choice only behaves well along sets for which the derivative is unique, i.e., those for which the tangent directions span a dense subset of the whole space. The predicates UniqueDiffWithinAt s x and UniqueDiffOn s, defined in TangentCone.lean express this property. We prove that indeed they imply the uniqueness of the derivative. This is satisfied for open subsets, and in particular for univ. This uniqueness only holds when the field is non-discrete, which we request at the very beginning: otherwise, a derivative can be defined, but it has no interesting properties whatsoever.

To make sure that the simplifier can prove automatically that functions are differentiable, we tag many lemmas with the simp attribute, for instance those saying that the sum of differentiable functions is differentiable, as well as their product, their cartesian product, and so on. A notable exception is the chain rule: we do not mark as a simp lemma the fact that, if f and g are differentiable, then their composition also is: simp would always be able to match this lemma, by taking f or g to be the identity. Instead, for every reasonable function (say, exp), we add a lemma that if f is differentiable then so is (fun x ↦ exp (f x)). This means adding some boilerplate lemmas, but these can also be useful in their own right.

Tests for this ability of the simplifier (with more examples) are provided in Tests/Differentiable.lean.

## Tags #

derivative, differentiable, Fréchet, calculus

theorem hasFDerivAtFilter_iff_isLittleO {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] (f : EF) (f' : E →L[𝕜] F) (x : E) (L : ) :
HasFDerivAtFilter f f' x L (fun (x' : E) => f x' - f x - f' (x' - x)) =o[L] fun (x' : E) => x' - x
structure HasFDerivAtFilter {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] (f : EF) (f' : E →L[𝕜] F) (x : E) (L : ) :

A function f has the continuous linear map f' as derivative along the filter L if f x' = f x + f' (x' - x) + o (x' - x) when x' converges along the filter L. This definition is designed to be specialized for L = 𝓝 x (in HasFDerivAt), giving rise to the usual notion of Fréchet derivative, and for L = 𝓝[s] x (in HasFDerivWithinAt), giving rise to the notion of Fréchet derivative along the set s.

• of_isLittleO :: (
• isLittleO : (fun (x' : E) => f x' - f x - f' (x' - x)) =o[L] fun (x' : E) => x' - x
• )
Instances For
theorem HasFDerivAtFilter.isLittleO {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {L : } (self : HasFDerivAtFilter f f' x L) :
(fun (x' : E) => f x' - f x - f' (x' - x)) =o[L] fun (x' : E) => x' - x
def HasFDerivWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] (f : EF) (f' : E →L[𝕜] F) (s : Set E) (x : E) :

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

Equations
Instances For
def HasFDerivAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] (f : EF) (f' : E →L[𝕜] F) (x : E) :

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.

Equations
Instances For
def HasStrictFDerivAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] (f : EF) (f' : E →L[𝕜] F) (x : E) :

A function f has derivative f' at a in the sense of strict differentiability if f x - f y - f' (x - y) = o(x - y) as x, y → a. This form of differentiability is required, e.g., by the inverse function theorem. Any C^1 function on a vector space over ℝ is strictly differentiable but this definition works, e.g., for vector spaces over p-adic numbers.

Equations
• = (fun (p : E × E) => f p.1 - f p.2 - f' (p.1 - p.2)) =o[nhds (x, x)] fun (p : E × E) => p.1 - p.2
Instances For
def DifferentiableWithinAt (𝕜 : Type u_1) {E : Type u_2} [] {F : Type u_3} [] (f : EF) (s : Set E) (x : E) :

A function f is differentiable at a point x within a set s if it admits a derivative there (possibly non-unique).

Equations
Instances For
def DifferentiableAt (𝕜 : Type u_1) {E : Type u_2} [] {F : Type u_3} [] (f : EF) (x : E) :

A function f is differentiable at a point x if it admits a derivative there (possibly non-unique).

Equations
Instances For
@[irreducible]
def fderivWithin (𝕜 : Type u_6) {E : Type u_7} [] {F : Type u_8} [] (f : EF) (s : Set E) (x : E) :
E →L[𝕜] F

If f has a derivative at x within s, then fderivWithin 𝕜 f s x is such a derivative. Otherwise, it is set to 0. If x is isolated in s, we take the derivative within s to be zero for convenience.

Equations
Instances For
theorem fderivWithin_def (𝕜 : Type u_6) {E : Type u_7} [] {F : Type u_8} [] (f : EF) (s : Set E) (x : E) :
fderivWithin 𝕜 f s x = if nhdsWithin x (s \ {x}) = then 0 else if h : ∃ (f' : E →L[𝕜] F), HasFDerivWithinAt f f' s x then else 0
theorem fderiv_def (𝕜 : Type u_6) {E : Type u_7} [] {F : Type u_8} [] (f : EF) (x : E) :
fderiv 𝕜 f x = if h : ∃ (f' : E →L[𝕜] F), HasFDerivAt f f' x then else 0
@[irreducible]
def fderiv (𝕜 : Type u_6) {E : Type u_7} [] {F : Type u_8} [] (f : EF) (x : E) :
E →L[𝕜] F

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

Equations
Instances For
def DifferentiableOn (𝕜 : Type u_1) {E : Type u_2} [] {F : Type u_3} [] (f : EF) (s : Set E) :

DifferentiableOn 𝕜 f s means that f is differentiable within s at any point of s.

Equations
• = xs,
Instances For
def Differentiable (𝕜 : Type u_1) {E : Type u_2} [] {F : Type u_3} [] (f : EF) :

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

Equations
• = ∀ (x : E),
Instances For
theorem fderivWithin_zero_of_isolated {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} (h : nhdsWithin x (s \ {x}) = ) :
fderivWithin 𝕜 f s x = 0
theorem fderivWithin_zero_of_nmem_closure {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} (h : x) :
fderivWithin 𝕜 f s x = 0
theorem fderivWithin_zero_of_not_differentiableWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} (h : ¬) :
fderivWithin 𝕜 f s x = 0
theorem fderiv_zero_of_not_differentiableAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} (h : ¬) :
fderiv 𝕜 f x = 0
theorem HasFDerivWithinAt.lim {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} (h : HasFDerivWithinAt f f' s x) {α : Type u_6} (l : ) {c : α𝕜} {d : αE} {v : E} (dtop : ∀ᶠ (n : α) in l, x + d n s) (clim : Filter.Tendsto (fun (n : α) => c n) l Filter.atTop) (cdlim : Filter.Tendsto (fun (n : α) => c n d n) l (nhds v)) :
Filter.Tendsto (fun (n : α) => c n (f (x + d n) - f x)) l (nhds (f' v))

If a function f has a derivative f' at x, a rescaled version of f around x converges to f', i.e., n (f (x + (1/n) v) - f x) converges to f' v. More generally, if c n tends to infinity and c n * d n tends to v, then c n * (f (x + d n) - f x) tends to f' v. This lemma expresses this fact, for functions having a derivative within a set. Its specific formulation is useful for tangent cone related discussions.

theorem HasFDerivWithinAt.unique_on {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {f₁' : E →L[𝕜] F} {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt f f₁' s x) :
Set.EqOn (f') (f₁') ()

If f' and f₁' are two derivatives of f within s at x, then they are equal on the tangent cone to s at x

theorem UniqueDiffWithinAt.eq {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {f₁' : E →L[𝕜] F} {x : E} {s : Set E} (H : ) (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt f f₁' s x) :
f' = f₁'

UniqueDiffWithinAt achieves its goal: it implies the uniqueness of the derivative.

theorem UniqueDiffOn.eq {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {f₁' : E →L[𝕜] F} {x : E} {s : Set E} (H : ) (hx : x s) (h : HasFDerivWithinAt f f' s x) (h₁ : HasFDerivWithinAt f f₁' s x) :
f' = f₁'

### Basic properties of the derivative #

theorem hasFDerivAtFilter_iff_tendsto {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {L : } :
HasFDerivAtFilter f f' x L Filter.Tendsto (fun (x' : E) => x' - x⁻¹ * f x' - f x - f' (x' - x)) L (nhds 0)
theorem hasFDerivWithinAt_iff_tendsto {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} :
HasFDerivWithinAt f f' s x Filter.Tendsto (fun (x' : E) => x' - x⁻¹ * f x' - f x - f' (x' - x)) () (nhds 0)
theorem hasFDerivAt_iff_tendsto {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} :
HasFDerivAt f f' x Filter.Tendsto (fun (x' : E) => x' - x⁻¹ * f x' - f x - f' (x' - x)) (nhds x) (nhds 0)
theorem hasFDerivAt_iff_isLittleO_nhds_zero {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} :
HasFDerivAt f f' x (fun (h : E) => f (x + h) - f x - f' h) =o[nhds 0] fun (h : E) => h
theorem HasFDerivAt.le_of_lip' {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x₀ : E} (hf : HasFDerivAt f f' x₀) {C : } (hC₀ : 0 C) (hlip : ∀ᶠ (x : E) in nhds x₀, f x - f x₀ C * x - x₀) :

Converse to the mean value inequality: if f is differentiable at x₀ and C-lipschitz on a neighborhood of x₀ then its derivative at x₀ has norm bounded by C. This version only assumes that ‖f x - f x₀‖ ≤ C * ‖x - x₀‖ in a neighborhood of x.

theorem HasFDerivAt.le_of_lipschitzOn {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x₀ : E} (hf : HasFDerivAt f f' x₀) {s : Set E} (hs : s nhds x₀) {C : NNReal} (hlip : ) :
f' C

Converse to the mean value inequality: if f is differentiable at x₀ and C-lipschitz on a neighborhood of x₀ then its derivative at x₀ has norm bounded by C.

theorem HasFDerivAt.le_of_lipschitz {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x₀ : E} (hf : HasFDerivAt f f' x₀) {C : NNReal} (hlip : ) :
f' C

Converse to the mean value inequality: if f is differentiable at x₀ and C-lipschitz then its derivative at x₀ has norm bounded by C.

theorem HasFDerivAtFilter.mono {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {L₁ : } {L₂ : } (h : HasFDerivAtFilter f f' x L₂) (hst : L₁ L₂) :
HasFDerivAtFilter f f' x L₁
theorem HasFDerivWithinAt.mono_of_mem {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} {t : Set E} (h : HasFDerivWithinAt f f' t x) (hst : t ) :
theorem HasFDerivWithinAt.mono {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} {t : Set E} (h : HasFDerivWithinAt f f' t x) (hst : s t) :
theorem HasFDerivAt.hasFDerivAtFilter {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {L : } (h : HasFDerivAt f f' x) (hL : L nhds x) :
theorem HasFDerivAt.hasFDerivWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} (h : HasFDerivAt f f' x) :
theorem HasFDerivWithinAt.differentiableWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} (h : HasFDerivWithinAt f f' s x) :
theorem HasFDerivAt.differentiableAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} (h : HasFDerivAt f f' x) :
@[simp]
theorem hasFDerivWithinAt_univ {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} :
HasFDerivWithinAt f f' Set.univ x HasFDerivAt f f' x
theorem HasFDerivWithinAt.hasFDerivAt_of_univ {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} :
HasFDerivWithinAt f f' Set.univ xHasFDerivAt f f' x

Alias of the forward direction of hasFDerivWithinAt_univ.

theorem hasFDerivWithinAt_of_mem_nhds {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} (h : s nhds x) :
theorem hasFDerivWithinAt_of_isOpen {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} (h : ) (hx : x s) :
theorem hasFDerivWithinAt_insert {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} {y : E} :
theorem HasFDerivWithinAt.of_insert {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} {y : E} :
HasFDerivWithinAt f f' (insert y s) xHasFDerivWithinAt f f' s x

Alias of the forward direction of hasFDerivWithinAt_insert.

theorem HasFDerivWithinAt.insert' {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} {y : E} :
HasFDerivWithinAt f f' s xHasFDerivWithinAt f f' (insert y s) x

Alias of the reverse direction of hasFDerivWithinAt_insert.

theorem HasFDerivWithinAt.insert {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {g : EF} {g' : E →L[𝕜] F} {x : E} {s : Set E} (h : HasFDerivWithinAt g g' s x) :
theorem hasFDerivWithinAt_diff_singleton {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} (y : E) :
HasFDerivWithinAt f f' (s \ {y}) x HasFDerivWithinAt f f' s x
theorem HasStrictFDerivAt.isBigO_sub {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} (hf : ) :
(fun (p : E × E) => f p.1 - f p.2) =O[nhds (x, x)] fun (p : E × E) => p.1 - p.2
theorem HasFDerivAtFilter.isBigO_sub {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {L : } (h : HasFDerivAtFilter f f' x L) :
(fun (x' : E) => f x' - f x) =O[L] fun (x' : E) => x' - x
theorem HasStrictFDerivAt.hasFDerivAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} (hf : ) :
theorem HasStrictFDerivAt.differentiableAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} (hf : ) :
theorem HasStrictFDerivAt.exists_lipschitzOnWith_of_nnnorm_lt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} (hf : ) (K : NNReal) (hK : f'‖₊ < K) :
snhds x,

If f is strictly differentiable at x with derivative f' and K > ‖f'‖₊, then f is K-Lipschitz in a neighborhood of x.

theorem HasStrictFDerivAt.exists_lipschitzOnWith {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} (hf : ) :
∃ (K : NNReal), snhds x,

If f is strictly differentiable at x with derivative f', then f is Lipschitz in a neighborhood of x. See also HasStrictFDerivAt.exists_lipschitzOnWith_of_nnnorm_lt for a more precise statement.

theorem HasFDerivAt.lim {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} (hf : HasFDerivAt f f' x) (v : E) {α : Type u_6} {c : α𝕜} {l : } (hc : Filter.Tendsto (fun (n : α) => c n) l Filter.atTop) :
Filter.Tendsto (fun (n : α) => c n (f (x + (c n)⁻¹ v) - f x)) l (nhds (f' v))

Directional derivative agrees with HasFDeriv.

theorem HasFDerivAt.unique {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f₀' : E →L[𝕜] F} {f₁' : E →L[𝕜] F} {x : E} (h₀ : HasFDerivAt f f₀' x) (h₁ : HasFDerivAt f f₁' x) :
f₀' = f₁'
theorem hasFDerivWithinAt_inter' {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} {t : Set E} (h : t ) :
theorem hasFDerivWithinAt_inter {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} {t : Set E} (h : t nhds x) :
theorem HasFDerivWithinAt.union {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} {t : Set E} (hs : HasFDerivWithinAt f f' s x) (ht : HasFDerivWithinAt f f' t x) :
HasFDerivWithinAt f f' (s t) x
theorem HasFDerivWithinAt.hasFDerivAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} (h : HasFDerivWithinAt f f' s x) (hs : s nhds x) :
theorem DifferentiableWithinAt.differentiableAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} (h : ) (hs : s nhds x) :
theorem HasFDerivWithinAt.of_nhdsWithin_eq_bot {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} (h : nhdsWithin x (s \ {x}) = ) :

If x is isolated in s, then f has any derivative at x within s, as this statement is empty.

theorem hasFDerivWithinAt_of_nmem_closure {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} (h : x) :

If x is not in the closure of s, then f has any derivative at x within s, as this statement is empty.

theorem DifferentiableWithinAt.hasFDerivWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} (h : ) :
HasFDerivWithinAt f (fderivWithin 𝕜 f s x) s x
theorem DifferentiableAt.hasFDerivAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} (h : ) :
HasFDerivAt f (fderiv 𝕜 f x) x
theorem DifferentiableOn.hasFDerivAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} (h : ) (hs : s nhds x) :
HasFDerivAt f (fderiv 𝕜 f x) x
theorem DifferentiableOn.differentiableAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} (h : ) (hs : s nhds x) :
theorem DifferentiableOn.eventually_differentiableAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} (h : ) (hs : s nhds x) :
∀ᶠ (y : E) in nhds x,
theorem HasFDerivAt.fderiv {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} (h : HasFDerivAt f f' x) :
fderiv 𝕜 f x = f'
theorem fderiv_eq {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : EE →L[𝕜] F} (h : ∀ (x : E), HasFDerivAt f (f' x) x) :
fderiv 𝕜 f = f'
theorem norm_fderiv_le_of_lip' (𝕜 : Type u_1) {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x₀ : E} {C : } (hC₀ : 0 C) (hlip : ∀ᶠ (x : E) in nhds x₀, f x - f x₀ C * x - x₀) :
fderiv 𝕜 f x₀ C

Converse to the mean value inequality: if f is C-lipschitz on a neighborhood of x₀ then its derivative at x₀ has norm bounded by C. This version only assumes that ‖f x - f x₀‖ ≤ C * ‖x - x₀‖ in a neighborhood of x.

theorem norm_fderiv_le_of_lipschitzOn (𝕜 : Type u_1) {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x₀ : E} {s : Set E} (hs : s nhds x₀) {C : NNReal} (hlip : ) :
fderiv 𝕜 f x₀ C

Converse to the mean value inequality: if f is C-lipschitz on a neighborhood of x₀ then its derivative at x₀ has norm bounded by C. Version using fderiv.

theorem norm_fderiv_le_of_lipschitz (𝕜 : Type u_1) {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x₀ : E} {C : NNReal} (hlip : ) :
fderiv 𝕜 f x₀ C

Converse to the mean value inequality: if f is C-lipschitz then its derivative at x₀ has norm bounded by C. Version using fderiv.

theorem HasFDerivWithinAt.fderivWithin {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} (h : HasFDerivWithinAt f f' s x) (hxs : ) :
fderivWithin 𝕜 f s x = f'
theorem DifferentiableWithinAt.mono {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} {t : Set E} (h : ) (st : s t) :
theorem DifferentiableWithinAt.mono_of_mem {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} (h : ) {t : Set E} (hst : s ) :
theorem differentiableWithinAt_univ {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} :
DifferentiableWithinAt 𝕜 f Set.univ x
theorem differentiableWithinAt_inter {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} {t : Set E} (ht : t nhds x) :
theorem differentiableWithinAt_inter' {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} {t : Set E} (ht : t ) :
theorem DifferentiableAt.differentiableWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} (h : ) :
theorem Differentiable.differentiableAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} (h : ) :
theorem DifferentiableAt.fderivWithin {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} (h : ) (hxs : ) :
fderivWithin 𝕜 f s x = fderiv 𝕜 f x
theorem DifferentiableOn.mono {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {s : Set E} {t : Set E} (h : ) (st : s t) :
theorem differentiableOn_univ {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} :
DifferentiableOn 𝕜 f Set.univ
theorem Differentiable.differentiableOn {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {s : Set E} (h : ) :
theorem differentiableOn_of_locally_differentiableOn {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {s : Set E} (h : xs, ∃ (u : Set E), x u DifferentiableOn 𝕜 f (s u)) :
theorem fderivWithin_of_mem {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} {t : Set E} (st : t ) (ht : ) (h : ) :
fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x
theorem fderivWithin_subset {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} {t : Set E} (st : s t) (ht : ) (h : ) :
fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x
theorem fderivWithin_inter {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} {t : Set E} (ht : t nhds x) :
fderivWithin 𝕜 f (s t) x = fderivWithin 𝕜 f s x
@[simp]
theorem fderivWithin_univ {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} :
fderivWithin 𝕜 f Set.univ = fderiv 𝕜 f
theorem fderivWithin_of_mem_nhds {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} (h : s nhds x) :
fderivWithin 𝕜 f s x = fderiv 𝕜 f x
theorem fderivWithin_of_isOpen {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} (hs : ) (hx : x s) :
fderivWithin 𝕜 f s x = fderiv 𝕜 f x
theorem fderivWithin_eq_fderiv {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} (hs : ) (h : ) :
fderivWithin 𝕜 f s x = fderiv 𝕜 f x
theorem fderiv_mem_iff {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {s : Set (E →L[𝕜] F)} {x : E} :
fderiv 𝕜 f x s fderiv 𝕜 f x s ¬ 0 s
theorem fderivWithin_mem_iff {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {t : Set E} {s : Set (E →L[𝕜] F)} {x : E} :
fderivWithin 𝕜 f t x s fderivWithin 𝕜 f t x s ¬ 0 s
theorem Asymptotics.IsBigO.hasFDerivWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {s : Set E} {x₀ : E} {n : } (h : f =O[nhdsWithin x₀ s] fun (x : E) => x - x₀ ^ n) (hx₀ : x₀ s) (hn : 1 < n) :
theorem Asymptotics.IsBigO.hasFDerivAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x₀ : E} {n : } (h : f =O[nhds x₀] fun (x : E) => x - x₀ ^ n) (hn : 1 < n) :
HasFDerivAt f 0 x₀
theorem HasFDerivWithinAt.isBigO_sub {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {s : Set E} {x₀ : E} {f' : E →L[𝕜] F} (h : HasFDerivWithinAt f f' s x₀) :
(fun (x : E) => f x - f x₀) =O[nhdsWithin x₀ s] fun (x : E) => x - x₀
theorem DifferentiableWithinAt.isBigO_sub {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {s : Set E} {x₀ : E} (h : ) :
(fun (x : E) => f x - f x₀) =O[nhdsWithin x₀ s] fun (x : E) => x - x₀
theorem HasFDerivAt.isBigO_sub {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x₀ : E} {f' : E →L[𝕜] F} (h : HasFDerivAt f f' x₀) :
(fun (x : E) => f x - f x₀) =O[nhds x₀] fun (x : E) => x - x₀
theorem DifferentiableAt.isBigO_sub {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x₀ : E} (h : DifferentiableAt 𝕜 f x₀) :
(fun (x : E) => f x - f x₀) =O[nhds x₀] fun (x : E) => x - x₀

### Deducing continuity from differentiability #

theorem HasFDerivAtFilter.tendsto_nhds {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {L : } (hL : L nhds x) (h : HasFDerivAtFilter f f' x L) :
Filter.Tendsto f L (nhds (f x))
theorem HasFDerivWithinAt.continuousWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} (h : HasFDerivWithinAt f f' s x) :
theorem HasFDerivAt.continuousAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} (h : HasFDerivAt f f' x) :
theorem DifferentiableWithinAt.continuousWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} (h : ) :
theorem DifferentiableAt.continuousAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} (h : ) :
theorem DifferentiableOn.continuousOn {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {s : Set E} (h : ) :
theorem Differentiable.continuous {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} (h : ) :
theorem HasStrictFDerivAt.continuousAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} (hf : ) :
theorem HasStrictFDerivAt.isBigO_sub_rev {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {f' : E ≃L[𝕜] F} (hf : HasStrictFDerivAt f (f') x) :
(fun (p : E × E) => p.1 - p.2) =O[nhds (x, x)] fun (p : E × E) => f p.1 - f p.2
theorem HasFDerivAtFilter.isBigO_sub_rev {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {L : } (hf : HasFDerivAtFilter f f' x L) {C : NNReal} (hf' : ) :
(fun (x' : E) => x' - x) =O[L] fun (x' : E) => f x' - f x

### congr properties of the derivative #

theorem hasFDerivWithinAt_congr_set' {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} {t : Set E} (y : E) (h : s =ᶠ[nhdsWithin x {y}] t) :
theorem hasFDerivWithinAt_congr_set {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} {t : Set E} (h : s =ᶠ[nhds x] t) :
theorem differentiableWithinAt_congr_set' {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} {t : Set E} (y : E) (h : s =ᶠ[nhdsWithin x {y}] t) :
theorem differentiableWithinAt_congr_set {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} {t : Set E} (h : s =ᶠ[nhds x] t) :
theorem fderivWithin_congr_set' {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} {t : Set E} (y : E) (h : s =ᶠ[nhdsWithin x {y}] t) :
fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x
theorem fderivWithin_congr_set {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} {t : Set E} (h : s =ᶠ[nhds x] t) :
fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x
theorem fderivWithin_eventually_congr_set' {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} {t : Set E} (y : E) (h : s =ᶠ[nhdsWithin x {y}] t) :
theorem fderivWithin_eventually_congr_set {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} {s : Set E} {t : Set E} (h : s =ᶠ[nhds x] t) :
theorem Filter.EventuallyEq.hasStrictFDerivAt_iff {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f₀ : EF} {f₁ : EF} {f₀' : E →L[𝕜] F} {f₁' : E →L[𝕜] F} {x : E} (h : f₀ =ᶠ[nhds x] f₁) (h' : ∀ (y : E), f₀' y = f₁' y) :
HasStrictFDerivAt f₀ f₀' x HasStrictFDerivAt f₁ f₁' x
theorem HasStrictFDerivAt.congr_fderiv {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {g' : E →L[𝕜] F} {x : E} (h : ) (h' : f' = g') :
theorem HasFDerivAt.congr_fderiv {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {g' : E →L[𝕜] F} {x : E} (h : HasFDerivAt f f' x) (h' : f' = g') :
theorem HasFDerivWithinAt.congr_fderiv {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f' : E →L[𝕜] F} {g' : E →L[𝕜] F} {x : E} {s : Set E} (h : HasFDerivWithinAt f f' s x) (h' : f' = g') :
theorem HasStrictFDerivAt.congr_of_eventuallyEq {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f₁ : EF} {f' : E →L[𝕜] F} {x : E} (h : ) (h₁ : f =ᶠ[nhds x] f₁) :
theorem Filter.EventuallyEq.hasFDerivAtFilter_iff {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f₀ : EF} {f₁ : EF} {f₀' : E →L[𝕜] F} {f₁' : E →L[𝕜] F} {x : E} {L : } (h₀ : f₀ =ᶠ[L] f₁) (hx : f₀ x = f₁ x) (h₁ : ∀ (x : E), f₀' x = f₁' x) :
HasFDerivAtFilter f₀ f₀' x L HasFDerivAtFilter f₁ f₁' x L
theorem HasFDerivAtFilter.congr_of_eventuallyEq {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f₁ : EF} {f' : E →L[𝕜] F} {x : E} {L : } (h : HasFDerivAtFilter f f' x L) (hL : f₁ =ᶠ[L] f) (hx : f₁ x = f x) :
HasFDerivAtFilter f₁ f' x L
theorem Filter.EventuallyEq.hasFDerivAt_iff {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f₀ : EF} {f₁ : EF} {f' : E →L[𝕜] F} {x : E} (h : f₀ =ᶠ[nhds x] f₁) :
HasFDerivAt f₀ f' x HasFDerivAt f₁ f' x
theorem Filter.EventuallyEq.differentiableAt_iff {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f₀ : EF} {f₁ : EF} {x : E} (h : f₀ =ᶠ[nhds x] f₁) :
DifferentiableAt 𝕜 f₀ x DifferentiableAt 𝕜 f₁ x
theorem Filter.EventuallyEq.hasFDerivWithinAt_iff {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f₀ : EF} {f₁ : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} (h : f₀ =ᶠ[] f₁) (hx : f₀ x = f₁ x) :
HasFDerivWithinAt f₀ f' s x HasFDerivWithinAt f₁ f' s x
theorem Filter.EventuallyEq.hasFDerivWithinAt_iff_of_mem {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f₀ : EF} {f₁ : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} (h : f₀ =ᶠ[] f₁) (hx : x s) :
HasFDerivWithinAt f₀ f' s x HasFDerivWithinAt f₁ f' s x
theorem Filter.EventuallyEq.differentiableWithinAt_iff {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f₀ : EF} {f₁ : EF} {x : E} {s : Set E} (h : f₀ =ᶠ[] f₁) (hx : f₀ x = f₁ x) :
theorem Filter.EventuallyEq.differentiableWithinAt_iff_of_mem {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f₀ : EF} {f₁ : EF} {x : E} {s : Set E} (h : f₀ =ᶠ[] f₁) (hx : x s) :
theorem HasFDerivWithinAt.congr_mono {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f₁ : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} {t : Set E} (h : HasFDerivWithinAt f f' s x) (ht : Set.EqOn f₁ f t) (hx : f₁ x = f x) (h₁ : t s) :
HasFDerivWithinAt f₁ f' t x
theorem HasFDerivWithinAt.congr {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f₁ : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} (h : HasFDerivWithinAt f f' s x) (hs : Set.EqOn f₁ f s) (hx : f₁ x = f x) :
HasFDerivWithinAt f₁ f' s x
theorem HasFDerivWithinAt.congr' {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f₁ : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} (h : HasFDerivWithinAt f f' s x) (hs : Set.EqOn f₁ f s) (hx : x s) :
HasFDerivWithinAt f₁ f' s x
theorem HasFDerivWithinAt.congr_of_eventuallyEq {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f₁ : EF} {f' : E →L[𝕜] F} {x : E} {s : Set E} (h : HasFDerivWithinAt f f' s x) (h₁ : f₁ =ᶠ[] f) (hx : f₁ x = f x) :
HasFDerivWithinAt f₁ f' s x
theorem HasFDerivAt.congr_of_eventuallyEq {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f₁ : EF} {f' : E →L[𝕜] F} {x : E} (h : HasFDerivAt f f' x) (h₁ : f₁ =ᶠ[nhds x] f) :
HasFDerivAt f₁ f' x
theorem DifferentiableWithinAt.congr_mono {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f₁ : EF} {x : E} {s : Set E} {t : Set E} (h : ) (ht : Set.EqOn f₁ f t) (hx : f₁ x = f x) (h₁ : t s) :
theorem DifferentiableWithinAt.congr {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f₁ : EF} {x : E} {s : Set E} (h : ) (ht : xs, f₁ x = f x) (hx : f₁ x = f x) :
theorem DifferentiableWithinAt.congr_of_eventuallyEq {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f₁ : EF} {x : E} {s : Set E} (h : ) (h₁ : f₁ =ᶠ[] f) (hx : f₁ x = f x) :
theorem DifferentiableOn.congr_mono {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f₁ : EF} {s : Set E} {t : Set E} (h : ) (h' : xt, f₁ x = f x) (h₁ : t s) :
DifferentiableOn 𝕜 f₁ t
theorem DifferentiableOn.congr {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f₁ : EF} {s : Set E} (h : ) (h' : xs, f₁ x = f x) :
DifferentiableOn 𝕜 f₁ s
theorem differentiableOn_congr {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f₁ : EF} {s : Set E} (h' : xs, f₁ x = f x) :
DifferentiableOn 𝕜 f₁ s
theorem DifferentiableAt.congr_of_eventuallyEq {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f₁ : EF} {x : E} (h : ) (hL : f₁ =ᶠ[nhds x] f) :
DifferentiableAt 𝕜 f₁ x
theorem DifferentiableWithinAt.fderivWithin_congr_mono {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f₁ : EF} {x : E} {s : Set E} {t : Set E} (h : ) (hs : Set.EqOn f₁ f t) (hx : f₁ x = f x) (hxt : ) (h₁ : t s) :
fderivWithin 𝕜 f₁ t x = fderivWithin 𝕜 f s x
theorem Filter.EventuallyEq.fderivWithin_eq {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f₁ : EF} {x : E} {s : Set E} (hs : f₁ =ᶠ[] f) (hx : f₁ x = f x) :
fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x
theorem Filter.EventuallyEq.fderivWithin' {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f₁ : EF} {x : E} {s : Set E} {t : Set E} (hs : f₁ =ᶠ[] f) (ht : t s) :
fderivWithin 𝕜 f₁ t =ᶠ[] fderivWithin 𝕜 f t
theorem Filter.EventuallyEq.fderivWithin {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f₁ : EF} {x : E} {s : Set E} (hs : f₁ =ᶠ[] f) :
fderivWithin 𝕜 f₁ s =ᶠ[] fderivWithin 𝕜 f s
theorem Filter.EventuallyEq.fderivWithin_eq_nhds {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f₁ : EF} {x : E} {s : Set E} (h : f₁ =ᶠ[nhds x] f) :
fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x
theorem fderivWithin_congr {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f₁ : EF} {x : E} {s : Set E} (hs : Set.EqOn f₁ f s) (hx : f₁ x = f x) :
fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x
theorem fderivWithin_congr' {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f₁ : EF} {x : E} {s : Set E} (hs : Set.EqOn f₁ f s) (hx : x s) :
fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x
theorem Filter.EventuallyEq.fderiv_eq {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f₁ : EF} {x : E} (h : f₁ =ᶠ[nhds x] f) :
fderiv 𝕜 f₁ x = fderiv 𝕜 f x
theorem Filter.EventuallyEq.fderiv {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {f₁ : EF} {x : E} (h : f₁ =ᶠ[nhds x] f) :
fderiv 𝕜 f₁ =ᶠ[nhds x] fderiv 𝕜 f

### Derivative of the identity #

theorem hasStrictFDerivAt_id {𝕜 : Type u_1} {E : Type u_2} [] (x : E) :
theorem hasFDerivAtFilter_id {𝕜 : Type u_1} {E : Type u_2} [] (x : E) (L : ) :
theorem hasFDerivWithinAt_id {𝕜 : Type u_1} {E : Type u_2} [] (x : E) (s : Set E) :
theorem hasFDerivAt_id {𝕜 : Type u_1} {E : Type u_2} [] (x : E) :
HasFDerivAt id () x
@[simp]
theorem differentiableAt_id {𝕜 : Type u_1} {E : Type u_2} [] {x : E} :
@[simp]
theorem differentiableAt_id' {𝕜 : Type u_1} {E : Type u_2} [] {x : E} :
DifferentiableAt 𝕜 (fun (x : E) => x) x
theorem differentiableWithinAt_id {𝕜 : Type u_1} {E : Type u_2} [] {x : E} {s : Set E} :
@[simp]
theorem differentiable_id {𝕜 : Type u_1} {E : Type u_2} [] :
@[simp]
theorem differentiable_id' {𝕜 : Type u_1} {E : Type u_2} [] :
Differentiable 𝕜 fun (x : E) => x
theorem differentiableOn_id {𝕜 : Type u_1} {E : Type u_2} [] {s : Set E} :
@[simp]
theorem fderiv_id {𝕜 : Type u_1} {E : Type u_2} [] {x : E} :
fderiv 𝕜 id x =
@[simp]
theorem fderiv_id' {𝕜 : Type u_1} {E : Type u_2} [] {x : E} :
fderiv 𝕜 (fun (x : E) => x) x =
theorem fderivWithin_id {𝕜 : Type u_1} {E : Type u_2} [] {x : E} {s : Set E} (hxs : ) :
fderivWithin 𝕜 id s x =
theorem fderivWithin_id' {𝕜 : Type u_1} {E : Type u_2} [] {x : E} {s : Set E} (hxs : ) :
fderivWithin 𝕜 (fun (x : E) => x) s x =

### Derivative of a constant function #

theorem hasStrictFDerivAt_const {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] (c : F) (x : E) :
HasStrictFDerivAt (fun (x : E) => c) 0 x
theorem hasFDerivAtFilter_const {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] (c : F) (x : E) (L : ) :
HasFDerivAtFilter (fun (x : E) => c) 0 x L
theorem hasFDerivWithinAt_const {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] (c : F) (x : E) (s : Set E) :
HasFDerivWithinAt (fun (x : E) => c) 0 s x
theorem hasFDerivAt_const {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] (c : F) (x : E) :
HasFDerivAt (fun (x : E) => c) 0 x
@[simp]
theorem differentiableAt_const {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {x : E} (c : F) :
DifferentiableAt 𝕜 (fun (x : E) => c) x
theorem differentiableWithinAt_const {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {x : E} {s : Set E} (c : F) :
DifferentiableWithinAt 𝕜 (fun (x : E) => c) s x
theorem fderiv_const_apply {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {x : E} (c : F) :
fderiv 𝕜 (fun (x : E) => c) x = 0
@[simp]
theorem fderiv_const {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] (c : F) :
(fderiv 𝕜 fun (x : E) => c) = 0
theorem fderivWithin_const_apply {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {x : E} {s : Set E} (c : F) (hxs : ) :
fderivWithin 𝕜 (fun (x : E) => c) s x = 0
@[simp]
theorem differentiable_const {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] (c : F) :
Differentiable 𝕜 fun (x : E) => c
theorem differentiableOn_const {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {s : Set E} (c : F) :
DifferentiableOn 𝕜 (fun (x : E) => c) s
theorem hasFDerivWithinAt_singleton {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] (f : EF) (x : E) :
theorem hasFDerivAt_of_subsingleton {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] [h : ] (f : EF) (x : E) :
theorem differentiableOn_empty {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} :
theorem differentiableOn_singleton {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} :
DifferentiableOn 𝕜 f {x}
theorem Set.Subsingleton.differentiableOn {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {s : Set E} (hs : s.Subsingleton) :
theorem hasFDerivAt_zero_of_eventually_const {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : EF} {x : E} (c : F) (hf : f =ᶠ[nhds x] fun (x : E) => c) :

### Support of derivatives #

theorem HasStrictFDerivAt.of_nmem_tsupport (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [] [] {f : EF} {x : E} (h : x) :
theorem HasFDerivAt.of_nmem_tsupport (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [] [] {f : EF} {x : E} (h : x) :
theorem HasFDerivWithinAt.of_not_mem_tsupport (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [] [] {f : EF} {s : Set E} {x : E} (h : x) :
theorem fderiv_of_not_mem_tsupport (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [] [] {f : EF} {x : E} (h : x) :
fderiv 𝕜 f x = 0
theorem support_fderiv_subset (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [] [] {f : EF} :
theorem tsupport_fderiv_subset (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [] [] {f : EF} :
tsupport (fderiv 𝕜 f)
theorem HasCompactSupport.fderiv (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [] [] {f : EF} (hf : ) :