# mathlib3documentation

analysis.calculus.deriv.basic

# One-dimensional derivatives #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

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

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

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

• `has_strict_deriv_at 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:

• `deriv_within f s x` is a derivative of `f` at `x` within `s`. If the derivative does not exist, then `deriv_within 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 `fderiv_within_deriv_within` 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 `has_deriv_at`'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 (Ξ» x, cos (sin x) * exp x) x = (cos(sin(x))-sin(sin(x))*cos(x))*exp(x) :=
by { simp, ring }
``````

## 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.lean`. See the explanations there.

def has_deriv_at_filter {π : Type u} {F : Type v} [normed_space π F] (f : π β F) (f' : F) (x : π) (L : filter π) :
Prop

`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
def has_deriv_within_at {π : Type u} {F : Type v} [normed_space π F] (f : π β F) (f' : F) (s : set π) (x : π) :
Prop

`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
• s x = x s)
def has_deriv_at {π : Type u} {F : Type v} [normed_space π F] (f : π β F) (f' : F) (x : π) :
Prop

`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
def has_strict_deriv_at {π : Type u} {F : Type v} [normed_space π F] (f : π β F) (f' : F) (x : π) :
Prop

`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
noncomputable def deriv_within {π : Type u} {F : Type v} [normed_space π 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', has_deriv_within_at f f' s x`), then `f x' = f x + (x' - x) β’ deriv_within f s x + o(x' - x)` where `x'` converges to `x` inside `s`.

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

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

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

Equations
theorem has_fderiv_at_filter_iff_has_deriv_at_filter {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {L : filter π} {f' : π βL[π] F} :
x L β (βf' 1) x L

Expressing `has_fderiv_at_filter f f' x L` in terms of `has_deriv_at_filter`

theorem has_fderiv_at_filter.has_deriv_at_filter {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {L : filter π} {f' : π βL[π] F} :
x L β (βf' 1) x L
theorem has_fderiv_within_at_iff_has_deriv_within_at {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s : set π} {f' : π βL[π] F} :
s x β (βf' 1) s x

Expressing `has_fderiv_within_at f f' s x` in terms of `has_deriv_within_at`

theorem has_deriv_within_at_iff_has_fderiv_within_at {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s : set π} {f' : F} :
s x β (1.smul_right f') s x

Expressing `has_deriv_within_at f f' s x` in terms of `has_fderiv_within_at`

theorem has_fderiv_within_at.has_deriv_within_at {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s : set π} {f' : π βL[π] F} :
s x β (βf' 1) s x
theorem has_deriv_within_at.has_fderiv_within_at {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s : set π} {f' : F} :
s x β (1.smul_right f') s x
theorem has_fderiv_at_iff_has_deriv_at {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {f' : π βL[π] F} :
f' x β (βf' 1) x

Expressing `has_fderiv_at f f' x` in terms of `has_deriv_at`

theorem has_fderiv_at.has_deriv_at {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {f' : π βL[π] F} :
f' x β (βf' 1) x
theorem has_strict_fderiv_at_iff_has_strict_deriv_at {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {f' : π βL[π] F} :
x β (βf' 1) x
@[protected]
theorem has_strict_fderiv_at.has_strict_deriv_at {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {f' : π βL[π] F} :
x β (βf' 1) x
theorem has_strict_deriv_at_iff_has_strict_fderiv_at {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} :
x β (1.smul_right f') x
theorem has_strict_deriv_at.has_strict_fderiv_at {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} :
x β (1.smul_right f') x

Alias of the forward direction of `has_strict_deriv_at_iff_has_strict_fderiv_at`.

theorem has_deriv_at_iff_has_fderiv_at {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {f' : F} :
f' x β (1.smul_right f') x

Expressing `has_deriv_at f f' x` in terms of `has_fderiv_at`

theorem has_deriv_at.has_fderiv_at {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {f' : F} :
f' x β (1.smul_right f') x

Alias of the forward direction of `has_deriv_at_iff_has_fderiv_at`.

theorem deriv_within_zero_of_not_differentiable_within_at {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s : set π} (h : Β¬ f s x) :
s x = 0
theorem differentiable_within_at_of_deriv_within_ne_zero {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s : set π} (h : s x β  0) :
f s x
theorem deriv_zero_of_not_differentiable_at {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} (h : Β¬ f x) :
x = 0
theorem differentiable_at_of_deriv_ne_zero {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} (h : x β  0) :
f x
theorem unique_diff_within_at.eq_deriv {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' fβ' : F} {x : π} (s : set π) (H : s x) (h : s x) (hβ : fβ' s x) :
f' = fβ'
theorem has_deriv_at_filter_iff_is_o {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {L : filter π} :
x L β (Ξ» (x' : π), f x' - f x - (x' - x) β’ f') =o[L] Ξ» (x' : π), x' - x
theorem has_deriv_at_filter_iff_tendsto {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {L : filter π} :
x L β filter.tendsto (Ξ» (x' : π), βx' - xββ»ΒΉ * βf x' - f x - (x' - x) β’ f'β) L (nhds 0)
theorem has_deriv_within_at_iff_is_o {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s : set π} :
s x β (Ξ» (x' : π), f x' - f x - (x' - x) β’ f') =o[ s] Ξ» (x' : π), x' - x
theorem has_deriv_within_at_iff_tendsto {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s : set π} :
s x β filter.tendsto (Ξ» (x' : π), βx' - xββ»ΒΉ * βf x' - f x - (x' - x) β’ f'β) s) (nhds 0)
theorem has_deriv_at_iff_is_o {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} :
f' x β (Ξ» (x' : π), f x' - f x - (x' - x) β’ f') =o[nhds x] Ξ» (x' : π), x' - x
theorem has_deriv_at_iff_tendsto {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} :
f' x β filter.tendsto (Ξ» (x' : π), βx' - xββ»ΒΉ * βf x' - f x - (x' - x) β’ f'β) (nhds x) (nhds 0)
theorem has_deriv_at_filter.is_O_sub {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {L : filter π} (h : x L) :
(Ξ» (x' : π), f x' - f x) =O[L] Ξ» (x' : π), x' - x
theorem has_deriv_at_filter.is_O_sub_rev {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {L : filter π} (hf : x L) (hf' : f' β  0) :
(Ξ» (x' : π), x' - x) =O[L] Ξ» (x' : π), f x' - f x
theorem has_strict_deriv_at.has_deriv_at {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} (h : x) :
f' x
theorem has_deriv_within_at_congr_set' {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s t : set π} (y : π) (h : s =αΆ [ {y}αΆ] t) :
s x β t x
theorem has_deriv_within_at_congr_set {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s t : set π} (h : s =αΆ [nhds x] t) :
s x β t x
theorem has_deriv_within_at.congr_set {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s t : set π} (h : s =αΆ [nhds x] t) :
s x β t x

Alias of the forward direction of `has_deriv_within_at_congr_set`.

@[simp]
theorem has_deriv_within_at_diff_singleton {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s : set π} :
(s \ {x}) x β s x
@[simp]
theorem has_deriv_within_at_Ioi_iff_Ici {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} [partial_order π] :
(set.Ioi x) x β (set.Ici x) x
theorem has_deriv_within_at.Ioi_of_Ici {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} [partial_order π] :
(set.Ici x) x β (set.Ioi x) x

Alias of the reverse direction of `has_deriv_within_at_Ioi_iff_Ici`.

theorem has_deriv_within_at.Ici_of_Ioi {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} [partial_order π] :
(set.Ioi x) x β (set.Ici x) x

Alias of the forward direction of `has_deriv_within_at_Ioi_iff_Ici`.

@[simp]
theorem has_deriv_within_at_Iio_iff_Iic {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} [partial_order π] :
(set.Iio x) x β (set.Iic x) x
theorem has_deriv_within_at.Iic_of_Iio {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} [partial_order π] :
(set.Iio x) x β (set.Iic x) x

Alias of the forward direction of `has_deriv_within_at_Iio_iff_Iic`.

theorem has_deriv_within_at.Iio_of_Iic {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} [partial_order π] :
(set.Iic x) x β (set.Iio x) x

Alias of the reverse direction of `has_deriv_within_at_Iio_iff_Iic`.

theorem has_deriv_within_at.Ioi_iff_Ioo {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} [linear_order π] [order_closed_topology π] {x y : π} (h : x < y) :
(set.Ioo x y) x β (set.Ioi x) x
theorem has_deriv_within_at.Ioo_of_Ioi {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} [linear_order π] [order_closed_topology π] {x y : π} (h : x < y) :
(set.Ioi x) x β (set.Ioo x y) x

Alias of the reverse direction of `has_deriv_within_at.Ioi_iff_Ioo`.

theorem has_deriv_within_at.Ioi_of_Ioo {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} [linear_order π] [order_closed_topology π] {x y : π} (h : x < y) :
(set.Ioo x y) x β (set.Ioi x) x

Alias of the forward direction of `has_deriv_within_at.Ioi_iff_Ioo`.

theorem has_deriv_at_iff_is_o_nhds_zero {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} :
f' x β (Ξ» (h : π), f (x + h) - f x - h β’ f') =o[nhds 0] Ξ» (h : π), h
theorem has_deriv_at_filter.mono {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {Lβ Lβ : filter π} (h : x Lβ) (hst : Lβ β€ Lβ) :
x Lβ
theorem has_deriv_within_at.mono {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s t : set π} (h : t x) (hst : s β t) :
s x
theorem has_deriv_within_at.mono_of_mem {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s t : set π} (h : t x) (hst : t β s) :
s x
theorem has_deriv_at.has_deriv_at_filter {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {L : filter π} (h : f' x) (hL : L β€ nhds x) :
x L
theorem has_deriv_at.has_deriv_within_at {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s : set π} (h : f' x) :
s x
theorem has_deriv_within_at.differentiable_within_at {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s : set π} (h : s x) :
f s x
theorem has_deriv_at.differentiable_at {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} (h : f' x) :
f x
@[simp]
theorem has_deriv_within_at_univ {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} :
x β f' x
theorem has_deriv_at.unique {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {fβ' fβ' : F} {x : π} (hβ : fβ' x) (hβ : fβ' x) :
fβ' = fβ'
theorem has_deriv_within_at_inter' {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s t : set π} (h : t β s) :
(s β© t) x β s x
theorem has_deriv_within_at_inter {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s t : set π} (h : t β nhds x) :
(s β© t) x β s x
theorem has_deriv_within_at.union {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s t : set π} (hs : s x) (ht : t x) :
(s βͺ t) x
theorem has_deriv_within_at.nhds_within {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s t : set π} (h : s x) (ht : s β t) :
t x
theorem has_deriv_within_at.has_deriv_at {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s : set π} (h : s x) (hs : s β nhds x) :
f' x
theorem differentiable_within_at.has_deriv_within_at {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s : set π} (h : f s x) :
s x) s x
theorem differentiable_at.has_deriv_at {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} (h : f x) :
(deriv f x) x
@[simp]
theorem has_deriv_at_deriv_iff {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} :
(deriv f x) x β f x
@[simp]
theorem has_deriv_within_at_deriv_within_iff {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s : set π} :
s x) s x β f s x
theorem differentiable_on.has_deriv_at {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s : set π} (h : f s) (hs : s β nhds x) :
(deriv f x) x
theorem has_deriv_at.deriv {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} (h : f' x) :
x = f'
theorem deriv_eq {π : Type u} {F : Type v} [normed_space π F] {f f' : π β F} (h : β (x : π), (f' x) x) :
= f'
theorem has_deriv_within_at.deriv_within {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s : set π} (h : s x) (hxs : s x) :
s x = f'
theorem fderiv_within_deriv_within {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s : set π} :
β(fderiv_within π f s x) 1 = s x
theorem deriv_within_fderiv_within {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s : set π} :
1.smul_right s x) = fderiv_within π f s x
theorem fderiv_deriv {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} :
β(fderiv π f x) 1 = x
theorem deriv_fderiv {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} :
1.smul_right (deriv f x) = fderiv π f x
theorem differentiable_at.deriv_within {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s : set π} (h : f x) (hxs : s x) :
s x = x
theorem has_deriv_within_at.deriv_eq_zero {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s : set π} (hd : s x) (H : s x) :
x = 0
theorem deriv_within_of_mem {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s t : set π} (st : t β s) (ht : s x) (h : f t x) :
s x = t x
theorem deriv_within_subset {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s t : set π} (st : s β t) (ht : s x) (h : f t x) :
s x = t x
theorem deriv_within_congr_set' {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s t : set π} (y : π) (h : s =αΆ [ {y}αΆ] t) :
s x = t x
theorem deriv_within_congr_set {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s t : set π} (h : s =αΆ [nhds x] t) :
s x = t x
@[simp]
theorem deriv_within_univ {π : Type u} {F : Type v} [normed_space π F] {f : π β F} :
theorem deriv_within_inter {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s t : set π} (ht : t β nhds x) :
(s β© t) x = s x
theorem deriv_within_of_open {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s : set π} (hs : is_open s) (hx : x β s) :
s x = x
theorem deriv_mem_iff {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {s : set F} {x : π} :
theorem deriv_within_mem_iff {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {t : set π} {s : set F} {x : π} :
t x β s β f t x β§ t x β s β¨ Β¬ f t x β§ 0 β s
theorem differentiable_within_at_Ioi_iff_Ici {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} [partial_order π] :
f (set.Ioi x) x β f (set.Ici x) x
theorem deriv_within_Ioi_eq_Ici {E : Type u_1} [ E] (f : β β E) (x : β) :
(set.Ioi x) x = (set.Ici x) x

### Congruence properties of derivatives #

theorem filter.eventually_eq.has_deriv_at_filter_iff {π : Type u} {F : Type v} [normed_space π F] {fβ fβ : π β F} {fβ' fβ' : F} {x : π} {L : filter π} (hβ : fβ =αΆ [L] fβ) (hx : fβ x = fβ x) (hβ : fβ' = fβ') :
fβ' x L β fβ' x L
theorem has_deriv_at_filter.congr_of_eventually_eq {π : Type u} {F : Type v} [normed_space π F] {f fβ : π β F} {f' : F} {x : π} {L : filter π} (h : x L) (hL : fβ =αΆ [L] f) (hx : fβ x = f x) :
f' x L
theorem has_deriv_within_at.congr_mono {π : Type u} {F : Type v} [normed_space π F] {f fβ : π β F} {f' : F} {x : π} {s t : set π} (h : s x) (ht : β (x : π), x β t β fβ x = f x) (hx : fβ x = f x) (hβ : t β s) :
f' t x
theorem has_deriv_within_at.congr {π : Type u} {F : Type v} [normed_space π F] {f fβ : π β F} {f' : F} {x : π} {s : set π} (h : s x) (hs : β (x : π), x β s β fβ x = f x) (hx : fβ x = f x) :
f' s x
theorem has_deriv_within_at.congr_of_mem {π : Type u} {F : Type v} [normed_space π F] {f fβ : π β F} {f' : F} {x : π} {s : set π} (h : s x) (hs : β (x : π), x β s β fβ x = f x) (hx : x β s) :
f' s x
theorem has_deriv_within_at.congr_of_eventually_eq {π : Type u} {F : Type v} [normed_space π F] {f fβ : π β F} {f' : F} {x : π} {s : set π} (h : s x) (hβ : fβ =αΆ [ s] f) (hx : fβ x = f x) :
f' s x
theorem has_deriv_within_at.congr_of_eventually_eq_of_mem {π : Type u} {F : Type v} [normed_space π F] {f fβ : π β F} {f' : F} {x : π} {s : set π} (h : s x) (hβ : fβ =αΆ [ s] f) (hx : x β s) :
f' s x
theorem has_deriv_at.congr_of_eventually_eq {π : Type u} {F : Type v} [normed_space π F] {f fβ : π β F} {f' : F} {x : π} (h : f' x) (hβ : fβ =αΆ [nhds x] f) :
has_deriv_at fβ f' x
theorem filter.eventually_eq.deriv_within_eq {π : Type u} {F : Type v} [normed_space π F] {f fβ : π β F} {x : π} {s : set π} (hL : fβ =αΆ [ s] f) (hx : fβ x = f x) :
deriv_within fβ s x = s x
theorem deriv_within_congr {π : Type u} {F : Type v} [normed_space π F] {f fβ : π β F} {x : π} {s : set π} (hs : set.eq_on fβ f s) (hx : fβ x = f x) :
deriv_within fβ s x = s x
theorem filter.eventually_eq.deriv_eq {π : Type u} {F : Type v} [normed_space π F] {f fβ : π β F} {x : π} (hL : fβ =αΆ [nhds x] f) :
deriv fβ x = x
@[protected]
theorem filter.eventually_eq.deriv {π : Type u} {F : Type v} [normed_space π F] {f fβ : π β F} {x : π} (h : fβ =αΆ [nhds x] f) :
deriv fβ =αΆ [nhds x]

### Derivative of the identity #

theorem has_deriv_at_filter_id {π : Type u} (x : π) (L : filter π) :
L
theorem has_deriv_within_at_id {π : Type u} (x : π) (s : set π) :
x
theorem has_deriv_at_id {π : Type u} (x : π) :
x
theorem has_deriv_at_id' {π : Type u} (x : π) :
has_deriv_at (Ξ» (x : π), x) 1 x
theorem has_strict_deriv_at_id {π : Type u} (x : π) :
theorem deriv_id {π : Type u} (x : π) :
x = 1
@[simp]
theorem deriv_id' {π : Type u}  :
= Ξ» (_x : π), 1
@[simp]
theorem deriv_id'' {π : Type u}  :
deriv (Ξ» (x : π), x) = Ξ» (_x : π), 1
theorem deriv_within_id {π : Type u} (x : π) (s : set π) (hxs : s x) :
x = 1

### Derivative of constant functions #

theorem has_deriv_at_filter_const {π : Type u} {F : Type v} [normed_space π F] (x : π) (L : filter π) (c : F) :
has_deriv_at_filter (Ξ» (x : π), c) 0 x L
theorem has_strict_deriv_at_const {π : Type u} {F : Type v} [normed_space π F] (x : π) (c : F) :
has_strict_deriv_at (Ξ» (x : π), c) 0 x
theorem has_deriv_within_at_const {π : Type u} {F : Type v} [normed_space π F] (x : π) (s : set π) (c : F) :
has_deriv_within_at (Ξ» (x : π), c) 0 s x
theorem has_deriv_at_const {π : Type u} {F : Type v} [normed_space π F] (x : π) (c : F) :
has_deriv_at (Ξ» (x : π), c) 0 x
theorem deriv_const {π : Type u} {F : Type v} [normed_space π F] (x : π) (c : F) :
deriv (Ξ» (x : π), c) x = 0
@[simp]
theorem deriv_const' {π : Type u} {F : Type v} [normed_space π F] (c : F) :
deriv (Ξ» (x : π), c) = Ξ» (x : π), 0
theorem deriv_within_const {π : Type u} {F : Type v} [normed_space π F] (x : π) (s : set π) (c : F) (hxs : s x) :
deriv_within (Ξ» (x : π), c) s x = 0

### Continuity of a function admitting a derivative #

theorem has_deriv_at_filter.tendsto_nhds {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {L : filter π} (hL : L β€ nhds x) (h : x L) :
(nhds (f x))
theorem has_deriv_within_at.continuous_within_at {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s : set π} (h : s x) :
x
theorem has_deriv_at.continuous_at {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} (h : f' x) :
@[protected]
theorem has_deriv_at.continuous_on {π : Type u} {F : Type v} [normed_space π F] {s : set π} {f f' : π β F} (hderiv : β (x : π), x β s β (f' x) x) :