# One-dimensional derivatives #

This file defines the derivative of a function f : π β F where π is a normed field and F is a normed space over this field. The derivative of such a function f at a point x is given by an element f' : F.

The theory is developed analogously to the FrΓ©chet derivatives. We first introduce predicates defined in terms of the corresponding predicates for FrΓ©chet derivatives:

• HasDerivAtFilter f f' x L states that the function f has the derivative f' at the point x as x goes along the filter L.

• HasDerivWithinAt f f' s x states that the function f has the derivative f' at the point x within the subset s.

• HasDerivAt f f' x states that the function f has the derivative f' at the point x.

• HasStrictDerivAt f f' x states that the function f has the derivative f' at the point x in the sense of strict differentiability, i.e., f y - f z = (y - z) β’ f' + o (y - z) as y, z β x.

For the last two notions we also define a functional version:

• derivWithin f s x is a derivative of f at x within s. If the derivative does not exist, then derivWithin f s x equals zero.

• deriv f x is a derivative of f at x. If the derivative does not exist, then deriv f x equals zero.

The theorems fderivWithin_derivWithin and fderiv_deriv show that the one-dimensional derivatives coincide with the general FrΓ©chet derivatives.

We also show the existence and compute the derivatives of:

• constants
• the identity function
• linear maps (in Linear.lean)
• addition (in Add.lean)
• sum of finitely many functions (in Add.lean)
• negation (in Add.lean)
• subtraction (in Add.lean)
• star (in Star.lean)
• multiplication of two functions in π β π (in Mul.lean)
• multiplication of a function in π β π and of a function in π β E (in Mul.lean)
• powers of a function (in Pow.lean and ZPow.lean)
• inverse x β xβ»ΒΉ (in Inv.lean)
• division (in Inv.lean)
• composition of a function in π β F with a function in π β π (in Comp.lean)
• composition of a function in F β E with a function in π β F (in Comp.lean)
• inverse function (assuming that it exists; the inverse function theorem is in Inverse.lean)
• polynomials (in Polynomial.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.

We set up the simplifier so that it can compute the derivative of simple functions. For instance,

example (x : β) :
deriv (fun x β¦ cos (sin x) * exp x) x = (cos(sin(x))-sin(sin(x))*cos(x))*exp(x) := by
simp; ring


The relationship between the derivative of a function and its definition from a standard undergraduate course as the limit of the slope (f y - f x) / (y - x) as y tends to π[β ] x is developed in the file Slope.lean.

## Implementation notes #

Most of the theorems are direct restatements of the corresponding theorems for FrΓ©chet derivatives.

The strategy to construct simp lemmas that give the simplifier the possibility to compute derivatives is the same as the one for differentiability statements, as explained in FDeriv/Basic.lean. See the explanations there.

def HasDerivAtFilter {π : Type u} [] {F : Type v} [NormedSpace π F] (f : π β F) (f' : F) (x : π) (L : Filter π) :

f has the derivative f' at the point x as x goes along the filter L.

That is, f x' = f x + (x' - x) β’ f' + o(x' - x) where x' converges along the filter L.

Equations
Instances For
def HasDerivWithinAt {π : Type u} [] {F : Type v} [NormedSpace π F] (f : π β F) (f' : F) (s : Set π) (x : π) :

f has the derivative f' at the point x within the subset s.

That is, f x' = f x + (x' - x) β’ f' + o(x' - x) where x' converges to x inside s.

