# mathlibdocumentation

analysis.calculus.fderiv

# The FrΓ©chet derivative #

Let `E` and `F` be normed spaces, `f : E β F`, and `f' : E βL[π] F` a continuous π-linear map, where `π` is a non-discrete normed field. Then

`has_fderiv_within_at f f' s x`

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

`has_fderiv_at f f' x := has_fderiv_within_at f f' x univ`

Finally,

`has_strict_fderiv_at f f' x`

means that `f : E β F` has derivative `f' : E βL[π] F` in the sense of strict differentiability, i.e., `f y - f z - f'(y - z) = o(y - z)` as `y, z β x`. This notion is used in the inverse function theorem, and is defined here only to avoid proving theorems like `is_bounded_bilinear_map.has_fderiv_at` twice: first for `has_fderiv_at`, then for `has_strict_fderiv_at`.

## Main results #

In addition to the definition and basic properties of the derivative, this file contains the usual formulas (and existence assertions) for the derivative of

• constants
• the identity
• bounded linear maps
• bounded bilinear maps
• sum of two functions
• sum of finitely many functions
• multiplication of a function by a scalar constant
• negative of a function
• subtraction of two functions
• multiplication of a function by a scalar function
• multiplication of two scalar functions
• composition of functions (the chain rule)
• inverse function (assuming that it exists; the inverse function theorem is in `inverse.lean`)

For most binary operations we also define `const_op` and `op_const` theorems for the cases when the first or second argument is a constant. This makes writing chains of `has_deriv_at`'s easier, and they more frequently lead to the desired result.

One can also interpret the derivative of a function `f : π β E` as an element of `E` (by identifying a linear function from `π` to `E` with its value at `1`). Results on the FrΓ©chet derivative are translated to this more elementary point of view on the derivative in the file `deriv.lean`. The derivative of polynomials is handled there, as it is naturally one-dimensional.

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

``````example (x : β) (h : 1 + sin x β  0) : differentiable_at β (Ξ» x, exp x / (1 + sin x)) x :=
by simp [h]
``````

Of course, these examples only work once `exp`, `cos` and `sin` have been shown to be differentiable, in `analysis.special_functions.trigonometric`.

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

## Implementation details #

The derivative is defined in terms of the `is_o` relation, but also characterized in terms of the `tendsto` relation.

We also introduce predicates `differentiable_within_at π f s x` (where `π` is the base field, `f` the function to be differentiated, `x` the point at which the derivative is asserted to exist, and `s` the set along which the derivative is defined), as well as `differentiable_at π f x`, `differentiable_on π f s` and `differentiable π f` to express the existence of a derivative.

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

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

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

## Tags #

derivative, differentiable, FrΓ©chet, calculus

