# mathlibdocumentation

analysis.calculus.deriv

# 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:

• `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
• sum of finitely many functions
• negation
• subtraction
• multiplication
• inverse `x β xβ»ΒΉ`
• multiplication of two functions in `π β π`
• multiplication of a function in `π β π` and of a function in `π β E`
• composition of a function in `π β F` with a function in `π β π`
• composition of a function in `F β E` with a function in `π β F`
• inverse function (assuming that it exists; the inverse function theorem is in `inverse.lean`)
• division
• polynomials

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_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_at_filter_iff_tendsto_slope {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {L : filter π} :

If the domain has dimension one, then FrΓ©chet derivative is equivalent to the classical definition with a limit. In this version we have to take the limit along the subset `-{x}`, because for `y=x` the slope equals zero due to the convention `0β»ΒΉ=0`.

theorem has_deriv_within_at_iff_tendsto_slope {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s : set π} :
s x β filter.tendsto (slope f x) (s \ {x})) (nhds f')
theorem has_deriv_within_at_iff_tendsto_slope' {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s : set π} (hs : x β s) :
s x β filter.tendsto (slope f x) s) (nhds f')
theorem has_deriv_at_iff_tendsto_slope {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} :
f' x β filter.tendsto (slope f x) {x}αΆ) (nhds f')
theorem has_deriv_within_at_congr_set {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s t u : set π} (hu : u β nhds x) (h : s β© u = t β© u) :
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 u : set π} (hu : u β nhds x) (h : s β© u = t β© u) :
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_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_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
@[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) (hs : s 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 π} (hs : s x) (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 : s x) (hL : β (y : π), y β s β fβ y = f y) (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

### Derivative of continuous linear maps #

@[protected]
theorem continuous_linear_map.has_deriv_at_filter {π : Type u} {F : Type v} [normed_space π F] {x : π} {L : filter π} (e : π βL[π] F) :
(βe 1) x L
@[protected]
theorem continuous_linear_map.has_strict_deriv_at {π : Type u} {F : Type v} [normed_space π F] {x : π} (e : π βL[π] F) :
(βe 1) x
@[protected]
theorem continuous_linear_map.has_deriv_at {π : Type u} {F : Type v} [normed_space π F] {x : π} (e : π βL[π] F) :
(βe 1) x
@[protected]
theorem continuous_linear_map.has_deriv_within_at {π : Type u} {F : Type v} [normed_space π F] {x : π} {s : set π} (e : π βL[π] F) :
(βe 1) s x
@[protected, simp]
theorem continuous_linear_map.deriv {π : Type u} {F : Type v} [normed_space π F] {x : π} (e : π βL[π] F) :
x = βe 1
@[protected]
theorem continuous_linear_map.deriv_within {π : Type u} {F : Type v} [normed_space π F] {x : π} {s : set π} (e : π βL[π] F) (hxs : s x) :
x = βe 1

### Derivative of bundled linear maps #

@[protected]
theorem linear_map.has_deriv_at_filter {π : Type u} {F : Type v} [normed_space π F] {x : π} {L : filter π} (e : π ββ[π] F) :
(βe 1) x L
@[protected]
theorem linear_map.has_strict_deriv_at {π : Type u} {F : Type v} [normed_space π F] {x : π} (e : π ββ[π] F) :
(βe 1) x
@[protected]
theorem linear_map.has_deriv_at {π : Type u} {F : Type v} [normed_space π F] {x : π} (e : π ββ[π] F) :
(βe 1) x
@[protected]
theorem linear_map.has_deriv_within_at {π : Type u} {F : Type v} [normed_space π F] {x : π} {s : set π} (e : π ββ[π] F) :
(βe 1) s x
@[protected, simp]
theorem linear_map.deriv {π : Type u} {F : Type v} [normed_space π F] {x : π} (e : π ββ[π] F) :
x = βe 1
@[protected]
theorem linear_map.deriv_within {π : Type u} {F : Type v} [normed_space π F] {x : π} {s : set π} (e : π ββ[π] F) (hxs : s x) :
x = βe 1

### Derivative of the sum of two functions #

theorem has_deriv_at_filter.add {π : Type u} {F : Type v} [normed_space π F] {f g : π β F} {f' g' : F} {x : π} {L : filter π} (hf : x L) (hg : x L) :
has_deriv_at_filter (Ξ» (y : π), f y + g y) (f' + g') x L
theorem has_strict_deriv_at.add {π : Type u} {F : Type v} [normed_space π F] {f g : π β F} {f' g' : F} {x : π} (hf : x) (hg : x) :
has_strict_deriv_at (Ξ» (y : π), f y + g y) (f' + g') x
theorem has_deriv_within_at.add {π : Type u} {F : Type v} [normed_space π F] {f g : π β F} {f' g' : F} {x : π} {s : set π} (hf : s x) (hg : s x) :
has_deriv_within_at (Ξ» (y : π), f y + g y) (f' + g') s x
theorem has_deriv_at.add {π : Type u} {F : Type v} [normed_space π F] {f g : π β F} {f' g' : F} {x : π} (hf : f' x) (hg : g' x) :
has_deriv_at (Ξ» (x : π), f x + g x) (f' + g') x
theorem deriv_within_add {π : Type u} {F : Type v} [normed_space π F] {f g : π β F} {x : π} {s : set π} (hxs : s x) (hf : f s x) (hg : g s x) :
deriv_within (Ξ» (y : π), f y + g y) s x = s x + s x
@[simp]
theorem deriv_add {π : Type u} {F : Type v} [normed_space π F] {f g : π β F} {x : π} (hf : f x) (hg : g x) :
deriv (Ξ» (y : π), f y + g y) x = x + x
theorem has_deriv_at_filter.add_const {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {L : filter π} (hf : x L) (c : F) :
has_deriv_at_filter (Ξ» (y : π), f y + c) f' x L
theorem has_deriv_within_at.add_const {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s : set π} (hf : s x) (c : F) :
has_deriv_within_at (Ξ» (y : π), f y + c) f' s x
theorem has_deriv_at.add_const {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} (hf : f' x) (c : F) :
has_deriv_at (Ξ» (x : π), f x + c) f' x
theorem deriv_within_add_const {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s : set π} (hxs : s x) (c : F) :
deriv_within (Ξ» (y : π), f y + c) s x = s x
theorem deriv_add_const {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} (c : F) :
deriv (Ξ» (y : π), f y + c) x = x
@[simp]
theorem deriv_add_const' {π : Type u} {F : Type v} [normed_space π F] {f : π β F} (c : F) :
deriv (Ξ» (y : π), f y + c) =
theorem has_deriv_at_filter.const_add {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {L : filter π} (c : F) (hf : x L) :
has_deriv_at_filter (Ξ» (y : π), c + f y) f' x L
theorem has_deriv_within_at.const_add {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s : set π} (c : F) (hf : s x) :
has_deriv_within_at (Ξ» (y : π), c + f y) f' s x
theorem has_deriv_at.const_add {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} (c : F) (hf : f' x) :
has_deriv_at (Ξ» (x : π), c + f x) f' x
theorem deriv_within_const_add {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s : set π} (hxs : s x) (c : F) :
deriv_within (Ξ» (y : π), c + f y) s x = s x
theorem deriv_const_add {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} (c : F) :
deriv (Ξ» (y : π), c + f y) x = x
@[simp]
theorem deriv_const_add' {π : Type u} {F : Type v} [normed_space π F] {f : π β F} (c : F) :
deriv (Ξ» (y : π), c + f y) =

### Derivative of a finite sum of functions #

theorem has_deriv_at_filter.sum {π : Type u} {F : Type v} [normed_space π F] {x : π} {L : filter π} {ΞΉ : Type u_1} {u : finset ΞΉ} {A : ΞΉ β π β F} {A' : ΞΉ β F} (h : β (i : ΞΉ), i β u β has_deriv_at_filter (A i) (A' i) x L) :
has_deriv_at_filter (Ξ» (y : π), u.sum (Ξ» (i : ΞΉ), A i y)) (u.sum (Ξ» (i : ΞΉ), A' i)) x L
theorem has_strict_deriv_at.sum {π : Type u} {F : Type v} [normed_space π F] {x : π} {ΞΉ : Type u_1} {u : finset ΞΉ} {A : ΞΉ β π β F} {A' : ΞΉ β F} (h : β (i : ΞΉ), i β u β has_strict_deriv_at (A i) (A' i) x) :
has_strict_deriv_at (Ξ» (y : π), u.sum (Ξ» (i : ΞΉ), A i y)) (u.sum (Ξ» (i : ΞΉ), A' i)) x
theorem has_deriv_within_at.sum {π : Type u} {F : Type v} [normed_space π F] {x : π} {s : set π} {ΞΉ : Type u_1} {u : finset ΞΉ} {A : ΞΉ β π β F} {A' : ΞΉ β F} (h : β (i : ΞΉ), i β u β has_deriv_within_at (A i) (A' i) s x) :
has_deriv_within_at (Ξ» (y : π), u.sum (Ξ» (i : ΞΉ), A i y)) (u.sum (Ξ» (i : ΞΉ), A' i)) s x
theorem has_deriv_at.sum {π : Type u} {F : Type v} [normed_space π F] {x : π} {ΞΉ : Type u_1} {u : finset ΞΉ} {A : ΞΉ β π β F} {A' : ΞΉ β F} (h : β (i : ΞΉ), i β u β has_deriv_at (A i) (A' i) x) :
has_deriv_at (Ξ» (y : π), u.sum (Ξ» (i : ΞΉ), A i y)) (u.sum (Ξ» (i : ΞΉ), A' i)) x
theorem deriv_within_sum {π : Type u} {F : Type v} [normed_space π F] {x : π} {s : set π} {ΞΉ : Type u_1} {u : finset ΞΉ} {A : ΞΉ β π β F} (hxs : s x) (h : β (i : ΞΉ), i β u β (A i) s x) :
deriv_within (Ξ» (y : π), u.sum (Ξ» (i : ΞΉ), A i y)) s x = u.sum (Ξ» (i : ΞΉ), deriv_within (A i) s x)
@[simp]
theorem deriv_sum {π : Type u} {F : Type v} [normed_space π F] {x : π} {ΞΉ : Type u_1} {u : finset ΞΉ} {A : ΞΉ β π β F} (h : β (i : ΞΉ), i β u β (A i) x) :
deriv (Ξ» (y : π), u.sum (Ξ» (i : ΞΉ), A i y)) x = u.sum (Ξ» (i : ΞΉ), deriv (A i) x)

### Derivatives of functions `f : π β Ξ  i, E i`#

@[simp]
theorem has_strict_deriv_at_pi {π : Type u} {x : π} {ΞΉ : Type u_1} [fintype ΞΉ] {E' : ΞΉ β Type u_2} [Ξ  (i : ΞΉ), normed_add_comm_group (E' i)] [Ξ  (i : ΞΉ), normed_space π (E' i)] {Ο : π β Ξ  (i : ΞΉ), E' i} {Ο' : Ξ  (i : ΞΉ), E' i} :
Ο' x β β (i : ΞΉ), has_strict_deriv_at (Ξ» (x : π), Ο x i) (Ο' i) x
@[simp]
theorem has_deriv_at_filter_pi {π : Type u} {x : π} {L : filter π} {ΞΉ : Type u_1} [fintype ΞΉ] {E' : ΞΉ β Type u_2} [Ξ  (i : ΞΉ), normed_add_comm_group (E' i)] [Ξ  (i : ΞΉ), normed_space π (E' i)] {Ο : π β Ξ  (i : ΞΉ), E' i} {Ο' : Ξ  (i : ΞΉ), E' i} :
Ο' x L β β (i : ΞΉ), has_deriv_at_filter (Ξ» (x : π), Ο x i) (Ο' i) x L
theorem has_deriv_at_pi {π : Type u} {x : π} {ΞΉ : Type u_1} [fintype ΞΉ] {E' : ΞΉ β Type u_2} [Ξ  (i : ΞΉ), normed_add_comm_group (E' i)] [Ξ  (i : ΞΉ), normed_space π (E' i)] {Ο : π β Ξ  (i : ΞΉ), E' i} {Ο' : Ξ  (i : ΞΉ), E' i} :
Ο' x β β (i : ΞΉ), has_deriv_at (Ξ» (x : π), Ο x i) (Ο' i) x
theorem has_deriv_within_at_pi {π : Type u} {x : π} {s : set π} {ΞΉ : Type u_1} [fintype ΞΉ] {E' : ΞΉ β Type u_2} [Ξ  (i : ΞΉ), normed_add_comm_group (E' i)] [Ξ  (i : ΞΉ), normed_space π (E' i)] {Ο : π β Ξ  (i : ΞΉ), E' i} {Ο' : Ξ  (i : ΞΉ), E' i} :
Ο' s x β β (i : ΞΉ), has_deriv_within_at (Ξ» (x : π), Ο x i) (Ο' i) s x
theorem deriv_within_pi {π : Type u} {x : π} {s : set π} {ΞΉ : Type u_1} [fintype ΞΉ] {E' : ΞΉ β Type u_2} [Ξ  (i : ΞΉ), normed_add_comm_group (E' i)] [Ξ  (i : ΞΉ), normed_space π (E' i)] {Ο : π β Ξ  (i : ΞΉ), E' i} (h : β (i : ΞΉ), (Ξ» (x : π), Ο x i) s x) (hs : s x) :
s x = Ξ» (i : ΞΉ), deriv_within (Ξ» (x : π), Ο x i) s x
theorem deriv_pi {π : Type u} {x : π} {ΞΉ : Type u_1} [fintype ΞΉ] {E' : ΞΉ β Type u_2} [Ξ  (i : ΞΉ), normed_add_comm_group (E' i)] [Ξ  (i : ΞΉ), normed_space π (E' i)] {Ο : π β Ξ  (i : ΞΉ), E' i} (h : β (i : ΞΉ), (Ξ» (x : π), Ο x i) x) :
deriv Ο x = Ξ» (i : ΞΉ), deriv (Ξ» (x : π), Ο x i) x

### Derivative of the multiplication of a scalar function and a vector function #

theorem has_deriv_within_at.smul {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s : set π} {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] [normed_space π' F] [is_scalar_tower π π' F] {c : π β π'} {c' : π'} (hc : s x) (hf : s x) :
has_deriv_within_at (Ξ» (y : π), c y β’ f y) (c x β’ f' + c' β’ f x) s x
theorem has_deriv_at.smul {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] [normed_space π' F] [is_scalar_tower π π' F] {c : π β π'} {c' : π'} (hc : c' x) (hf : f' x) :
has_deriv_at (Ξ» (y : π), c y β’ f y) (c x β’ f' + c' β’ f x) x
theorem has_strict_deriv_at.smul {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] [normed_space π' F] [is_scalar_tower π π' F] {c : π β π'} {c' : π'} (hc : x) (hf : x) :
has_strict_deriv_at (Ξ» (y : π), c y β’ f y) (c x β’ f' + c' β’ f x) x
theorem deriv_within_smul {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s : set π} {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] [normed_space π' F] [is_scalar_tower π π' F] {c : π β π'} (hxs : s x) (hc : c s x) (hf : f s x) :
deriv_within (Ξ» (y : π), c y β’ f y) s x = c x β’ s x + s x β’ f x
theorem deriv_smul {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] [normed_space π' F] [is_scalar_tower π π' F] {c : π β π'} (hc : c x) (hf : f x) :
deriv (Ξ» (y : π), c y β’ f y) x = c x β’ x + x β’ f x
theorem has_strict_deriv_at.smul_const {π : Type u} {F : Type v} [normed_space π F] {x : π} {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] [normed_space π' F] [is_scalar_tower π π' F] {c : π β π'} {c' : π'} (hc : x) (f : F) :
has_strict_deriv_at (Ξ» (y : π), c y β’ f) (c' β’ f) x
theorem has_deriv_within_at.smul_const {π : Type u} {F : Type v} [normed_space π F] {x : π} {s : set π} {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] [normed_space π' F] [is_scalar_tower π π' F] {c : π β π'} {c' : π'} (hc : s x) (f : F) :
has_deriv_within_at (Ξ» (y : π), c y β’ f) (c' β’ f) s x
theorem has_deriv_at.smul_const {π : Type u} {F : Type v} [normed_space π F] {x : π} {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] [normed_space π' F] [is_scalar_tower π π' F] {c : π β π'} {c' : π'} (hc : c' x) (f : F) :
has_deriv_at (Ξ» (y : π), c y β’ f) (c' β’ f) x
theorem deriv_within_smul_const {π : Type u} {F : Type v} [normed_space π F] {x : π} {s : set π} {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] [normed_space π' F] [is_scalar_tower π π' F] {c : π β π'} (hxs : s x) (hc : c s x) (f : F) :
deriv_within (Ξ» (y : π), c y β’ f) s x = s x β’ f
theorem deriv_smul_const {π : Type u} {F : Type v} [normed_space π F] {x : π} {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] [normed_space π' F] [is_scalar_tower π π' F] {c : π β π'} (hc : c x) (f : F) :
deriv (Ξ» (y : π), c y β’ f) x = x β’ f
theorem has_strict_deriv_at.const_smul {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {R : Type u_1} [semiring R] [ F] [smul_comm_class π R F] (c : R) (hf : x) :
has_strict_deriv_at (Ξ» (y : π), c β’ f y) (c β’ f') x
theorem has_deriv_at_filter.const_smul {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {L : filter π} {R : Type u_1} [semiring R] [ F] [smul_comm_class π R F] (c : R) (hf : x L) :
has_deriv_at_filter (Ξ» (y : π), c β’ f y) (c β’ f') x L
theorem has_deriv_within_at.const_smul {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s : set π} {R : Type u_1} [semiring R] [ F] [smul_comm_class π R F] (c : R) (hf : s x) :
has_deriv_within_at (Ξ» (y : π), c β’ f y) (c β’ f') s x
theorem has_deriv_at.const_smul {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {R : Type u_1} [semiring R] [ F] [smul_comm_class π R F] (c : R) (hf : f' x) :
has_deriv_at (Ξ» (y : π), c β’ f y) (c β’ f') x
theorem deriv_within_const_smul {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s : set π} {R : Type u_1} [semiring R] [ F] [smul_comm_class π R F] (hxs : s x) (c : R) (hf : f s x) :
deriv_within (Ξ» (y : π), c β’ f y) s x = c β’ s x
theorem deriv_const_smul {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {R : Type u_1} [semiring R] [ F] [smul_comm_class π R F] (c : R) (hf : f x) :
deriv (Ξ» (y : π), c β’ f y) x = c β’ x

### Derivative of the negative of a function #

theorem has_deriv_at_filter.neg {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {L : filter π} (h : x L) :
has_deriv_at_filter (Ξ» (x : π), -f x) (-f') x L
theorem has_deriv_within_at.neg {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s : set π} (h : s x) :
has_deriv_within_at (Ξ» (x : π), -f x) (-f') s x
theorem has_deriv_at.neg {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} (h : f' x) :
has_deriv_at (Ξ» (x : π), -f x) (-f') x
theorem has_strict_deriv_at.neg {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} (h : x) :
has_strict_deriv_at (Ξ» (x : π), -f x) (-f') x
theorem deriv_within.neg {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s : set π} (hxs : s x) :
deriv_within (Ξ» (y : π), -f y) s x = - s x
theorem deriv.neg {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} :
deriv (Ξ» (y : π), -f y) x = - x
@[simp]
theorem deriv.neg' {π : Type u} {F : Type v} [normed_space π F] {f : π β F} :
deriv (Ξ» (y : π), -f y) = Ξ» (x : π), - x

### Derivative of the negation function (i.e `has_neg.neg`) #

theorem has_deriv_at_filter_neg {π : Type u} (x : π) (L : filter π) :
L
theorem has_deriv_within_at_neg {π : Type u} (x : π) (s : set π) :
x
theorem has_deriv_at_neg {π : Type u} (x : π) :
x
theorem has_deriv_at_neg' {π : Type u} (x : π) :
has_deriv_at (Ξ» (x : π), -x) (-1) x
theorem has_strict_deriv_at_neg {π : Type u} (x : π) :
theorem deriv_neg {π : Type u} (x : π) :
= -1
@[simp]
theorem deriv_neg' {π : Type u}  :
= Ξ» (_x : π), -1
@[simp]
theorem deriv_neg'' {π : Type u} (x : π) :
deriv (Ξ» (x : π), -x) x = -1
theorem deriv_within_neg {π : Type u} (x : π) (s : set π) (hxs : s x) :
= -1
theorem differentiable_neg {π : Type u}  :
theorem differentiable_on_neg {π : Type u} (s : set π) :
s

### Derivative of the difference of two functions #

theorem has_deriv_at_filter.sub {π : Type u} {F : Type v} [normed_space π F] {f g : π β F} {f' g' : F} {x : π} {L : filter π} (hf : x L) (hg : x L) :
has_deriv_at_filter (Ξ» (x : π), f x - g x) (f' - g') x L
theorem has_deriv_within_at.sub {π : Type u} {F : Type v} [normed_space π F] {f g : π β F} {f' g' : F} {x : π} {s : set π} (hf : s x) (hg : s x) :
has_deriv_within_at (Ξ» (x : π), f x - g x) (f' - g') s x
theorem has_deriv_at.sub {π : Type u} {F : Type v} [normed_space π F] {f g : π β F} {f' g' : F} {x : π} (hf : f' x) (hg : g' x) :
has_deriv_at (Ξ» (x : π), f x - g x) (f' - g') x
theorem has_strict_deriv_at.sub {π : Type u} {F : Type v} [normed_space π F] {f g : π β F} {f' g' : F} {x : π} (hf : x) (hg : x) :
has_strict_deriv_at (Ξ» (x : π), f x - g x) (f' - g') x
theorem deriv_within_sub {π : Type u} {F : Type v} [normed_space π F] {f g : π β F} {x : π} {s : set π} (hxs : s x) (hf : f s x) (hg : g s x) :
deriv_within (Ξ» (y : π), f y - g y) s x = s x - s x
@[simp]
theorem deriv_sub {π : Type u} {F : Type v} [normed_space π F] {f g : π β F} {x : π} (hf : f x) (hg : g x) :
deriv (Ξ» (y : π), f y - g y) x = x - x
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_deriv_at_filter.sub_const {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {L : filter π} (hf : x L) (c : F) :
has_deriv_at_filter (Ξ» (x : π), f x - c) f' x L
theorem has_deriv_within_at.sub_const {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s : set π} (hf : s x) (c : F) :
has_deriv_within_at (Ξ» (x : π), f x - c) f' s x
theorem has_deriv_at.sub_const {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} (hf : f' x) (c : F) :
has_deriv_at (Ξ» (x : π), f x - c) f' x
theorem deriv_within_sub_const {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s : set π} (hxs : s x) (c : F) :
deriv_within (Ξ» (y : π), f y - c) s x = s x
theorem deriv_sub_const {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} (c : F) :
deriv (Ξ» (y : π), f y - c) x = x
theorem has_deriv_at_filter.const_sub {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {L : filter π} (c : F) (hf : x L) :
has_deriv_at_filter (Ξ» (x : π), c - f x) (-f') x L
theorem has_deriv_within_at.const_sub {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} {s : set π} (c : F) (hf : s x) :
has_deriv_within_at (Ξ» (x : π), c - f x) (-f') s x
theorem has_strict_deriv_at.const_sub {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} (c : F) (hf : x) :
has_strict_deriv_at (Ξ» (x : π), c - f x) (-f') x
theorem has_deriv_at.const_sub {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {f' : F} {x : π} (c : F) (hf : f' x) :
has_deriv_at (Ξ» (x : π), c - f x) (-f') x
theorem deriv_within_const_sub {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} {s : set π} (hxs : s x) (c : F) :
deriv_within (Ξ» (y : π), c - f y) s x = - s x
theorem deriv_const_sub {π : Type u} {F : Type v} [normed_space π F] {f : π β F} {x : π} (c : F) :
deriv (Ξ» (y : π), c - f y) x = - x

### 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) :

### Derivative of the cartesian product of two functions #

theorem has_deriv_at_filter.prod {π : Type u} {F : Type v} [normed_space π F] {fβ : π β F} {fβ' : F} {x : π} {L : filter π} {G : Type w} [normed_space π G] {fβ : π β G} {fβ' : G} (hfβ : fβ' x L) (hfβ : fβ' x L) :
has_deriv_at_filter (Ξ» (x : π), (fβ x, fβ x)) (fβ', fβ') x L
theorem has_deriv_within_at.prod {π : Type u} {F : Type v} [normed_space π F] {fβ : π β F} {fβ' : F} {x : π} {s : set π} {G : Type w} [normed_space π G] {fβ : π β G} {fβ' : G} (hfβ : fβ' s x) (hfβ : fβ' s x) :
has_deriv_within_at (Ξ» (x : π), (fβ x, fβ x)) (fβ', fβ') s x
theorem has_deriv_at.prod {π : Type u} {F : Type v} [normed_space π F] {fβ : π β F} {fβ' : F} {x : π} {G : Type w} [normed_space π G] {fβ : π β G} {fβ' : G} (hfβ : has_deriv_at fβ fβ' x) (hfβ : has_deriv_at fβ fβ' x) :
has_deriv_at (Ξ» (x : π), (fβ x, fβ x)) (fβ', fβ') x
theorem has_strict_deriv_at.prod {π : Type u} {F : Type v} [normed_space π F] {fβ : π β F} {fβ' : F} {x : π} {G : Type w} [normed_space π G] {fβ : π β G} {fβ' : G} (hfβ : fβ' x) (hfβ : fβ' x) :
has_strict_deriv_at (Ξ» (x : π), (fβ x, fβ x)) (fβ', fβ') x

### Derivative of the composition of a vector function and a scalar function #

We use `scomp` in lemmas on composition of vector valued and scalar valued functions, and `comp` in lemmas on composition of scalar valued functions, in analogy for `smul` and `mul` (and also because the `comp` version with the shorter name will show up much more often in applications). The formula for the derivative involves `smul` in `scomp` lemmas, which can be reduced to usual multiplication in `comp` lemmas.

theorem has_deriv_at_filter.scomp {π : Type u} {F : Type v} [normed_space π F] (x : π) {L : filter π} {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] [normed_space π' F] [is_scalar_tower π π' F] {h : π β π'} {h' : π'} {gβ : π' β F} {gβ' : F} {L' : filter π'} (hg : gβ' (h x) L') (hh : x L) (hL : L') :
has_deriv_at_filter (gβ β h) (h' β’ gβ') x L
theorem has_deriv_within_at.scomp_has_deriv_at {π : Type u} {F : Type v} [normed_space π F] (x : π) {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] [normed_space π' F] [is_scalar_tower π π' F] {s' : set π'} {h : π β π'} {h' : π'} {gβ : π' β F} {gβ' : F} (hg : gβ' s' (h x)) (hh : h' x) (hs : β (x : π), h x β s') :
has_deriv_at (gβ β h) (h' β’ gβ') x
theorem has_deriv_within_at.scomp {π : Type u} {F : Type v} [normed_space π F] (x : π) {s : set π} {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] [normed_space π' F] [is_scalar_tower π π' F] {t' : set π'} {h : π β π'} {h' : π'} {gβ : π' β F} {gβ' : F} (hg : gβ' t' (h x)) (hh : s x) (hst : s t') :
has_deriv_within_at (gβ β h) (h' β’ gβ') s x
theorem has_deriv_at.scomp {π : Type u} {F : Type v} [normed_space π F] (x : π) {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] [normed_space π' F] [is_scalar_tower π π' F] {h : π β π'} {h' : π'} {gβ : π' β F} {gβ' : F} (hg : has_deriv_at gβ gβ' (h x)) (hh : h' x) :
has_deriv_at (gβ β h) (h' β’ gβ') x

The chain rule.

theorem has_strict_deriv_at.scomp {π : Type u} {F : Type v} [normed_space π F] (x : π) {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] [normed_space π' F] [is_scalar_tower π π' F] {h : π β π'} {h' : π'} {gβ : π' β F} {gβ' : F} (hg : gβ' (h x)) (hh : x) :
has_strict_deriv_at (gβ β h) (h' β’ gβ') x
theorem has_deriv_at.scomp_has_deriv_within_at {π : Type u} {F : Type v} [normed_space π F] (x : π) {s : set π} {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] [normed_space π' F] [is_scalar_tower π π' F] {h : π β π'} {h' : π'} {gβ : π' β F} {gβ' : F} (hg : has_deriv_at gβ gβ' (h x)) (hh : s x) :
has_deriv_within_at (gβ β h) (h' β’ gβ') s x
theorem deriv_within.scomp {π : Type u} {F : Type v} [normed_space π F] (x : π) {s : set π} {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] [normed_space π' F] [is_scalar_tower π π' F] {t' : set π'} {h : π β π'} {gβ : π' β F} (hg : gβ t' (h x)) (hh : h s x) (hs : s t') (hxs : s x) :
deriv_within (gβ β h) s x = s x β’ deriv_within gβ t' (h x)
theorem deriv.scomp {π : Type u} {F : Type v} [normed_space π F] (x : π) {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] [normed_space π' F] [is_scalar_tower π π' F] {h : π β π'} {gβ : π' β F} (hg : differentiable_at π' gβ (h x)) (hh : h x) :
deriv (gβ β h) x = x β’ deriv gβ (h x)

### Derivative of the composition of a scalar and vector functions #

theorem has_deriv_at_filter.comp_has_fderiv_at_filter {π : Type u} {E : Type w} [normed_space π E] {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] {hβ : π' β π'} {hβ' : π'} {L' : filter π'} {f : E β π'} {f' : E βL[π] π'} (x : E) {L'' : filter E} (hhβ : hβ' (f x) L') (hf : x L'') (hL : L'' L') :
has_fderiv_at_filter (hβ β f) (hβ' β’ f') x L''
theorem has_strict_deriv_at.comp_has_strict_fderiv_at {π : Type u} {E : Type w} [normed_space π E] {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] {hβ : π' β π'} {hβ' : π'} {f : E β π'} {f' : E βL[π] π'} (x : E) (hh : hβ' (f x)) (hf : x) :
has_strict_fderiv_at (hβ β f) (hβ' β’ f') x
theorem has_deriv_at.comp_has_fderiv_at {π : Type u} {E : Type w} [normed_space π E] {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] {hβ : π' β π'} {hβ' : π'} {f : E β π'} {f' : E βL[π] π'} (x : E) (hh : has_deriv_at hβ hβ' (f x)) (hf : f' x) :
has_fderiv_at (hβ β f) (hβ' β’ f') x
theorem has_deriv_at.comp_has_fderiv_within_at {π : Type u} {E : Type w} [normed_space π E] {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] {hβ : π' β π'} {hβ' : π'} {f : E β π'} {f' : E βL[π] π'} {s : set E} (x : E) (hh : has_deriv_at hβ hβ' (f x)) (hf : s x) :
has_fderiv_within_at (hβ β f) (hβ' β’ f') s x
theorem has_deriv_within_at.comp_has_fderiv_within_at {π : Type u} {E : Type w} [normed_space π E] {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] {hβ : π' β π'} {hβ' : π'} {f : E β π'} {f' : E βL[π] π'} {s : set E} {t : set π'} (x : E) (hh : hβ' t (f x)) (hf : s x) (hst : s t) :
has_fderiv_within_at (hβ β f) (hβ' β’ f') s x

### Derivative of the composition of two scalar functions #

theorem has_deriv_at_filter.comp {π : Type u} (x : π) {L : filter π} {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] {h : π β π'} {hβ : π' β π'} {h' hβ' : π'} {L' : filter π'} (hhβ : hβ' (h x) L') (hh : x L) (hL : L') :
has_deriv_at_filter (hβ β h) (hβ' * h') x L
theorem has_deriv_within_at.comp {π : Type u} (x : π) {s : set π} {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] {s' : set π'} {h : π β π'} {hβ : π' β π'} {h' hβ' : π'} (hhβ : hβ' s' (h x)) (hh : s x) (hst : s s') :
has_deriv_within_at (hβ β h) (hβ' * h') s x
theorem has_deriv_at.comp {π : Type u} (x : π) {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] {h : π β π'} {hβ : π' β π'} {h' hβ' : π'} (hhβ : has_deriv_at hβ hβ' (h x)) (hh : h' x) :
has_deriv_at (hβ β h) (hβ' * h') x

The chain rule.

theorem has_strict_deriv_at.comp {π : Type u} (x : π) {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] {h : π β π'} {hβ : π' β π'} {h' hβ' : π'} (hhβ : hβ' (h x)) (hh : x) :
has_strict_deriv_at (hβ β h) (hβ' * h') x
theorem has_deriv_at.comp_has_deriv_within_at {π : Type u} (x : π) {s : set π} {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] {h : π β π'} {hβ : π' β π'} {h' hβ' : π'} (hhβ : has_deriv_at hβ hβ' (h x)) (hh : s x) :
has_deriv_within_at (hβ β h) (hβ' * h') s x
theorem deriv_within.comp {π : Type u} (x : π) {s : set π} {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] {s' : set π'} {h : π β π'} {hβ : π' β π'} (hhβ : hβ s' (h x)) (hh : h s x) (hs : s s') (hxs : s x) :
deriv_within (hβ β h) s x = deriv_within hβ s' (h x) * s x
theorem deriv.comp {π : Type u} (x : π) {π' : Type u_1} [nontrivially_normed_field π'] [normed_algebra π π'] {h : π β π'} {hβ : π' β π'} (hhβ : differentiable_at π' hβ (h x)) (hh : h x) :
deriv (hβ β h) x = deriv hβ (h x) * x
@[protected]
theorem has_deriv_at_filter.iterate {π : Type u} (x : π) {L : filter π} {f : π β π} {f' : π} (hf : x L) (hL : L) (hx : f x = x) (n : β) :
(f' ^ n) x L
@[protected]
theorem has_deriv_at.iterate {π : Type u} (x : π) {f : π β π} {f' : π} (hf : f' x) (hx : f x = x) (n : β) :
(f' ^ n) x
@[protected]
theorem has_deriv_within_at.iterate {π : Type u} (x : π) {s : set π} {f : π β π} {f' : π} (hf : s x) (hx : f x = x) (hs : s s) (n : β) :
(f' ^ n) s x
@[protected]
theorem has_strict_deriv_at.iterate {π : Type u} (x : π) {f : π β π} {f' : π} (hf : x) (hx : f x = x) (n : β) :
(f' ^ n) x

### Derivative of the composition of a function between vector spaces and a function on `π`#

theorem has_fderiv_within_at.comp_has_deriv_within_at {π : Type u} {F : Type v} [normed_space π F] {E : Type w} [normed_space π E] {f : π β F} {f' : F} (x : π) {s : set π} {l : F β E} {l' : F βL[π] E} {t : set F} (hl : t (f x)) (hf : s x) (hst : s t) :

The composition `l β f` where `l : F β E` and `f : π β F`, has a derivative within a set equal to the FrΓ©chet derivative of `l` applied to the derivative of `f`.

theorem has_fderiv_at.comp_has_deriv_within_at {π : Type u} {F : Type v} [normed_space π F] {E : Type w} [normed_space π E] {f : π β F} {f' : F} (x : π) {s : set π} {l : F β E} {l' : F βL[π] E} (hl : l' (f x)) (hf : s x) :
theorem has_fderiv_at.comp_has_deriv_at {π : Type u} {F : Type v} [normed_space π F] {E : Type w} [normed_space π E] {f : π β F} {f' : F} (x : π) {l : F β E} {l' : F βL[π] E} (hl : l' (f x)) (hf : f' x) :
has_deriv_at (l β f) (βl' f') x

The composition `l β f` where `l : F β E` and `f : π β F`, has a derivative equal to the FrΓ©chet derivative of `l` applied to the derivative of `f`.

theorem has_strict_fderiv_at.comp_has_strict_deriv_at {π : Type u} {F : Type v} [normed_space π F] {E : Type w} [normed_space π E] {f : π β F} {f' : F} (x : π) {l : F β E} {l' : F βL[π] E} (hl : (f x)) (hf : x) :
theorem fderiv_within.comp_deriv_within {π : Type u} {F : Type v} [normed_space π F] {E : Type w} [normed_space π E] {f : π β F} (x : π) {s : set π} {l : F β E} {t : set F} (hl : l t (f x)) (hf : f s x) (hs : s t) (hxs : s x) :
deriv_within (l β f) s x = β(fderiv_within π l t (f x)) s x)
theorem fderiv.comp_deriv {π : Type u} {F : Type v} [normed_space π F] {E : Type w} [normed_space π E] {f : π β F} (x : π) {l : F β E} (hl : l (f x)) (hf : f x) :
deriv (l β f) x = β(fderiv π l (f x)) (deriv f x)

### Derivative of the multiplication of two functions #

theorem has_deriv_within_at.mul {π : Type u} {x : π} {s : set π} {πΈ : Type u_2} [normed_ring πΈ] [normed_algebra π πΈ] {c d : π β πΈ} {c' d' : πΈ} (hc : s x) (hd : s x) :
has_deriv_within_at (Ξ» (y : π), c y * d y) (c' * d x + c x * d') s x
theorem has_deriv_at.mul {π : Type u} {x : π} {πΈ : Type u_2} [normed_ring πΈ] [normed_algebra π πΈ] {c d : π β πΈ} {c' d' : πΈ} (hc : c' x) (hd : d' x) :
has_deriv_at (Ξ» (y : π), c y * d y) (c' * d x + c x * d') x
theorem has_strict_deriv_at.mul {π : Type u} {x : π} {πΈ : Type u_2} [normed_ring πΈ] [normed_algebra π πΈ] {c d : π β πΈ} {c' d' : πΈ} (hc : x) (hd : x) :
has_strict_deriv_at (Ξ» (y : π), c y * d y) (c' * d x + c x * d') x
theorem deriv_within_mul {π : Type u} {x : π} {s : set π} {πΈ : Type u_2} [normed_ring πΈ] [normed_algebra π πΈ] {c d : π β πΈ} (hxs : s x) (hc : c s x) (hd : d s x) :
deriv_within (Ξ» (y : π), c y * d y) s x = s x * d x + c x * s x
@[simp]
theorem deriv_mul {π : Type u} {x : π} {πΈ : Type u_2} [normed_ring πΈ] [normed_algebra π πΈ] {c d : π β πΈ} (hc : c x) (hd : d x) :
deriv (Ξ» (y : π), c y * d y) x = x * d x + c x * x
theorem has_deriv_within_at.mul_const {π : Type u} {x : π} {s : set π} {πΈ : Type u_2} [normed_ring πΈ] [normed_algebra π πΈ] {c : π β πΈ} {c' : πΈ} (hc : s x) (d : πΈ) :
has_deriv_within_at (Ξ» (y : π), c y * d) (c' * d) s x
theorem has_deriv_at.mul_const {π : Type u} {x : π} {πΈ : Type u_2} [normed_ring πΈ] [normed_algebra π πΈ] {c : π β πΈ} {c' : πΈ} (hc : c' x) (d : πΈ) :
has_deriv_at (Ξ» (y : π), c y * d) (c' * d) x
theorem has_deriv_at_mul_const {π : Type u} {x : π} (c : π) :
has_deriv_at (Ξ» (x : π), x * c) c x
theorem has_strict_deriv_at.mul_const {π : Type u} {x : π} {πΈ : Type u_2} [normed_ring πΈ] [normed_algebra π πΈ] {c : π β πΈ} {c' : πΈ} (hc : x) (d : πΈ) :
has_strict_deriv_at (Ξ» (y : π), c y * d) (c' * d) x
theorem deriv_within_mul_const {π : Type u} {x : π} {s : set π} {πΈ : Type u_2} [normed_ring πΈ] [normed_algebra π πΈ] {c : π β πΈ} (hxs : s x) (hc : c s x) (d : πΈ) :
deriv_within (Ξ» (y : π), c y * d) s x = s x * d
theorem deriv_mul_const {π : Type u} {x : π} {πΈ : Type u_2} [normed_ring πΈ] [normed_algebra π πΈ] {c : π β πΈ} (hc : c x) (d : πΈ) :
deriv (Ξ» (y : π), c y * d) x = x * d
theorem deriv_mul_const_field {π : Type u} {x : π} {π' : Type u_1} [normed_field π'] [normed_algebra π π'] {u : π β π'} (v : π') :
deriv (Ξ» (y : π), u y * v) x = x * v
@[simp]
theorem deriv_mul_const_field' {π : Type u} {π' : Type u_1} [normed_field π'] [normed_algebra π π'] {u : π β π'} (v : π') :
deriv (Ξ» (x : π), u x * v) = Ξ» (x : π), x * v
theorem has_deriv_within_at.const_mul {π : Type u} {x : π} {s : set π} {πΈ : Type u_2} [normed_ring πΈ] [normed_algebra π πΈ] {d : π β πΈ} {d' : πΈ} (c : πΈ) (hd : s x) :
has_deriv_within_at (Ξ» (y : π), c * d y) (c * d') s x
theorem has_deriv_at.const_mul {π : Type u} {x : π} {πΈ : Type u_2} [normed_ring πΈ] [normed_algebra π πΈ] {d : π β πΈ} {d' : πΈ} (c : πΈ) (hd : d' x) :
has_deriv_at (Ξ» (y : π), c * d y) (c * d') x
theorem has_strict_deriv_at.const_mul {π : Type u} {x : π} {πΈ : Type u_2} [normed_ring πΈ] [normed_algebra π πΈ] {d : π β πΈ} {d' : πΈ} (c : πΈ) (hd : x) :
has_strict_deriv_at (Ξ» (y : π), c * d y) (c * d') x
theorem deriv_within_const_mul {π : Type u} {x : π} {s : set π} {πΈ : Type u_2} [normed_ring πΈ] [normed_algebra π πΈ] {d : π β πΈ} (hxs : s x) (c : πΈ) (hd : d s x) :
deriv_within (Ξ» (y : π), c * d y) s x = c * s x
theorem deriv_const_mul {π : Type u} {x : π} {πΈ : Type u_2} [normed_ring πΈ] [normed_algebra π πΈ] {d : π β πΈ} (c : πΈ) (hd : d x) :
deriv (Ξ» (y : π), c * d y) x = c * x
theorem deriv_const_mul_field {π : Type u} {x : π} {π' : Type u_1} [normed_field π'] [normed_algebra π π'] {v : π β π'} (u : π') :
deriv (Ξ» (y : π), u * v y) x = u * x
@[simp]
theorem deriv_const_mul_field' {π : Type u} {π' : Type u_1} [normed_field π'] [normed_algebra π π'] {v : π β π'} (u : π') :
deriv (Ξ» (x : π), u * v x) = Ξ» (x : π), u * x

### Derivative of `x β¦ xβ»ΒΉ`#

theorem has_strict_deriv_at_inv {π : Type u} {x : π} (hx : x β  0) :
x
theorem has_deriv_at_inv {π : Type u} {x : π} (x_ne_zero : x β  0) :
has_deriv_at (Ξ» (y : π), yβ»ΒΉ) (-(x ^ 2)β»ΒΉ) x
theorem has_deriv_within_at_inv {π : Type u} {x : π} (x_ne_zero : x β  0) (s : set π) :
has_deriv_within_at (Ξ» (x : π), xβ»ΒΉ) (-(x ^ 2)β»ΒΉ) s x
theorem differentiable_at_inv {π : Type u} {x : π} :
(Ξ» (x : π), xβ»ΒΉ) x β x β  0
theorem differentiable_within_at_inv {π : Type u} {x : π} {s : set π} (x_ne_zero : x β  0) :
(Ξ» (x : π), xβ»ΒΉ) s x
theorem differentiable_on_inv {π : Type u}  :
(Ξ» (x : π), xβ»ΒΉ) {x : π | x β  0}
theorem deriv_inv {π : Type u} {x : π} :
deriv (Ξ» (x : π), xβ»ΒΉ) x = -(x ^ 2)β»ΒΉ
@[simp]
theorem deriv_inv' {π : Type u}  :
deriv (Ξ» (x : π), xβ»ΒΉ) = Ξ» (x : π), -(x ^ 2)β»ΒΉ
theorem deriv_within_inv {π : Type u} {x : π} {s : set π} (x_ne_zero : x β  0) (hxs : s x) :
deriv_within (Ξ» (x : π), xβ»ΒΉ) s x = -(x ^ 2)β»ΒΉ
theorem has_fderiv_at_inv {π : Type u} {x : π} (x_ne_zero : x β  0) :
has_fderiv_at (Ξ» (x : π), xβ»ΒΉ) (1.smul_right (-(x ^ 2)β»ΒΉ)) x
theorem has_fderiv_within_at_inv {π : Type u} {x : π} {s : set π} (x_ne_zero : x β  0) :
has_fderiv_within_at (Ξ» (x : π), xβ»ΒΉ) (1.smul_right (-(x ^ 2)β»ΒΉ)) s x
theorem fderiv_inv {π : Type u} {x : π} :
fderiv π (Ξ» (x : π), xβ»ΒΉ) x = 1.smul_right (-(x ^ 2)β»ΒΉ)
theorem fderiv_within_inv {π : Type u} {x : π} {s : set π} (x_ne_zero : x β  0) (hxs : s x) :
fderiv_within π (Ξ» (x : π), xβ»ΒΉ) s x = 1.smul_right (-(x ^ 2)β»ΒΉ)
theorem has_deriv_within_at.inv {π : Type u} {x : π} {s : set π} {c : π β π} {c' : π} (hc : s x) (hx : c x β  0) :
has_deriv_within_at (Ξ» (y : π), (c y)β»ΒΉ) (-c' / c x ^ 2) s x
theorem has_deriv_at.inv {π : Type u} {x : π} {c : π β π} {c' : π} (hc : c' x) (hx : c x β  0) :
has_deriv_at (Ξ» (y : π), (c y)β»ΒΉ) (-c' / c x ^ 2) x
theorem differentiable_within_at.inv {π : Type u} {E :