mathlib3documentation

analysis.calculus.fderiv.basic

The Fréchet derivative #

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

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, the folder `analysis/calculus/fderiv/` contains the usual formulas (and existence assertions) for the derivative of

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

For most binary operations we also define `const_op` and `op_const` theorems for the cases when the first or second argument is a constant. This makes writing chains of `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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s : set E} (h : ¬ x) :
s x = 0
theorem fderiv_zero_of_not_differentiable_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} (h : ¬ x) :
f x = 0
theorem has_fderiv_within_at.lim {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ F] {f : E F} {f' f₁' : E →L[𝕜] F} {x : E} {s : set E} (hf : s x) (hg : f₁' s x) :
f₁' 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} [ E] {F : Type u_3} [ F] {f : E F} {f' f₁' : E →L[𝕜] F} {x : E} {s : set E} (H : 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} [ E] {F : Type u_3} [ F] {f : E F} {f' f₁' : E →L[𝕜] F} {x : E} {s : set E} (H : 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ F] {f : E F} {f' : E →L[𝕜] F} {x : E} {s : set E} (h : s x) :
x
theorem has_fderiv_at.differentiable_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {f' : E →L[𝕜] F} {x : E} (h : f' x) :
x
@[simp]
theorem has_fderiv_within_at_univ {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ F] {f : E F} {f' : E →L[𝕜] F} {x : E} {s : set E} {y : E} :
s) x s x
theorem has_fderiv_within_at.insert' {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {f' : E →L[𝕜] F} {x : E} {s : set E} {y : E} :
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} [ E] {F : Type u_3} [ F] {f : E F} {f' : E →L[𝕜] F} {x : E} {s : set E} {y : E} :
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} [ E] {F : Type u_3} [ F] {f : E F} {f' : E →L[𝕜] F} {x : E} {s : set E} (h : s x) :
s) x
theorem has_fderiv_within_at_diff_singleton {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {f' : E →L[𝕜] F} {x : E} {s : set E} (y : E) :
(s \ {y}) x s x
theorem has_strict_fderiv_at.is_O_sub {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ F] {f : E F} {f' : E →L[𝕜] F} {x : E} (hf : x) :
x
theorem has_strict_fderiv_at.exists_lipschitz_on_with_of_nnnorm_lt {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s : set E} (h : x) (hs : s nhds x) :
x
theorem differentiable_within_at.has_fderiv_within_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s : set E} (h : x) :
f s x) s x
theorem differentiable_at.has_fderiv_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} (h : x) :
(fderiv 𝕜 f x) x
theorem differentiable_on.has_fderiv_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s : set E} (h : s) (hs : s nhds x) :
(fderiv 𝕜 f x) x
theorem differentiable_on.differentiable_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s : set E} (h : s) (hs : s nhds x) :
x
theorem differentiable_on.eventually_differentiable_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s : set E} (h : s) (hs : s nhds x) :
∀ᶠ (y : E) in nhds x, y
theorem has_fderiv_at.fderiv {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {f' : E →L[𝕜] F} {x : E} (h : f' x) :
f x = f'
theorem fderiv_eq {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {f' : E (E →L[𝕜] F)} (h : (x : E), (f' x) x) :
f = f'
theorem fderiv_at.le_of_lip {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x₀ : E} (hf : x₀) {s : set E} (hs : s nhds x₀) {C : nnreal} (hlip : s) :
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} [ E] {F : Type u_3} [ F] {f : E F} {f' : E →L[𝕜] F} {x : E} {s : set E} (h : s x) (hxs : x) :
s x = f'
theorem has_fderiv_within_at_of_not_mem_closure {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s t : set E} (h : x) (st : s t) :
x
theorem differentiable_within_at.mono_of_mem {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s : set E} (h : x) {t : set E} (hst : s t) :
x
theorem differentiable_within_at_univ {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} :
x
theorem differentiable_within_at_inter {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s t : set E} (ht : t nhds x) :
(s t) x x
theorem differentiable_within_at_inter' {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s t : set E} (ht : t s) :
(s t) x x
theorem differentiable_at.differentiable_within_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s : set E} (h : x) :
x
theorem differentiable.differentiable_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} (h : f) :
x
theorem differentiable_at.fderiv_within {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s : set E} (h : x) (hxs : x) :
s x = f x
theorem differentiable_on.mono {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {s t : set E} (h : t) (st : s t) :
s
theorem differentiable_on_univ {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} :
theorem differentiable.differentiable_on {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {s : set E} (h : f) :
s
theorem differentiable_on_of_locally_differentiable_on {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {s : set E} (h : (x : E), x s ( (u : set E), x u (s u))) :
s
theorem fderiv_within_of_mem {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s t : set E} (st : t s) (ht : x) (h : x) :
s x = t x
theorem fderiv_within_subset {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s t : set E} (st : s t) (ht : x) (h : x) :
s x = t x
theorem fderiv_within_inter {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s t : set E} (ht : t nhds x) :
(s t) x = s x
theorem fderiv_within_of_mem_nhds {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s : set E} (h : s nhds x) :
s x = f x
@[simp]
theorem fderiv_within_univ {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} :
= f
theorem fderiv_within_of_open {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s : set E} (hs : is_open s) (hx : x s) :
s x = f x
theorem fderiv_within_eq_fderiv {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s : set E} (hs : x) (h : x) :
s x = f x
theorem fderiv_mem_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {s : set (E →L[𝕜] F)} {x : E} :
f x s x f x s ¬ x 0 s
theorem fderiv_within_mem_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {t : set E} {s : set (E →L[𝕜] F)} {x : E} :
t x s x t x s ¬ x 0 s
theorem asymptotics.is_O.has_fderiv_within_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {s : set E} {x₀ : E} {n : } (h : f =O[ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ F] {f : E F} {s : set E} {x₀ : E} {f' : E →L[𝕜] F} (h : s x₀) :
(λ (x : E), f x - f x₀) =O[ s] λ (x : E), x - x₀
theorem has_fderiv_at.is_O {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s : set E} (h : x) :
x
theorem differentiable_at.continuous_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} (h : x) :
theorem differentiable_on.continuous_on {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {s : set E} (h : s) :
theorem differentiable.continuous {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} (h : f) :
@[protected]
theorem has_strict_fderiv_at.continuous_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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 has_fderiv_within_at_congr_set' {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {f' : E →L[𝕜] F} {x : E} {s t : set E} (y : E) (h : s =ᶠ[ {y}] t) :
s x t x
theorem has_fderiv_within_at_congr_set {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {f' : E →L[𝕜] F} {x : E} {s t : set E} (h : s =ᶠ[nhds x] t) :
s x t x
theorem differentiable_within_at_congr_set' {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s t : set E} (y : E) (h : s =ᶠ[ {y}] t) :
x x
theorem differentiable_within_at_congr_set {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s t : set E} (h : s =ᶠ[nhds x] t) :
x x
theorem fderiv_within_congr_set' {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s t : set E} (y : E) (h : s =ᶠ[ {y}] t) :
s x = t x
theorem fderiv_within_congr_set {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s t : set E} (h : s =ᶠ[nhds x] t) :
s x = t x
theorem fderiv_within_eventually_congr_set' {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s t : set E} (y : E) (h : s =ᶠ[ {y}] t) :
s =ᶠ[nhds x] t
theorem fderiv_within_eventually_congr_set {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s t : set E} (h : s =ᶠ[nhds x] t) :
s =ᶠ[nhds x] t
theorem filter.eventually_eq.has_strict_fderiv_at_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ F] {f₀ f₁ : E F} {f' : E →L[𝕜] F} {x : E} (h : f₀ =ᶠ[nhds x] f₁) :
f' x f' x
theorem filter.eventually_eq.differentiable_at_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f₀ f₁ : E F} {x : E} (h : f₀ =ᶠ[nhds x] f₁) :
x x
theorem filter.eventually_eq.has_fderiv_within_at_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ F] {f₀ f₁ : E F} {x : E} {s : set E} (h : f₀ =ᶠ[ s] f₁) (hx : f₀ x = f₁ x) :
s x s x
theorem filter.eventually_eq.differentiable_within_at_iff_of_mem {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f₀ f₁ : E F} {x : E} {s : set E} (h : f₀ =ᶠ[ s] f₁) (hx : x s) :
s x s x
theorem has_fderiv_within_at.congr_mono {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f f₁ : E F} {f' : E →L[𝕜] F} {x : E} {s t : set E} (h : s x) (ht : f t) (hx : f₁ x = f x) (h₁ : t s) :
f' t x
theorem has_fderiv_within_at.congr {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f f₁ : E F} {f' : E →L[𝕜] F} {x : E} {s : set E} (h : s x) (hs : f s) (hx : f₁ x = f x) :
f' s x
theorem has_fderiv_within_at.congr' {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f f₁ : E F} {f' : E →L[𝕜] F} {x : E} {s : set E} (h : s x) (hs : f s) (hx : x s) :
f' s x
theorem has_fderiv_within_at.congr_of_eventually_eq {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ F] {f f₁ : E F} {f' : E →L[𝕜] F} {x : E} (h : f' x) (h₁ : f₁ =ᶠ[nhds x] f) :
f' x
theorem differentiable_within_at.congr_mono {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f f₁ : E F} {x : E} {s t : set E} (h : x) (ht : f t) (hx : f₁ x = f x) (h₁ : t s) :
t x
theorem differentiable_within_at.congr {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f f₁ : E F} {x : E} {s : set E} (h : x) (ht : (x : E), x s f₁ x = f x) (hx : f₁ x = f x) :
s x
theorem differentiable_within_at.congr_of_eventually_eq {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f f₁ : E F} {x : E} {s : set E} (h : x) (h₁ : f₁ =ᶠ[ s] f) (hx : f₁ x = f x) :
s x
theorem differentiable_on.congr_mono {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f f₁ : E F} {s t : set E} (h : s) (h' : (x : E), x t f₁ x = f x) (h₁ : t s) :
t
theorem differentiable_on.congr {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f f₁ : E F} {s : set E} (h : s) (h' : (x : E), x s f₁ x = f x) :
s
theorem differentiable_on_congr {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f f₁ : E F} {s : set E} (h' : (x : E), x s f₁ x = f x) :
s s
theorem differentiable_at.congr_of_eventually_eq {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f f₁ : E F} {x : E} (h : x) (hL : f₁ =ᶠ[nhds x] f) :
x
theorem differentiable_within_at.fderiv_within_congr_mono {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f f₁ : E F} {x : E} {s t : set E} (h : x) (hs : f t) (hx : f₁ x = f x) (hxt : x) (h₁ : t s) :
f₁ t x = s x
theorem filter.eventually_eq.fderiv_within_eq {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f f₁ : E F} {x : E} {s : set E} (hs : f₁ =ᶠ[ s] f) (hx : f₁ x = f x) :
f₁ s x = s x
theorem filter.eventually_eq.fderiv_within' {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f f₁ : E F} {x : E} {s t : set E} (hs : f₁ =ᶠ[ s] f) (ht : t s) :
f₁ t =ᶠ[ s] t
@[protected]
theorem filter.eventually_eq.fderiv_within {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f f₁ : E F} {x : E} {s : set E} (hs : f₁ =ᶠ[ s] f) :
f₁ s =ᶠ[ s] s
theorem filter.eventually_eq.fderiv_within_eq_nhds {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f f₁ : E F} {x : E} {s : set E} (h : f₁ =ᶠ[nhds x] f) :
f₁ s x = s x
theorem fderiv_within_congr {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f f₁ : E F} {x : E} {s : set E} (hs : f s) (hx : f₁ x = f x) :
f₁ s x = s x
theorem fderiv_within_congr' {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f f₁ : E F} {x : E} {s : set E} (hs : f s) (hx : x s) :
f₁ s x = s x
theorem filter.eventually_eq.fderiv_eq {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f f₁ : E F} {x : E} (h : f₁ =ᶠ[nhds x] f) :
f₁ x = f x
@[protected]
theorem filter.eventually_eq.fderiv {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f f₁ : E F} {x : E} (h : f₁ =ᶠ[nhds x] f) :
f₁ =ᶠ[nhds x] f

Derivative of the identity #

theorem has_strict_fderiv_at_id {𝕜 : Type u_1} {E : Type u_2} [ E] (x : E) :
theorem has_fderiv_at_filter_id {𝕜 : Type u_1} {E : Type u_2} [ E] (x : E) (L : filter E) :
theorem has_fderiv_within_at_id {𝕜 : Type u_1} {E : Type u_2} [ E] (x : E) (s : set E) :
theorem has_fderiv_at_id {𝕜 : Type u_1} {E : Type u_2} [ E] (x : E) :
@[simp]
theorem differentiable_at_id {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} :
@[simp]
theorem differentiable_at_id' {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} :
(λ (x : E), x) x
theorem differentiable_within_at_id {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {s : set E} :
@[simp]
theorem differentiable_id {𝕜 : Type u_1} {E : Type u_2} [ E] :
@[simp]
theorem differentiable_id' {𝕜 : Type u_1} {E : Type u_2} [ E] :
(λ (x : E), x)
theorem differentiable_on_id {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} :
theorem fderiv_id {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} :
id x =
@[simp]
theorem fderiv_id' {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} :
(λ (x : E), x) x =
theorem fderiv_within_id {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {s : set E} (hxs : x) :
s x =
theorem fderiv_within_id' {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {s : set E} (hxs : x) :
(λ (x : E), x) s x =

derivative of a constant function #

theorem has_strict_fderiv_at_const {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ 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} [ E] {F : Type u_3} [ F] {x : E} (c : F) :
(λ (x : E), c) x
theorem differentiable_within_at_const {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} {s : set E} (c : F) :
(λ (x : E), c) s x
theorem fderiv_const_apply {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} (c : F) :
(λ (y : E), c) x = 0
@[simp]
theorem fderiv_const {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] (c : F) :
(λ (y : E), c) = 0
theorem fderiv_within_const_apply {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} {s : set E} (c : F) (hxs : x) :
(λ (y : E), c) s x = 0
@[simp]
theorem differentiable_const {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] (c : F) :
(λ (x : E), c)
theorem differentiable_on_const {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {s : set E} (c : F) :
(λ (x : E), c) s
theorem has_fderiv_within_at_singleton {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E F) (x : E) :
{x} x
theorem has_fderiv_at_of_subsingleton {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] [h : subsingleton E] (f : E F) (x : E) :
x
theorem differentiable_on_empty {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} :
theorem differentiable_on_singleton {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} :
{x}
theorem set.subsingleton.differentiable_on {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {s : set E} (hs : s.subsingleton) :
s
theorem has_fderiv_at_zero_of_eventually_const {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} (c : F) (hf : f =ᶠ[nhds x] λ (y : E), c) :
x

Support of derivatives #

theorem support_fderiv_subset (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [ E] [ F] {f : E F} :
theorem tsupport_fderiv_subset (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [ E] [ F] {f : E F} :
tsupport (fderiv 𝕜 f)
theorem has_compact_support.fderiv (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [ E] [ F] {f : E F} (hf : has_compact_support f) :