def has_fderiv_at_filter {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (f : E β F) (f' : E βL[π] F) (x : E) (L : filter E) :
Prop

A function `f` has the continuous linear map `f'` as derivative along the filter `L` if `f x' = f x + f' (x' - x) + o (x' - x)` when `x'` converges along the filter `L`. This definition is designed to be specialized for `L = π x` (in `has_fderiv_at`), giving rise to the usual notion of FrΓ©chet derivative, and for `L = π[s] x` (in `has_fderiv_within_at`), giving rise to the notion of FrΓ©chet derivative along the set `s`.

Equations
• x L = (Ξ» (x' : E), f x' - f x - βf' (x' - x)) =o[L] Ξ» (x' : E), x' - x
def has_fderiv_within_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (f : E β F) (f' : E βL[π] F) (s : set E) (x : E) :
Prop

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

Equations
• s x = x s)
def has_fderiv_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (f : E β F) (f' : E βL[π] F) (x : E) :
Prop

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

Equations
def has_strict_fderiv_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (f : E β F) (f' : E βL[π] F) (x : E) :
Prop

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

Equations
def differentiable_within_at (π : Type u_1) {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (f : E β F) (s : set E) (x : E) :
Prop

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

Equations
def differentiable_at (π : Type u_1) {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (f : E β F) (x : E) :
Prop

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

Equations
noncomputable def fderiv_within (π : Type u_1) {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (f : E β F) (s : set E) (x : E) :
E βL[π] F

If `f` has a derivative at `x` within `s`, then `fderiv_within π f s x` is such a derivative. Otherwise, it is set to `0`.

Equations
noncomputable def fderiv (π : Type u_1) {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (f : E β F) (x : E) :
E βL[π] F

If `f` has a derivative at `x`, then `fderiv π f x` is such a derivative. Otherwise, it is set to `0`.

Equations
def differentiable_on (π : Type u_1) {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (f : E β F) (s : set E) :
Prop

`differentiable_on π f s` means that `f` is differentiable within `s` at any point of `s`.

Equations
def differentiable (π : Type u_1) {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (f : E β F) :
Prop

`differentiable π f` means that `f` is differentiable at any point.

Equations
theorem fderiv_within_zero_of_not_differentiable_within_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {s : set E} (h : Β¬ f s x) :
fderiv_within π f s x = 0
theorem fderiv_zero_of_not_differentiable_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} (h : Β¬ f x) :
fderiv π f x = 0
theorem has_fderiv_within_at.lim {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} {s : set E} (h : s x) {Ξ± : Type u_4} (l : filter Ξ±) {c : Ξ± β π} {d : Ξ± β E} {v : E} (dtop : βαΆ  (n : Ξ±) in l, x + d n β s) (clim : filter.tendsto (Ξ» (n : Ξ±), βc nβ) l filter.at_top) (cdlim : filter.tendsto (Ξ» (n : Ξ±), c n β’ d n) l (nhds v)) :
filter.tendsto (Ξ» (n : Ξ±), c n β’ (f (x + d n) - f x)) l (nhds (βf' v))

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

theorem has_fderiv_within_at.unique_on {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' fβ' : E βL[π] F} {x : E} {s : set E} (hf : s x) (hg : fβ' s x) :
βfβ' (tangent_cone_at π s x)

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

theorem unique_diff_within_at.eq {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' fβ' : E βL[π] F} {x : E} {s : set E} (H : s x) (hf : s x) (hg : fβ' s x) :
f' = fβ'

`unique_diff_within_at` achieves its goal: it implies the uniqueness of the derivative.

theorem unique_diff_on.eq {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' fβ' : E βL[π] F} {x : E} {s : set E} (H : unique_diff_on π s) (hx : x β s) (h : s x) (hβ : fβ' s x) :
f' = fβ'

### Basic properties of the derivative #

theorem has_fderiv_at_filter_iff_tendsto {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} {L : filter E} :
x L β filter.tendsto (Ξ» (x' : E), βx' - xββ»ΒΉ * βf x' - f x - βf' (x' - x)β) L (nhds 0)
theorem has_fderiv_within_at_iff_tendsto {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} {s : set E} :
s x β filter.tendsto (Ξ» (x' : E), βx' - xββ»ΒΉ * βf x' - f x - βf' (x' - x)β) s) (nhds 0)
theorem has_fderiv_at_iff_tendsto {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} :
f' x β filter.tendsto (Ξ» (x' : E), βx' - xββ»ΒΉ * βf x' - f x - βf' (x' - x)β) (nhds x) (nhds 0)
theorem has_fderiv_at_iff_is_o_nhds_zero {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} :
f' x β (Ξ» (h : E), f (x + h) - f x - βf' h) =o[nhds 0] Ξ» (h : E), h
theorem has_fderiv_at.le_of_lip' {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {xβ : E} (hf : f' xβ) {C : β} (hCβ : 0 β€ C) (hlip : βαΆ  (x : E) in nhds xβ, βf x - f xββ β€ C * βx - xββ) :

Converse to the mean value inequality: if `f` is differentiable at `xβ` and `C`-lipschitz on a neighborhood of `xβ` then it 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 has_fderiv_at.le_of_lip {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {xβ : E} (hf : f' xβ) {s : set E} (hs : s β nhds xβ) {C : nnreal} (hlip : s) :

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

theorem has_fderiv_at_filter.mono {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} {Lβ Lβ : filter E} (h : x Lβ) (hst : Lβ β€ Lβ) :
x Lβ
theorem has_fderiv_within_at.mono_of_mem {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} {s t : set E} (h : t x) (hst : t β s) :
s x
theorem has_fderiv_within_at.mono {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} {s t : set E} (h : t x) (hst : s β t) :
s x
theorem has_fderiv_at.has_fderiv_at_filter {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} {L : filter E} (h : f' x) (hL : L β€ nhds x) :
x L
theorem has_fderiv_at.has_fderiv_within_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} {s : set E} (h : f' x) :
s x
theorem has_fderiv_within_at.differentiable_within_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} {s : set E} (h : s x) :
f s x
theorem has_fderiv_at.differentiable_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} (h : f' x) :
f x
@[simp]
theorem has_fderiv_within_at_univ {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} :
x β f' x
theorem has_fderiv_within_at.has_fderiv_at_of_univ {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} :
x β f' x

Alias of the forward direction of `has_fderiv_within_at_univ`.

theorem has_fderiv_within_at_insert {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {g : E β F} {x : E} {s : set E} {y : E} {g' : E βL[π] F} :
s) x β s x
theorem has_fderiv_within_at.insert' {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {g : E β F} {x : E} {s : set E} {y : E} {g' : E βL[π] F} :
s x β s) x

Alias of the reverse direction of `has_fderiv_within_at_insert`.

theorem has_fderiv_within_at.of_insert {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {g : E β F} {x : E} {s : set E} {y : E} {g' : E βL[π] F} :
s) x β s x

Alias of the forward direction of `has_fderiv_within_at_insert`.

theorem has_fderiv_within_at.insert {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {g : E β F} {x : E} {s : set E} {g' : E βL[π] F} (h : s x) :
s) x
theorem has_strict_fderiv_at.is_O_sub {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} (hf : x) :
(Ξ» (p : E Γ E), f p.fst - f p.snd) =O[nhds (x, x)] Ξ» (p : E Γ E), p.fst - p.snd
theorem has_fderiv_at_filter.is_O_sub {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} {L : filter E} (h : x L) :
(Ξ» (x' : E), f x' - f x) =O[L] Ξ» (x' : E), x' - x
@[protected]
theorem has_strict_fderiv_at.has_fderiv_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} (hf : x) :
f' x
@[protected]
theorem has_strict_fderiv_at.differentiable_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} (hf : x) :
f x
theorem has_strict_fderiv_at.exists_lipschitz_on_with_of_nnnorm_lt {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} (hf : x) (K : nnreal) (hK : βf'ββ < K) :
β (s : set E) (H : s β nhds x), s

If `f` is strictly differentiable at `x` with derivative `f'` and `K > βf'ββ`, then `f` is `K`-Lipschitz in a neighborhood of `x`.

theorem has_strict_fderiv_at.exists_lipschitz_on_with {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} (hf : x) :
β (K : nnreal) (s : set E) (H : s β nhds x), s

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

theorem has_fderiv_at.lim {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} (hf : f' x) (v : E) {Ξ± : Type u_4} {c : Ξ± β π} {l : filter Ξ±} (hc : filter.tendsto (Ξ» (n : Ξ±), βc nβ) l filter.at_top) :
filter.tendsto (Ξ» (n : Ξ±), c n β’ (f (x + (c n)β»ΒΉ β’ v) - f x)) l (nhds (βf' v))

Directional derivative agrees with `has_fderiv`.

theorem has_fderiv_at.unique {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {fβ' fβ' : E βL[π] F} {x : E} (hβ : fβ' x) (hβ : fβ' x) :
fβ' = fβ'
theorem has_fderiv_within_at_inter' {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} {s t : set E} (h : t β s) :
(s β© t) x β s x
theorem has_fderiv_within_at_inter {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} {s t : set E} (h : t β nhds x) :
(s β© t) x β s x
theorem has_fderiv_within_at.union {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} {s t : set E} (hs : s x) (ht : t x) :
(s βͺ t) x
theorem has_fderiv_within_at.nhds_within {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} {s t : set E} (h : s x) (ht : s β t) :
t x
theorem has_fderiv_within_at.has_fderiv_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} {s : set E} (h : s x) (hs : s β nhds x) :
f' x
theorem differentiable_within_at.differentiable_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {s : set E} (h : f s x) (hs : s β nhds x) :
f x
theorem differentiable_within_at.has_fderiv_within_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {s : set E} (h : f s x) :
(fderiv_within π f s x) s x
theorem differentiable_at.has_fderiv_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} (h : f x) :
(fderiv π f x) x
theorem differentiable_on.has_fderiv_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {s : set E} (h : f s) (hs : s β nhds x) :
(fderiv π f x) x
theorem differentiable_on.differentiable_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {s : set E} (h : f s) (hs : s β nhds x) :
f x
theorem differentiable_on.eventually_differentiable_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {s : set E} (h : f s) (hs : s β nhds x) :
βαΆ  (y : E) in nhds x, f y
theorem has_fderiv_at.fderiv {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} (h : f' x) :
fderiv π f x = f'
theorem fderiv_eq {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E β (E βL[π] F)} (h : β (x : E), (f' x) x) :
fderiv π f = f'
theorem fderiv_at.le_of_lip {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {xβ : E} (hf : f xβ) {s : set E} (hs : s β nhds xβ) {C : nnreal} (hlip : s) :
βfderiv π f xββ β€ βC

Converse to the mean value inequality: if `f` is differentiable at `xβ` and `C`-lipschitz on a neighborhood of `xβ` then it its derivative at `xβ` has norm bounded by `C`. Version using `fderiv`.

theorem has_fderiv_within_at.fderiv_within {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} {s : set E} (h : s x) (hxs : s x) :
fderiv_within π f s x = f'
theorem has_fderiv_within_at_of_not_mem_closure {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} {s : set E} (h : x β ) :
s x

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

theorem differentiable_within_at.mono {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {s t : set E} (h : f t x) (st : s β t) :
f s x
theorem differentiable_within_at.mono_of_mem {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {s : set E} (h : f s x) {t : set E} (hst : s β t) :
f t x
theorem differentiable_within_at_univ {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} :
x β f x
theorem differentiable_within_at_inter {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {s t : set E} (ht : t β nhds x) :
f (s β© t) x β f s x
theorem differentiable_within_at_inter' {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {s t : set E} (ht : t β s) :
f (s β© t) x β f s x
theorem differentiable_within_at.antimono {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {s t : set E} (h : f s x) (hst : s β t) (hx : s β t) :
f t x
theorem has_fderiv_within_at.antimono {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} {s t : set E} (h : s x) (hst : s β t) (hs : s x) (hx : s β t) :
t x
theorem differentiable_at.differentiable_within_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {s : set E} (h : f x) :
f s x
theorem differentiable.differentiable_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} (h : differentiable π f) :
f x
theorem differentiable_at.fderiv_within {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {s : set E} (h : f x) (hxs : s x) :
fderiv_within π f s x = fderiv π f x
theorem differentiable_on.mono {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {s t : set E} (h : f t) (st : s β t) :
f s
theorem differentiable_on_univ {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} :
theorem differentiable.differentiable_on {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {s : set E} (h : differentiable π f) :
f s
theorem differentiable_on_of_locally_differentiable_on {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {s : set E} (h : β (x : E), x β s β (β (u : set E), β§ x β u β§ f (s β© u))) :
f s
theorem fderiv_within_subset {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {s t : set E} (st : s β t) (ht : s x) (h : f t x) :
fderiv_within π f s x = fderiv_within π f t x
theorem fderiv_within_subset' {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {s t : set E} (st : s β t) (ht : s x) (hx : s β t) (h : f s x) :
fderiv_within π f s x = fderiv_within π f t x
@[simp]
theorem fderiv_within_univ {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} :
fderiv_within π f set.univ = fderiv π f
theorem fderiv_within_inter {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {s t : set E} (ht : t β nhds x) (hs : s x) :
fderiv_within π f (s β© t) x = fderiv_within π f s x
theorem fderiv_within_of_mem_nhds {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {s : set E} (h : s β nhds x) :
fderiv_within π f s x = fderiv π f x
theorem fderiv_within_of_open {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {s : set E} (hs : is_open s) (hx : x β s) :
fderiv_within π f s x = fderiv π f x
theorem fderiv_within_eq_fderiv {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {s : set E} (hs : s x) (h : f x) :
fderiv_within π f s x = fderiv π f x
theorem fderiv_mem_iff {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {s : set (E βL[π] F)} {x : E} :
fderiv π f x β s β f x β§ fderiv π f x β s β¨ Β¬ f x β§ 0 β s
theorem fderiv_within_mem_iff {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {t : set E} {s : set (E βL[π] F)} {x : E} :
fderiv_within π f t x β s β f t x β§ fderiv_within π f t x β s β¨ Β¬ f t x β§ 0 β s
theorem asymptotics.is_O.has_fderiv_within_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {s : set E} {xβ : E} {n : β} (h : f =O[nhds_within xβ s] Ξ» (x : E), βx - xββ ^ n) (hxβ : xβ β s) (hn : 1 < n) :
s xβ
theorem asymptotics.is_O.has_fderiv_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {xβ : E} {n : β} (h : f =O[nhds xβ] Ξ» (x : E), βx - xββ ^ n) (hn : 1 < n) :
xβ
theorem has_fderiv_within_at.is_O {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {s : set E} {xβ : E} {f' : E βL[π] F} (h : s xβ) :
(Ξ» (x : E), f x - f xβ) =O[nhds_within xβ s] Ξ» (x : E), x - xβ
theorem has_fderiv_at.is_O {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {xβ : E} {f' : E βL[π] F} (h : f' xβ) :
(Ξ» (x : E), f x - f xβ) =O[nhds xβ] Ξ» (x : E), x - xβ

### Deducing continuity from differentiability #

theorem has_fderiv_at_filter.tendsto_nhds {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} {L : filter E} (hL : L β€ nhds x) (h : x L) :
(nhds (f x))
theorem has_fderiv_within_at.continuous_within_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} {s : set E} (h : s x) :
x
theorem has_fderiv_at.continuous_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} (h : f' x) :
theorem differentiable_within_at.continuous_within_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {s : set E} (h : f s x) :
x
theorem differentiable_at.continuous_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} (h : f x) :
theorem differentiable_on.continuous_on {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {s : set E} (h : f s) :
theorem differentiable.continuous {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} (h : differentiable π f) :
@[protected]
theorem has_strict_fderiv_at.continuous_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} (hf : x) :
theorem has_strict_fderiv_at.is_O_sub_rev {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {f' : E βL[π] F} (hf : x) :
(Ξ» (p : E Γ E), p.fst - p.snd) =O[nhds (x, x)] Ξ» (p : E Γ E), f p.fst - f p.snd
theorem has_fderiv_at_filter.is_O_sub_rev {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {f' : E βL[π] F} {x : E} {L : filter E} (hf : x L) {C : nnreal} (hf' : βf') :
(Ξ» (x' : E), x' - x) =O[L] Ξ» (x' : E), f x' - f x

### congr properties of the derivative #

theorem filter.eventually_eq.has_strict_fderiv_at_iff {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {fβ fβ : E β F} {fβ' fβ' : E βL[π] F} {x : E} (h : fβ =αΆ [nhds x] fβ) (h' : β (y : E), βfβ' y = βfβ' y) :
fβ' x β fβ' x
theorem has_strict_fderiv_at.congr_of_eventually_eq {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f fβ : E β F} {f' : E βL[π] F} {x : E} (h : x) (hβ : f =αΆ [nhds x] fβ) :
f' x
theorem filter.eventually_eq.has_fderiv_at_filter_iff {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {fβ fβ : E β F} {fβ' fβ' : E βL[π] F} {x : E} {L : filter E} (hβ : fβ =αΆ [L] fβ) (hx : fβ x = fβ x) (hβ : β (x : E), βfβ' x = βfβ' x) :
fβ' x L β fβ' x L
theorem has_fderiv_at_filter.congr_of_eventually_eq {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f fβ : E β F} {f' : E βL[π] F} {x : E} {L : filter E} (h : x L) (hL : fβ =αΆ [L] f) (hx : fβ x = f x) :
f' x L
theorem filter.eventually_eq.has_fderiv_at_iff {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {fβ fβ : E β F} {f' : E βL[π] F} {x : E} (h : fβ =αΆ [nhds x] fβ) :
has_fderiv_at fβ f' x β has_fderiv_at fβ f' x
theorem filter.eventually_eq.differentiable_at_iff {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {fβ fβ : E β F} {x : E} (h : fβ =αΆ [nhds x] fβ) :
fβ x β fβ x
theorem filter.eventually_eq.has_fderiv_within_at_iff {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {fβ fβ : E β F} {f' : E βL[π] F} {x : E} {s : set E} (h : fβ =αΆ [ s] fβ) (hx : fβ x = fβ x) :
f' s x β f' s x
theorem filter.eventually_eq.has_fderiv_within_at_iff_of_mem {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {fβ fβ : E β F} {f' : E βL[π] F} {x : E} {s : set E} (h : fβ =αΆ [ s] fβ) (hx : x β s) :
f' s x β f' s x
theorem filter.eventually_eq.differentiable_within_at_iff {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {fβ fβ : E β F} {x : E} {s : set E} (h : fβ =αΆ [ s] fβ) (hx : fβ x = fβ x) :
fβ s x β fβ s x
theorem filter.eventually_eq.differentiable_within_at_iff_of_mem {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {fβ fβ : E β F} {x : E} {s : set E} (h : fβ =αΆ [ s] fβ) (hx : x β s) :
fβ s x β fβ s x
theorem has_fderiv_within_at.congr_mono {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f fβ : E β F} {f' : E βL[π] F} {x : E} {s t : set E} (h : s x) (ht : β (x : E), x β t β fβ x = f x) (hx : fβ x = f x) (hβ : t β s) :
f' t x
theorem has_fderiv_within_at.congr {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f fβ : E β F} {f' : E βL[π] F} {x : E} {s : set E} (h : s x) (hs : β (x : E), x β s β fβ x = f x) (hx : fβ x = f x) :
f' s x
theorem has_fderiv_within_at.congr' {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f fβ : E β F} {f' : E βL[π] F} {x : E} {s : set E} (h : s x) (hs : β (x : E), x β s β fβ x = f x) (hx : x β s) :
f' s x
theorem has_fderiv_within_at.congr_of_eventually_eq {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f fβ : E β F} {f' : E βL[π] F} {x : E} {s : set E} (h : s x) (hβ : fβ =αΆ [ s] f) (hx : fβ x = f x) :
f' s x
theorem has_fderiv_at.congr_of_eventually_eq {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f fβ : E β F} {f' : E βL[π] F} {x : E} (h : f' x) (hβ : fβ =αΆ [nhds x] f) :
has_fderiv_at fβ f' x
theorem differentiable_within_at.congr_mono {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f fβ : E β F} {x : E} {s t : set E} (h : f s x) (ht : β (x : E), x β t β fβ x = f x) (hx : fβ x = f x) (hβ : t β s) :
fβ t x
theorem differentiable_within_at.congr {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f fβ : E β F} {x : E} {s : set E} (h : f s x) (ht : β (x : E), x β s β fβ x = f x) (hx : fβ x = f x) :
fβ s x
theorem differentiable_within_at.congr_of_eventually_eq {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f fβ : E β F} {x : E} {s : set E} (h : f s x) (hβ : fβ =αΆ [ s] f) (hx : fβ x = f x) :
fβ s x
theorem differentiable_on.congr_mono {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f fβ : E β F} {s t : set E} (h : f s) (h' : β (x : E), x β t β fβ x = f x) (hβ : t β s) :
fβ t
theorem differentiable_on.congr {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f fβ : E β F} {s : set E} (h : f s) (h' : β (x : E), x β s β fβ x = f x) :
fβ s
theorem differentiable_on_congr {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f fβ : E β F} {s : set E} (h' : β (x : E), x β s β fβ x = f x) :
fβ s β f s
theorem differentiable_at.congr_of_eventually_eq {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f fβ : E β F} {x : E} (h : f x) (hL : fβ =αΆ [nhds x] f) :
fβ x
theorem differentiable_within_at.fderiv_within_congr_mono {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f fβ : E β F} {x : E} {s t : set E} (h : f s x) (hs : β (x : E), x β t β fβ x = f x) (hx : fβ x = f x) (hxt : t x) (hβ : t β s) :
fderiv_within π fβ t x = fderiv_within π f s x
theorem filter.eventually_eq.fderiv_within_eq {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f fβ : E β F} {x : E} {s : set E} (hs : s x) (hL : fβ =αΆ [ s] f) (hx : fβ x = f x) :
fderiv_within π fβ s x = fderiv_within π f s x
theorem filter.eventually_eq.fderiv_within_eq_nhds {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f fβ : E β F} {x : E} {s : set E} (hs : s x) (hL : fβ =αΆ [nhds x] f) :
fderiv_within π fβ s x = fderiv_within π f s x
theorem fderiv_within_congr {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f fβ : E β F} {x : E} {s : set E} (hs : s x) (hL : β (y : E), y β s β fβ y = f y) (hx : fβ x = f x) :
fderiv_within π fβ s x = fderiv_within π f s x
theorem filter.eventually_eq.fderiv_eq {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f fβ : E β F} {x : E} (hL : fβ =αΆ [nhds x] f) :
fderiv π fβ x = fderiv π f x
@[protected]
theorem filter.eventually_eq.fderiv {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f fβ : E β F} {x : E} (h : fβ =αΆ [nhds x] f) :
fderiv π fβ =αΆ [nhds x] fderiv π f

### Derivative of the identity #

theorem has_strict_fderiv_at_id {π : Type u_1} {E : Type u_2} [normed_space π E] (x : E) :
x
theorem has_fderiv_at_filter_id {π : Type u_1} {E : Type u_2} [normed_space π E] (x : E) (L : filter E) :
x L
theorem has_fderiv_within_at_id {π : Type u_1} {E : Type u_2} [normed_space π E] (x : E) (s : set E) :
s x
theorem has_fderiv_at_id {π : Type u_1} {E : Type u_2} [normed_space π E] (x : E) :
E) x
@[simp]
theorem differentiable_at_id {π : Type u_1} {E : Type u_2} [normed_space π E] {x : E} :
id x
@[simp]
theorem differentiable_at_id' {π : Type u_1} {E : Type u_2} [normed_space π E] {x : E} :
(Ξ» (x : E), x) x
theorem differentiable_within_at_id {π : Type u_1} {E : Type u_2} [normed_space π E] {x : E} {s : set E} :
s x
@[simp]
theorem differentiable_id {π : Type u_1} {E : Type u_2} [normed_space π E] :
@[simp]
theorem differentiable_id' {π : Type u_1} {E : Type u_2} [normed_space π E] :
differentiable π (Ξ» (x : E), x)
theorem differentiable_on_id {π : Type u_1} {E : Type u_2} [normed_space π E] {s : set E} :
id s
theorem fderiv_id {π : Type u_1} {E : Type u_2} [normed_space π E] {x : E} :
fderiv π id x = E
@[simp]
theorem fderiv_id' {π : Type u_1} {E : Type u_2} [normed_space π E] {x : E} :
fderiv π (Ξ» (x : E), x) x = E
theorem fderiv_within_id {π : Type u_1} {E : Type u_2} [normed_space π E] {x : E} {s : set E} (hxs : s x) :
fderiv_within π id s x = E
theorem fderiv_within_id' {π : Type u_1} {E : Type u_2} [normed_space π E] {x : E} {s : set E} (hxs : s x) :
fderiv_within π (Ξ» (x : E), x) s x = E

### derivative of a constant function #

theorem has_strict_fderiv_at_const {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (c : F) (x : E) :
has_strict_fderiv_at (Ξ» (_x : E), c) 0 x
theorem has_fderiv_at_filter_const {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (c : F) (x : E) (L : filter E) :
has_fderiv_at_filter (Ξ» (x : E), c) 0 x L
theorem has_fderiv_within_at_const {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (c : F) (x : E) (s : set E) :
has_fderiv_within_at (Ξ» (x : E), c) 0 s x
theorem has_fderiv_at_const {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (c : F) (x : E) :
has_fderiv_at (Ξ» (x : E), c) 0 x
@[simp]
theorem differentiable_at_const {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {x : E} (c : F) :
(Ξ» (x : E), c) x
theorem differentiable_within_at_const {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {x : E} {s : set E} (c : F) :
(Ξ» (x : E), c) s x
theorem fderiv_const_apply {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {x : E} (c : F) :
fderiv π (Ξ» (y : E), c) x = 0
@[simp]
theorem fderiv_const {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (c : F) :
fderiv π (Ξ» (y : E), c) = 0
theorem fderiv_within_const_apply {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {x : E} {s : set E} (c : F) (hxs : s x) :
fderiv_within π (Ξ» (y : E), c) s x = 0
@[simp]
theorem differentiable_const {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (c : F) :
differentiable π (Ξ» (x : E), c)
theorem differentiable_on_const {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {s : set E} (c : F) :
(Ξ» (x : E), c) s
theorem has_fderiv_within_at_singleton {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (f : E β F) (x : E) :
{x} x
theorem has_fderiv_at_of_subsingleton {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] [h : subsingleton E] (f : E β F) (x : E) :
x
theorem differentiable_on_empty {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} :
theorem differentiable_on_singleton {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} :
f {x}
theorem set.subsingleton.differentiable_on {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {s : set E} (hs : s.subsingleton) :
f s
theorem has_fderiv_at_zero_of_eventually_const {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} (c : F) (hf : f =αΆ [nhds x] Ξ» (y : E), c) :
x

### Continuous linear maps #

There are currently two variants of these in mathlib, the bundled version (named `continuous_linear_map`, and denoted `E βL[π] F`), and the unbundled version (with a predicate `is_bounded_linear_map`). We give statements for both versions.

@[protected]
theorem continuous_linear_map.has_strict_fderiv_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (e : E βL[π] F) {x : E} :
@[protected]
theorem continuous_linear_map.has_fderiv_at_filter {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (e : E βL[π] F) {x : E} {L : filter E} :
L
@[protected]
theorem continuous_linear_map.has_fderiv_within_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (e : E βL[π] F) {x : E} {s : set E} :
x
@[protected]
theorem continuous_linear_map.has_fderiv_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (e : E βL[π] F) {x : E} :
x
@[protected, simp]
theorem continuous_linear_map.differentiable_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (e : E βL[π] F) {x : E} :
βe x
@[protected]
theorem continuous_linear_map.differentiable_within_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (e : E βL[π] F) {x : E} {s : set E} :
s x
@[protected, simp]
theorem continuous_linear_map.fderiv {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (e : E βL[π] F) {x : E} :
fderiv π βe x = e
@[protected]
theorem continuous_linear_map.fderiv_within {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (e : E βL[π] F) {x : E} {s : set E} (hxs : s x) :
fderiv_within π βe s x = e
@[protected, simp]
theorem continuous_linear_map.differentiable {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (e : E βL[π] F) :
@[protected]
theorem continuous_linear_map.differentiable_on {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (e : E βL[π] F) {s : set E} :
βe s
theorem is_bounded_linear_map.has_fderiv_at_filter {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {L : filter E} (h : f) :
theorem is_bounded_linear_map.has_fderiv_within_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {s : set E} (h : f) :
theorem is_bounded_linear_map.has_fderiv_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} (h : f) :
theorem is_bounded_linear_map.differentiable_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} (h : f) :
f x
theorem is_bounded_linear_map.differentiable_within_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {s : set E} (h : f) :
f s x
theorem is_bounded_linear_map.fderiv {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} (h : f) :
theorem is_bounded_linear_map.fderiv_within {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {x : E} {s : set E} (h : f) (hxs : s x) :
theorem is_bounded_linear_map.differentiable {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} (h : f) :
differentiable π f
theorem is_bounded_linear_map.differentiable_on {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {f : E β F} {s : set E} (h : f) :
f s

### Derivative of the composition of two functions #

For composition lemmas, we put x explicit to help the elaborator, as otherwise Lean tends to get confused since there are too many possibilities for composition

theorem has_fderiv_at_filter.comp {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {f : E β F} {f' : E βL[π] F} (x : E) {L : filter E} {g : F β G} {g' : F βL[π] G} {L' : filter F} (hg : (f x) L') (hf : x L) (hL : L') :
has_fderiv_at_filter (g β f) (g'.comp f') x L
theorem has_fderiv_within_at.comp {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {f : E β F} {f' : E βL[π] F} (x : E) {s : set E} {g : F β G} {g' : F βL[π] G} {t : set F} (hg : t (f x)) (hf : s x) (hst : s t) :
has_fderiv_within_at (g β f) (g'.comp f') s x
theorem has_fderiv_at.comp_has_fderiv_within_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {f : E β F} {f' : E βL[π] F} (x : E) {s : set E} {g : F β G} {g' : F βL[π] G} (hg : g' (f x)) (hf : s x) :
has_fderiv_within_at (g β f) (g'.comp f') s x
theorem has_fderiv_within_at.comp_of_mem {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {f : E β F} {f' : E βL[π] F} (x : E) {s : set E} {g : F β G} {g' : F βL[π] G} {t : set F} (hg : t (f x)) (hf : s x) (hst : s) (nhds_within (f x) t)) :
has_fderiv_within_at (g β f) (g'.comp f') s x
theorem has_fderiv_at.comp {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {f : E β F} {f' : E βL[π] F} (x : E) {g : F β G} {g' : F βL[π] G} (hg : g' (f x)) (hf : f' x) :
has_fderiv_at (g β f) (g'.comp f') x

The chain rule.

theorem differentiable_within_at.comp {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {f : E β F} (x : E) {s : set E} {g : F β G} {t : set F} (hg : g t (f x)) (hf : f s x) (h : s t) :
(g β f) s x
theorem differentiable_within_at.comp' {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {f : E β F} (x : E) {s : set E} {g : F β G} {t : set F} (hg : g t (f x)) (hf : f s x) :
(g β f) (s β© f β»ΒΉ' t) x
theorem differentiable_at.comp {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {f : E β F} (x : E) {g : F β G} (hg : g (f x)) (hf : f x) :
(g β f) x
theorem differentiable_at.comp_differentiable_within_at {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {f : E β F} (x : E) {s : set E} {g : F β G} (hg : g (f x)) (hf : f s x) :
(g β f) s x
theorem fderiv_within.comp {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {f : E β F} (x : E) {s : set E} {g : F β G} {t : set F} (hg : g t (f x)) (hf : f s x) (h : s t) (hxs : s x) :
fderiv_within π (g β f) s x = (fderiv_within π g t (f x)).comp (fderiv_within π f s x)
theorem fderiv_within.compβ {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {G' : Type u_5} [normed_space π G'] {f : E β F} (x : E) {s : set E} {g' : G β G'} {g : F β G} {t : set F} {u : set G} {y : F} {y' : G} (hg' : g' u y') (hg : g t y) (hf : f s x) (h2g : t u) (h2f : s t) (h3g : g y = y') (h3f : f x = y) (hxs : s x) :
fderiv_within π (g' β g β f) s x = (fderiv_within π g' u y').comp ((fderiv_within π g t y).comp (fderiv_within π f s x))

Ternary version of `fderiv_within.comp`, with equality assumptions of basepoints added, in order to apply more easily as a rewrite from right-to-left.

theorem fderiv.comp {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {f : E β F} (x : E) {g : F β G} (hg : g (f x)) (hf : f x) :
fderiv π (g β f) x = (fderiv π g (f x)).comp (fderiv π f x)
theorem fderiv.comp_fderiv_within {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {f : E β F} (x : E) {s : set E} {g : F β G} (hg : g (f x)) (hf : f s x) (hxs : s x) :
fderiv_within π (g β f) s x = (fderiv π g (f x)).comp (fderiv_within π f s x)
theorem differentiable_on.comp {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {f : E β F} {s : set E} {g : F β G} {t : set F} (hg : g t) (hf : f s) (st : s t) :
(g β f) s
theorem differentiable.comp {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {f : E β F} {g : F β G} (hg : differentiable π g) (hf : differentiable π f) :
differentiable π (g β f)
theorem differentiable.comp_differentiable_on {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {f : E β F} {s : set E} {g : F β G} (hg : differentiable π g) (hf : f s) :
(g β f) s
@[protected]
theorem has_strict_fderiv_at.comp {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {f : E β F} {f' : E βL[π] F} (x : E) {g : F β G} {g' : F βL[π] G} (hg : (f x)) (hf : x) :
has_strict_fderiv_at (Ξ» (x : E), g (f x)) (g'.comp f') x

The chain rule for derivatives in the sense of strict differentiability.

@[protected]
theorem differentiable.iterate {π : Type u_1} {E : Type u_2} [normed_space π E] {f : E β E} (hf : differentiable π f) (n : β) :
differentiable π f^[n]
@[protected]
theorem differentiable_on.iterate {π : Type u_1} {E : Type u_2} [normed_space π E] {s : set E} {f : E β E} (hf : f s) (hs : s s) (n : β) :
f^[n] s
@[protected]
theorem has_fderiv_at_filter.iterate {π : Type u_1} {E : Type u_2} [normed_space π E] {x : E} {L : filter E} {f : E β E} {f' : E βL[π] E} (hf : x L) (hL : L) (hx : f x = x) (n : β) :
(f' ^ n) x L
@[protected]
theorem has_fderiv_at.iterate {π : Type u_1} {E : Type u_2} [normed_space π E] {x : E} {f : E β E} {f' : E βL[π] E} (hf : f' x) (hx : f x = x) (n : β) :
(f' ^ n) x
@[protected]
theorem has_fderiv_within_at.iterate {π : Type u_1} {E : Type u_2} [normed_space π E] {x : E} {s : set E} {f : E β E} {f' : E βL[π] E} (hf : s x) (hx : f x = x) (hs : s s) (n : β) :
(f' ^ n) s x
@[protected]
theorem has_strict_fderiv_at.iterate {π : Type u_1} {E : Type u_2} [normed_space π E] {x : E} {f : E β E} {f' : E βL[π] E} (hf : x) (hx : f x = x) (n : β) :
(f' ^ n) x
@[protected]
theorem differentiable_at.iterate {π : Type u_1} {E : Type u_2} [normed_space π E] {x : E} {f : E β E} (hf : f x) (hx : f x = x) (n : β) :
f^[n] x
@[protected]
theorem differentiable_within_at.iterate {π : Type u_1} {E : Type u_2} [normed_space π E] {x : E} {s : set E} {f : E β E} (hf : f s x) (hx : f x = x) (hs : s s) (n : β) :
f^[n] s x

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

@[protected]
theorem has_strict_fderiv_at.prod {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {fβ : E β F} {fβ' : E βL[π] F} {x : E} {fβ : E β G} {fβ' : E βL[π] G} (hfβ : fβ' x) (hfβ : fβ' x) :
has_strict_fderiv_at (Ξ» (x : E), (fβ x, fβ x)) (fβ'.prod fβ') x
theorem has_fderiv_at_filter.prod {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {fβ : E β F} {fβ' : E βL[π] F} {x : E} {L : filter E} {fβ : E β G} {fβ' : E βL[π] G} (hfβ : fβ' x L) (hfβ : fβ' x L) :
has_fderiv_at_filter (Ξ» (x : E), (fβ x, fβ x)) (fβ'.prod fβ') x L
theorem has_fderiv_within_at.prod {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {fβ : E β F} {fβ' : E βL[π] F} {x : E} {s : set E} {fβ : E β G} {fβ' : E βL[π] G} (hfβ : fβ' s x) (hfβ : fβ' s x) :
has_fderiv_within_at (Ξ» (x : E), (fβ x, fβ x)) (fβ'.prod fβ') s x
theorem has_fderiv_at.prod {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {fβ : E β F} {fβ' : E βL[π] F} {x : E} {fβ : E β G} {fβ' : E βL[π] G} (hfβ : has_fderiv_at fβ fβ' x) (hfβ : has_fderiv_at fβ fβ' x) :
has_fderiv_at (Ξ» (x : E), (fβ x, fβ x)) (fβ'.prod fβ') x
theorem has_fderiv_at_prod_mk_left {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (eβ : E) (fβ : F) :
has_fderiv_at (Ξ» (e : E), (e, fβ)) E F) eβ
theorem has_fderiv_at_prod_mk_right {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] (eβ : E) (fβ : F) :
has_fderiv_at (Ξ» (f : F), (eβ, f)) E F) fβ
theorem differentiable_within_at.prod {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {fβ : E β F} {x : E} {s : set E} {fβ : E β G} (hfβ : fβ s x) (hfβ : fβ s x) :
(Ξ» (x : E), (fβ x, fβ x)) s x
@[simp]
theorem differentiable_at.prod {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {fβ : E β F} {x : E} {fβ : E β G} (hfβ : fβ x) (hfβ : fβ x) :
(Ξ» (x : E), (fβ x, fβ x)) x
theorem differentiable_on.prod {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {fβ : E β F} {s : set E} {fβ : E β G} (hfβ : fβ s) (hfβ : fβ s) :
(Ξ» (x : E), (fβ x, fβ x)) s
@[simp]
theorem differentiable.prod {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {fβ : E β F} {fβ : E β G} (hfβ : differentiable π fβ) (hfβ : differentiable π fβ) :
differentiable π (Ξ» (x : E), (fβ x, fβ x))
theorem differentiable_at.fderiv_prod {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {fβ : E β F} {x : E} {fβ : E β G} (hfβ : fβ x) (hfβ : fβ x) :
fderiv π (Ξ» (x : E), (fβ x, fβ x)) x = (fderiv π fβ x).prod (fderiv π fβ x)
theorem differentiable_at.fderiv_within_prod {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {fβ : E β F} {x : E} {s : set E} {fβ : E β G} (hfβ : fβ s x) (hfβ : fβ s x) (hxs : s x) :
fderiv_within π (Ξ» (x : E), (fβ x, fβ x)) s x = (fderiv_within π fβ s x).prod (fderiv_within π fβ s x)
theorem has_strict_fderiv_at_fst {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {p : E Γ F} :
p
@[protected]
theorem has_strict_fderiv_at.fst {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {x : E} {fβ : E β F Γ G} {fβ' : E βL[π] F Γ G} (h : fβ' x) :
has_strict_fderiv_at (Ξ» (x : E), (fβ x).fst) F G).comp fβ') x
theorem has_fderiv_at_filter_fst {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {p : E Γ F} {L : filter (E Γ F)} :
p L
@[protected]
theorem has_fderiv_at_filter.fst {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {x : E} {L : filter E} {fβ : E β F Γ G} {fβ' : E βL[π] F Γ G} (h : fβ' x L) :
has_fderiv_at_filter (Ξ» (x : E), (fβ x).fst) F G).comp fβ') x L
theorem has_fderiv_at_fst {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {p : E Γ F} :
E F) p
@[protected]
theorem has_fderiv_at.fst {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {x : E} {fβ : E β F Γ G} {fβ' : E βL[π] F Γ G} (h : has_fderiv_at fβ fβ' x) :
has_fderiv_at (Ξ» (x : E), (fβ x).fst) F G).comp fβ') x
theorem has_fderiv_within_at_fst {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {p : E Γ F} {s : set (E Γ F)} :
s p
@[protected]
theorem has_fderiv_within_at.fst {π : Type u_1} {E : Type u_2} [normed_space π E] {F : Type u_3} [normed_space π F] {G : Type u_4} [normed_space π G] {x : E} {s : set E} {fβ : E β F Γ G} {fβ' : E βL[π] F Γ G} (h : fβ' s x) :
has_fderiv_within_at (Ξ» (x : E), (fβ x).fst) F G).comp fβ') s x
theorem differentiable_at_fst {π :