Equations
Instances For
def HasDerivAt {π : Type u} [] {F : Type v} [NormedSpace π F] (f : π β F) (f' : F) (x : π) :

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.

Equations
Instances For
def HasStrictDerivAt {π : Type u} [] {F : Type v} [NormedSpace π F] (f : π β F) (f' : F) (x : π) :

f has the derivative f' at the point x in the sense of strict differentiability.

That is, f y - f z = (y - z) β’ f' + o(y - z) as y, z β x.

Equations
Instances For
def derivWithin {π : Type u} [] {F : Type v} [NormedSpace π F] (f : π β F) (s : Set π) (x : π) :
F

Derivative of f at the point x within the set s, if it exists. Zero otherwise.

If the derivative exists (i.e., β f', HasDerivWithinAt f f' s x), then f x' = f x + (x' - x) β’ derivWithin f s x + o(x' - x) where x' converges to x inside s.

Equations
Instances For
def deriv {π : Type u} [] {F : Type v} [NormedSpace π F] (f : π β F) (x : π) :
F

Derivative of f at the point x, if it exists. Zero otherwise.

If the derivative exists (i.e., β f', HasDerivAt f f' x), then f x' = f x + (x' - x) β’ deriv f x + o(x' - x) where x' converges to x.

Equations
Instances For
theorem hasFDerivAtFilter_iff_hasDerivAtFilter {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {L : Filter π} {f' : π βL[π] F} :

Expressing HasFDerivAtFilter f f' x L in terms of HasDerivAtFilter

theorem HasFDerivAtFilter.hasDerivAtFilter {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {L : Filter π} {f' : π βL[π] F} :
HasFDerivAtFilter f f' x L β HasDerivAtFilter f (f' 1) x L
theorem hasFDerivWithinAt_iff_hasDerivWithinAt {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {s : Set π} {f' : π βL[π] F} :

Expressing HasFDerivWithinAt f f' s x in terms of HasDerivWithinAt

theorem hasDerivWithinAt_iff_hasFDerivWithinAt {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {s : Set π} {f' : F} :

Expressing HasDerivWithinAt f f' s x in terms of HasFDerivWithinAt

theorem HasFDerivWithinAt.hasDerivWithinAt {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {s : Set π} {f' : π βL[π] F} :
HasFDerivWithinAt f f' s x β HasDerivWithinAt f (f' 1) s x
theorem HasDerivWithinAt.hasFDerivWithinAt {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {s : Set π} {f' : F} :
HasDerivWithinAt f f' s x β
theorem hasFDerivAt_iff_hasDerivAt {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {f' : π βL[π] F} :
HasFDerivAt f f' x β HasDerivAt f (f' 1) x

Expressing HasFDerivAt f f' x in terms of HasDerivAt

theorem HasFDerivAt.hasDerivAt {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {f' : π βL[π] F} :
HasFDerivAt f f' x β HasDerivAt f (f' 1) x
theorem hasStrictFDerivAt_iff_hasStrictDerivAt {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {f' : π βL[π] F} :
theorem HasStrictFDerivAt.hasStrictDerivAt {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {f' : π βL[π] F} :
β HasStrictDerivAt f (f' 1) x
theorem hasStrictDerivAt_iff_hasStrictFDerivAt {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} :
theorem HasStrictDerivAt.hasStrictFDerivAt {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} :
HasStrictDerivAt f f' x β

Alias of the forward direction of hasStrictDerivAt_iff_hasStrictFDerivAt.

theorem hasDerivAt_iff_hasFDerivAt {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {f' : F} :

Expressing HasDerivAt f f' x in terms of HasFDerivAt

theorem HasDerivAt.hasFDerivAt {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {f' : F} :
HasDerivAt f f' x β

Alias of the forward direction of hasDerivAt_iff_hasFDerivAt.

Expressing HasDerivAt f f' x in terms of HasFDerivAt

theorem derivWithin_zero_of_not_differentiableWithinAt {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {s : Set π} (h : Β¬DifferentiableWithinAt π f s x) :
derivWithin f s x = 0
theorem derivWithin_zero_of_isolated {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {s : Set π} (h : nhdsWithin x (s \ {x}) = β₯) :
derivWithin f s x = 0
theorem derivWithin_zero_of_nmem_closure {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {s : Set π} (h : x β ) :
derivWithin f s x = 0
theorem differentiableWithinAt_of_derivWithin_ne_zero {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {s : Set π} (h : derivWithin f s x β  0) :
DifferentiableWithinAt π f s x
theorem deriv_zero_of_not_differentiableAt {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} (h : Β¬DifferentiableAt π f x) :
deriv f x = 0
theorem differentiableAt_of_deriv_ne_zero {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} (h : deriv f x β  0) :
DifferentiableAt π f x
theorem UniqueDiffWithinAt.eq_deriv {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {fβ' : F} {x : π} (s : Set π) (H : UniqueDiffWithinAt π s x) (h : HasDerivWithinAt f f' s x) (hβ : HasDerivWithinAt f fβ' s x) :
f' = fβ'
theorem hasDerivAtFilter_iff_isLittleO {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} {L : Filter π} :
HasDerivAtFilter f f' x L β (fun (x' : π) => f x' - f x - (x' - x) β’ f') =o[L] fun (x' : π) => x' - x
theorem hasDerivAtFilter_iff_tendsto {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} {L : Filter π} :
HasDerivAtFilter f f' x L β Filter.Tendsto (fun (x' : π) => βx' - xββ»ΒΉ * βf x' - f x - (x' - x) β’ f'β) L (nhds 0)
theorem hasDerivWithinAt_iff_isLittleO {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} {s : Set π} :
HasDerivWithinAt f f' s x β (fun (x' : π) => f x' - f x - (x' - x) β’ f') =o[] fun (x' : π) => x' - x
theorem hasDerivWithinAt_iff_tendsto {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} {s : Set π} :
HasDerivWithinAt f f' s x β Filter.Tendsto (fun (x' : π) => βx' - xββ»ΒΉ * βf x' - f x - (x' - x) β’ f'β) () (nhds 0)
theorem hasDerivAt_iff_isLittleO {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} :
HasDerivAt f f' x β (fun (x' : π) => f x' - f x - (x' - x) β’ f') =o[nhds x] fun (x' : π) => x' - x
theorem hasDerivAt_iff_tendsto {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} :
HasDerivAt f f' x β Filter.Tendsto (fun (x' : π) => βx' - xββ»ΒΉ * βf x' - f x - (x' - x) β’ f'β) (nhds x) (nhds 0)
theorem HasDerivAtFilter.isBigO_sub {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} {L : Filter π} (h : HasDerivAtFilter f f' x L) :
(fun (x' : π) => f x' - f x) =O[L] fun (x' : π) => x' - x
theorem HasDerivAtFilter.isBigO_sub_rev {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} {L : Filter π} (hf : HasDerivAtFilter f f' x L) (hf' : f' β  0) :
(fun (x' : π) => x' - x) =O[L] fun (x' : π) => f x' - f x
theorem HasStrictDerivAt.hasDerivAt {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} (h : HasStrictDerivAt f f' x) :
HasDerivAt f f' x
theorem hasDerivWithinAt_congr_set' {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} {s : Set π} {t : Set π} (y : π) (h : s =αΆ [nhdsWithin x {y}αΆ] t) :
theorem hasDerivWithinAt_congr_set {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} {s : Set π} {t : Set π} (h : s =αΆ [nhds x] t) :
theorem HasDerivWithinAt.congr_set {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} {s : Set π} {t : Set π} (h : s =αΆ [nhds x] t) :
HasDerivWithinAt f f' s x β HasDerivWithinAt f f' t x

Alias of the forward direction of hasDerivWithinAt_congr_set.

@[simp]
theorem hasDerivWithinAt_diff_singleton {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} {s : Set π} :
HasDerivWithinAt f f' (s \ {x}) x β HasDerivWithinAt f f' s x
@[simp]
theorem hasDerivWithinAt_Ioi_iff_Ici {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} [PartialOrder π] :
theorem HasDerivWithinAt.Ioi_of_Ici {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} [PartialOrder π] :
HasDerivWithinAt f f' () x β HasDerivWithinAt f f' () x

Alias of the reverse direction of hasDerivWithinAt_Ioi_iff_Ici.

theorem HasDerivWithinAt.Ici_of_Ioi {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} [PartialOrder π] :
HasDerivWithinAt f f' () x β HasDerivWithinAt f f' () x

Alias of the forward direction of hasDerivWithinAt_Ioi_iff_Ici.

@[simp]
theorem hasDerivWithinAt_Iio_iff_Iic {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} [PartialOrder π] :
theorem HasDerivWithinAt.Iio_of_Iic {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} [PartialOrder π] :
HasDerivWithinAt f f' () x β HasDerivWithinAt f f' () x

Alias of the reverse direction of hasDerivWithinAt_Iio_iff_Iic.

theorem HasDerivWithinAt.Iic_of_Iio {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} [PartialOrder π] :
HasDerivWithinAt f f' () x β HasDerivWithinAt f f' () x

Alias of the forward direction of hasDerivWithinAt_Iio_iff_Iic.

theorem HasDerivWithinAt.Ioi_iff_Ioo {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} [LinearOrder π] [] {x : π} {y : π} (h : x < y) :
theorem HasDerivWithinAt.Ioo_of_Ioi {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} [LinearOrder π] [] {x : π} {y : π} (h : x < y) :
HasDerivWithinAt f f' () x β HasDerivWithinAt f f' (Set.Ioo x y) x

Alias of the reverse direction of HasDerivWithinAt.Ioi_iff_Ioo.

theorem HasDerivWithinAt.Ioi_of_Ioo {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} [LinearOrder π] [] {x : π} {y : π} (h : x < y) :
HasDerivWithinAt f f' (Set.Ioo x y) x β HasDerivWithinAt f f' () x

Alias of the forward direction of HasDerivWithinAt.Ioi_iff_Ioo.

theorem hasDerivAt_iff_isLittleO_nhds_zero {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} :
HasDerivAt f f' x β (fun (h : π) => f (x + h) - f x - h β’ f') =o[nhds 0] fun (h : π) => h
theorem HasDerivAtFilter.mono {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} {Lβ : Filter π} {Lβ : Filter π} (h : HasDerivAtFilter f f' x Lβ) (hst : Lβ β€ Lβ) :
HasDerivAtFilter f f' x Lβ
theorem HasDerivWithinAt.mono {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} {s : Set π} {t : Set π} (h : HasDerivWithinAt f f' t x) (hst : s β t) :
theorem HasDerivWithinAt.mono_of_mem {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} {s : Set π} {t : Set π} (h : HasDerivWithinAt f f' t x) (hst : t β ) :
theorem HasDerivAt.hasDerivAtFilter {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} {L : Filter π} (h : HasDerivAt f f' x) (hL : L β€ nhds x) :
theorem HasDerivAt.hasDerivWithinAt {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} {s : Set π} (h : HasDerivAt f f' x) :
theorem HasDerivWithinAt.differentiableWithinAt {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} {s : Set π} (h : HasDerivWithinAt f f' s x) :
DifferentiableWithinAt π f s x
theorem HasDerivAt.differentiableAt {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} (h : HasDerivAt f f' x) :
DifferentiableAt π f x
@[simp]
theorem hasDerivWithinAt_univ {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} :
HasDerivWithinAt f f' Set.univ x β HasDerivAt f f' x
theorem HasDerivAt.unique {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {fβ' : F} {fβ' : F} {x : π} (hβ : HasDerivAt f fβ' x) (hβ : HasDerivAt f fβ' x) :
fβ' = fβ'
theorem hasDerivWithinAt_inter' {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} {s : Set π} {t : Set π} (h : t β ) :
theorem hasDerivWithinAt_inter {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} {s : Set π} {t : Set π} (h : t β nhds x) :
theorem HasDerivWithinAt.union {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} {s : Set π} {t : Set π} (hs : HasDerivWithinAt f f' s x) (ht : HasDerivWithinAt f f' t x) :
theorem HasDerivWithinAt.hasDerivAt {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} {s : Set π} (h : HasDerivWithinAt f f' s x) (hs : s β nhds x) :
HasDerivAt f f' x
theorem DifferentiableWithinAt.hasDerivWithinAt {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {s : Set π} (h : DifferentiableWithinAt π f s x) :
theorem DifferentiableAt.hasDerivAt {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} (h : DifferentiableAt π f x) :
HasDerivAt f (deriv f x) x
@[simp]
theorem hasDerivAt_deriv_iff {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} :
HasDerivAt f (deriv f x) x β DifferentiableAt π f x
@[simp]
theorem hasDerivWithinAt_derivWithin_iff {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {s : Set π} :
theorem DifferentiableOn.hasDerivAt {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {s : Set π} (h : DifferentiableOn π f s) (hs : s β nhds x) :
HasDerivAt f (deriv f x) x
theorem HasDerivAt.deriv {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} (h : HasDerivAt f f' x) :
deriv f x = f'
theorem deriv_eq {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : π β F} (h : β (x : π), HasDerivAt f (f' x) x) :
= f'
theorem HasDerivWithinAt.derivWithin {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} {s : Set π} (h : HasDerivWithinAt f f' s x) (hxs : UniqueDiffWithinAt π s x) :
derivWithin f s x = f'
theorem fderivWithin_derivWithin {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {s : Set π} :
(fderivWithin π f s x) 1 = derivWithin f s x
theorem derivWithin_fderivWithin {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {s : Set π} :
= fderivWithin π f s x
theorem norm_derivWithin_eq_norm_fderivWithin {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {s : Set π} :
theorem fderiv_deriv {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} :
(fderiv π f x) 1 = deriv f x
@[simp]
theorem fderiv_eq_smul_deriv {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} (y : π) :
(fderiv π f x) y = y β’ deriv f x
theorem deriv_fderiv {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} :
= fderiv π f x
theorem fderiv_eq_deriv_mul {π : Type u} [] {f : π β π} {x : π} {y : π} :
(fderiv π f x) y = deriv f x * y
theorem norm_deriv_eq_norm_fderiv {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} :
theorem DifferentiableAt.derivWithin {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {s : Set π} (h : DifferentiableAt π f x) (hxs : UniqueDiffWithinAt π s x) :
derivWithin f s x = deriv f x
theorem HasDerivWithinAt.deriv_eq_zero {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {s : Set π} (hd : HasDerivWithinAt f 0 s x) (H : UniqueDiffWithinAt π s x) :
deriv f x = 0
theorem derivWithin_of_mem {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {s : Set π} {t : Set π} (st : t β ) (ht : UniqueDiffWithinAt π s x) (h : DifferentiableWithinAt π f t x) :
theorem derivWithin_subset {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {s : Set π} {t : Set π} (st : s β t) (ht : UniqueDiffWithinAt π s x) (h : DifferentiableWithinAt π f t x) :
theorem derivWithin_congr_set' {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {s : Set π} {t : Set π} (y : π) (h : s =αΆ [nhdsWithin x {y}αΆ] t) :
theorem derivWithin_congr_set {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {s : Set π} {t : Set π} (h : s =αΆ [nhds x] t) :
@[simp]
theorem derivWithin_univ {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} :
derivWithin f Set.univ =
theorem derivWithin_inter {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {s : Set π} {t : Set π} (ht : t β nhds x) :
theorem derivWithin_of_mem_nhds {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {s : Set π} (h : s β nhds x) :
derivWithin f s x = deriv f x
theorem derivWithin_of_isOpen {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} {s : Set π} (hs : ) (hx : x β s) :
derivWithin f s x = deriv f x
theorem deriv_eqOn {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {s : Set π} {f' : π β F} (hs : ) (hf' : β x β s, HasDerivWithinAt f (f' x) s x) :
Set.EqOn () f' s
theorem deriv_mem_iff {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {s : Set F} {x : π} :
theorem derivWithin_mem_iff {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {t : Set π} {s : Set F} {x : π} :
theorem differentiableWithinAt_Ioi_iff_Ici {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {x : π} [PartialOrder π] :
DifferentiableWithinAt π f () x β DifferentiableWithinAt π f () x
theorem derivWithin_Ioi_eq_Ici {E : Type u_1} [] (f : β β E) (x : β) :
derivWithin f () x = derivWithin f () x

### Congruence properties of derivatives #

theorem Filter.EventuallyEq.hasDerivAtFilter_iff {π : Type u} [] {F : Type v} [NormedSpace π F] {fβ : π β F} {fβ : π β F} {fβ' : F} {fβ' : F} {x : π} {L : Filter π} (hβ : fβ =αΆ [L] fβ) (hx : fβ x = fβ x) (hβ : fβ' = fβ') :
HasDerivAtFilter fβ fβ' x L β HasDerivAtFilter fβ fβ' x L
theorem HasDerivAtFilter.congr_of_eventuallyEq {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {fβ : π β F} {f' : F} {x : π} {L : Filter π} (h : HasDerivAtFilter f f' x L) (hL : fβ =αΆ [L] f) (hx : fβ x = f x) :
HasDerivAtFilter fβ f' x L
theorem HasDerivWithinAt.congr_mono {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {fβ : π β F} {f' : F} {x : π} {s : Set π} {t : Set π} (h : HasDerivWithinAt f f' s x) (ht : β x β t, fβ x = f x) (hx : fβ x = f x) (hβ : t β s) :
HasDerivWithinAt fβ f' t x
theorem HasDerivWithinAt.congr {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {fβ : π β F} {f' : F} {x : π} {s : Set π} (h : HasDerivWithinAt f f' s x) (hs : β x β s, fβ x = f x) (hx : fβ x = f x) :
HasDerivWithinAt fβ f' s x
theorem HasDerivWithinAt.congr_of_mem {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {fβ : π β F} {f' : F} {x : π} {s : Set π} (h : HasDerivWithinAt f f' s x) (hs : β x β s, fβ x = f x) (hx : x β s) :
HasDerivWithinAt fβ f' s x
theorem HasDerivWithinAt.congr_of_eventuallyEq {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {fβ : π β F} {f' : F} {x : π} {s : Set π} (h : HasDerivWithinAt f f' s x) (hβ : fβ =αΆ [] f) (hx : fβ x = f x) :
HasDerivWithinAt fβ f' s x
theorem Filter.EventuallyEq.hasDerivWithinAt_iff {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {fβ : π β F} {f' : F} {x : π} {s : Set π} (hβ : fβ =αΆ [] f) (hx : fβ x = f x) :
HasDerivWithinAt fβ f' s x β HasDerivWithinAt f f' s x
theorem HasDerivWithinAt.congr_of_eventuallyEq_of_mem {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {fβ : π β F} {f' : F} {x : π} {s : Set π} (h : HasDerivWithinAt f f' s x) (hβ : fβ =αΆ [] f) (hx : x β s) :
HasDerivWithinAt fβ f' s x
theorem Filter.EventuallyEq.hasDerivWithinAt_iff_of_mem {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {fβ : π β F} {f' : F} {x : π} {s : Set π} (hβ : fβ =αΆ [] f) (hx : x β s) :
HasDerivWithinAt fβ f' s x β HasDerivWithinAt f f' s x
theorem HasStrictDerivAt.congr_deriv {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {g' : F} {x : π} (h : HasStrictDerivAt f f' x) (h' : f' = g') :
theorem HasDerivAt.congr_deriv {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {g' : F} {x : π} (h : HasDerivAt f f' x) (h' : f' = g') :
HasDerivAt f g' x
theorem HasDerivWithinAt.congr_deriv {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {g' : F} {x : π} {s : Set π} (h : HasDerivWithinAt f f' s x) (h' : f' = g') :
theorem HasDerivAt.congr_of_eventuallyEq {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {fβ : π β F} {f' : F} {x : π} (h : HasDerivAt f f' x) (hβ : fβ =αΆ [nhds x] f) :
HasDerivAt fβ f' x
theorem Filter.EventuallyEq.hasDerivAt_iff {π : Type u} [] {F : Type v} [NormedSpace π F] {fβ : π β F} {fβ : π β F} {f' : F} {x : π} (h : fβ =αΆ [nhds x] fβ) :
HasDerivAt fβ f' x β HasDerivAt fβ f' x
theorem Filter.EventuallyEq.derivWithin_eq {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {fβ : π β F} {x : π} {s : Set π} (hs : fβ =αΆ [] f) (hx : fβ x = f x) :
derivWithin fβ s x = derivWithin f s x
theorem derivWithin_congr {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {fβ : π β F} {x : π} {s : Set π} (hs : Set.EqOn fβ f s) (hx : fβ x = f x) :
derivWithin fβ s x = derivWithin f s x
theorem Filter.EventuallyEq.deriv_eq {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {fβ : π β F} {x : π} (hL : fβ =αΆ [nhds x] f) :
deriv fβ x = deriv f x
theorem Filter.EventuallyEq.deriv {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {fβ : π β F} {x : π} (h : fβ =αΆ [nhds x] f) :
deriv fβ =αΆ [nhds x]

### Derivative of the identity #

theorem hasDerivAtFilter_id {π : Type u} [] (x : π) (L : Filter π) :
theorem hasDerivWithinAt_id {π : Type u} [] (x : π) (s : Set π) :
theorem hasDerivAt_id {π : Type u} [] (x : π) :
HasDerivAt id 1 x
theorem hasDerivAt_id' {π : Type u} [] (x : π) :
HasDerivAt (fun (x : π) => x) 1 x
theorem hasStrictDerivAt_id {π : Type u} [] (x : π) :
theorem deriv_id {π : Type u} [] (x : π) :
deriv id x = 1
@[simp]
theorem deriv_id' {π : Type u} [] :
deriv id = fun (x : π) => 1
@[simp]
theorem deriv_id'' {π : Type u} [] :
(deriv fun (x : π) => x) = fun (x : π) => 1
theorem derivWithin_id {π : Type u} [] (x : π) (s : Set π) (hxs : UniqueDiffWithinAt π s x) :
derivWithin id s x = 1

### Derivative of constant functions #

theorem hasDerivAtFilter_const {π : Type u} [] {F : Type v} [NormedSpace π F] (x : π) (L : Filter π) (c : F) :
HasDerivAtFilter (fun (x : π) => c) 0 x L
theorem hasStrictDerivAt_const {π : Type u} [] {F : Type v} [NormedSpace π F] (x : π) (c : F) :
HasStrictDerivAt (fun (x : π) => c) 0 x
theorem hasDerivWithinAt_const {π : Type u} [] {F : Type v} [NormedSpace π F] (x : π) (s : Set π) (c : F) :
HasDerivWithinAt (fun (x : π) => c) 0 s x
theorem hasDerivAt_const {π : Type u} [] {F : Type v} [NormedSpace π F] (x : π) (c : F) :
HasDerivAt (fun (x : π) => c) 0 x
theorem deriv_const {π : Type u} [] {F : Type v} [NormedSpace π F] (x : π) (c : F) :
deriv (fun (x : π) => c) x = 0
@[simp]
theorem deriv_const' {π : Type u} [] {F : Type v} [NormedSpace π F] (c : F) :
(deriv fun (x : π) => c) = fun (x : π) => 0
theorem derivWithin_const {π : Type u} [] {F : Type v} [NormedSpace π F] (x : π) (s : Set π) (c : F) (hxs : UniqueDiffWithinAt π s x) :
derivWithin (fun (x : π) => c) s x = 0

### Continuity of a function admitting a derivative #

theorem HasDerivAtFilter.tendsto_nhds {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} {L : Filter π} (hL : L β€ nhds x) (h : HasDerivAtFilter f f' x L) :
Filter.Tendsto f L (nhds (f x))
theorem HasDerivWithinAt.continuousWithinAt {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} {s : Set π} (h : HasDerivWithinAt f f' s x) :
theorem HasDerivAt.continuousAt {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {x : π} (h : HasDerivAt f f' x) :
theorem HasDerivAt.continuousOn {π : Type u} [] {F : Type v} [NormedSpace π F] {s : Set π} {f : π β F} {f' : π β F} (hderiv : β x β s, HasDerivAt f (f' x) x) :
theorem HasDerivAt.le_of_lip' {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {xβ : π} (hf : HasDerivAt f f' xβ) {C : β} (hCβ : 0 β€ C) (hlip : βαΆ  (x : π) 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 HasDerivAt.le_of_lipschitzOn {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {xβ : π} (hf : HasDerivAt f f' xβ) {s : Set π} (hs : s β nhds xβ) {C : NNReal} (hlip : ) :

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 HasDerivAt.le_of_lipschitz {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {f' : F} {xβ : π} (hf : HasDerivAt f f' xβ) {C : NNReal} (hlip : ) :

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 norm_deriv_le_of_lip' {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {xβ : π} {C : β} (hCβ : 0 β€ C) (hlip : βαΆ  (x : π) in nhds xβ, βf x - f xββ β€ C * βx - xββ) :

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_deriv_le_of_lipschitzOn {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {xβ : π} {s : Set π} (hs : s β nhds xβ) {C : NNReal} (hlip : ) :
βderiv 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 deriv.

theorem norm_deriv_le_of_lipschitz {π : Type u} [] {F : Type v} [NormedSpace π F] {f : π β F} {xβ : π} {C : NNReal} (hlip : ) :
βderiv 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 deriv.