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}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F] :
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
- has_fderiv_at_filter f f' x L = asymptotics.is_o (Ξ» (x' : E), f x' - f x - βf' (x' - x)) (Ξ» (x' : E), x' - x) L
def
has_fderiv_within_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F] :
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
- has_fderiv_within_at f f' s x = has_fderiv_at_filter f f' x (nhds_within x s)
def
has_fderiv_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F] :
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
- has_fderiv_at f f' x = has_fderiv_at_filter f f' x (nhds x)
def
has_strict_fderiv_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F] :
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.
def
differentiable_within_at
(π : Type u_1)
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F] :
(E β F) β set E β 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
- differentiable_within_at π f s x = β (f' : E βL[π] F), has_fderiv_within_at f f' s x
def
differentiable_at
(π : Type u_1)
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F] :
(E β F) β E β Prop
A function f is differentiable at a point x if it admits a derivative there (possibly
non-unique).
Equations
- differentiable_at π f x = β (f' : E βL[π] F), has_fderiv_at f f' x
def
fderiv_within
(π : Type u_1)
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π 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
- fderiv_within π f s x = dite (β (f' : E βL[π] F), has_fderiv_within_at f f' s x) (Ξ» (h : β (f' : E βL[π] F), has_fderiv_within_at f f' s x), classical.some h) (Ξ» (h : Β¬β (f' : E βL[π] F), has_fderiv_within_at f f' s x), 0)
def
fderiv
(π : Type u_1)
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F] :
If f has a derivative at x, then fderiv π f x is such a derivative. Otherwise, it is
set to 0.
Equations
- fderiv π f x = dite (β (f' : E βL[π] F), has_fderiv_at f f' x) (Ξ» (h : β (f' : E βL[π] F), has_fderiv_at f f' x), classical.some h) (Ξ» (h : Β¬β (f' : E βL[π] F), has_fderiv_at f f' x), 0)
def
differentiable_on
(π : Type u_1)
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F] :
(E β F) β set E β Prop
differentiable_on π f s means that f is differentiable within s at any point of s.
Equations
- differentiable_on π f s = β (x : E), x β s β differentiable_within_at π f s x
def
differentiable
(π : Type u_1)
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F] :
(E β F) β Prop
differentiable π f means that f is differentiable at any point.
Equations
- differentiable π f = β (x : E), differentiable_at π f x
theorem
fderiv_within_zero_of_not_differentiable_within_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s : set E} :
Β¬differentiable_within_at π f s x β fderiv_within π f s x = 0
theorem
fderiv_zero_of_not_differentiable_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E} :
Β¬differentiable_at π f x β fderiv π f x = 0
theorem
has_fderiv_within_at.lim
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{s : set E}
(h : has_fderiv_within_at f f' s x)
{Ξ± : Type u_4}
(l : filter Ξ±)
{c : Ξ± β π}
{d : Ξ± β E}
{v : E} :
(βαΆ (n : Ξ±) in l, x + d n β s) β filter.tendsto (Ξ» (n : Ξ±), β₯c nβ₯) l filter.at_top β 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
unique_diff_within_at.eq
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' fβ' : E βL[π] F}
{x : E}
{s : set E} :
unique_diff_within_at π s x β has_fderiv_within_at f f' s x β has_fderiv_within_at f 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}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' fβ' : E βL[π] F}
{x : E}
{s : set E} :
unique_diff_on π s β x β s β has_fderiv_within_at f f' s x β has_fderiv_within_at f fβ' s x β f' = fβ'
Basic properties of the derivative
theorem
has_fderiv_at_filter_iff_tendsto
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{L : filter E} :
theorem
has_fderiv_within_at_iff_tendsto
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{s : set E} :
theorem
has_fderiv_at_iff_tendsto
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E} :
theorem
has_fderiv_at_iff_is_o_nhds_zero
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E} :
has_fderiv_at f f' x β asymptotics.is_o (Ξ» (h : E), f (x + h) - f x - βf' h) (Ξ» (h : E), h) (nhds 0)
theorem
has_fderiv_at_filter.mono
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{Lβ Lβ : filter E} :
has_fderiv_at_filter f f' x Lβ β Lβ β€ Lβ β has_fderiv_at_filter f f' x Lβ
theorem
has_fderiv_within_at.mono
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{s t : set E} :
has_fderiv_within_at f f' t x β s β t β has_fderiv_within_at f f' s x
theorem
has_fderiv_at.has_fderiv_at_filter
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{L : filter E} :
has_fderiv_at f f' x β L β€ nhds x β has_fderiv_at_filter f f' x L
theorem
has_fderiv_at.has_fderiv_within_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{s : set E} :
has_fderiv_at f f' x β has_fderiv_within_at f f' s x
theorem
has_fderiv_within_at.differentiable_within_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{s : set E} :
has_fderiv_within_at f f' s x β differentiable_within_at π f s x
theorem
has_fderiv_at.differentiable_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E} :
has_fderiv_at f f' x β differentiable_at π f x
@[simp]
theorem
has_fderiv_within_at_univ
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E} :
has_fderiv_within_at f f' set.univ x β has_fderiv_at f f' x
theorem
has_strict_fderiv_at.is_O_sub
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E} :
theorem
has_fderiv_at_filter.is_O_sub
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{L : filter E} :
has_fderiv_at_filter f f' x L β asymptotics.is_O (Ξ» (x' : E), f x' - f x) (Ξ» (x' : E), x' - x) L
theorem
has_strict_fderiv_at.has_fderiv_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E} :
has_strict_fderiv_at f f' x β has_fderiv_at f f' x
theorem
has_strict_fderiv_at.differentiable_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E} :
has_strict_fderiv_at f f' x β differentiable_at π f x
theorem
has_fderiv_at.lim
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
(hf : has_fderiv_at f f' x)
(v : E)
{Ξ± : Type u_4}
{c : Ξ± β π}
{l : filter Ξ±} :
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}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{fβ' fβ' : E βL[π] F}
{x : E} :
has_fderiv_at f fβ' x β has_fderiv_at f fβ' x β fβ' = fβ'
theorem
has_fderiv_within_at_inter'
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{s t : set E} :
t β nhds_within x s β (has_fderiv_within_at f f' (s β© t) x β has_fderiv_within_at f f' s x)
theorem
has_fderiv_within_at_inter
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{s t : set E} :
t β nhds x β (has_fderiv_within_at f f' (s β© t) x β has_fderiv_within_at f f' s x)
theorem
has_fderiv_within_at.union
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{s t : set E} :
has_fderiv_within_at f f' s x β has_fderiv_within_at f f' t x β has_fderiv_within_at f f' (s βͺ t) x
theorem
has_fderiv_within_at.nhds_within
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{s t : set E} :
has_fderiv_within_at f f' s x β s β nhds_within x t β has_fderiv_within_at f f' t x
theorem
has_fderiv_within_at.has_fderiv_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{s : set E} :
has_fderiv_within_at f f' s x β s β nhds x β has_fderiv_at f f' x
theorem
differentiable_within_at.has_fderiv_within_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s : set E} :
differentiable_within_at π f s x β has_fderiv_within_at f (fderiv_within π f s x) s x
theorem
differentiable_at.has_fderiv_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E} :
differentiable_at π f x β has_fderiv_at f (fderiv π f x) x
theorem
has_fderiv_at.fderiv
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E} :
has_fderiv_at f f' x β fderiv π f x = f'
theorem
has_fderiv_within_at.fderiv_within
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{s : set E} :
has_fderiv_within_at f f' s x β unique_diff_within_at π s x β fderiv_within π f s x = f'
theorem
has_fderiv_within_at_of_not_mem_closure
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{s : set E} :
x β closure s β has_fderiv_within_at f f' 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}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s t : set E} :
differentiable_within_at π f t x β s β t β differentiable_within_at π f s x
theorem
differentiable_within_at_univ
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E} :
differentiable_within_at π f set.univ x β differentiable_at π f x
theorem
differentiable_within_at_inter
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s t : set E} :
t β nhds x β (differentiable_within_at π f (s β© t) x β differentiable_within_at π f s x)
theorem
differentiable_within_at_inter'
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s t : set E} :
t β nhds_within x s β (differentiable_within_at π f (s β© t) x β differentiable_within_at π f s x)
theorem
differentiable_at.differentiable_within_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s : set E} :
differentiable_at π f x β differentiable_within_at π f s x
theorem
differentiable.differentiable_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E} :
differentiable π f β differentiable_at π f x
theorem
differentiable_within_at.differentiable_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s : set E} :
differentiable_within_at π f s x β s β nhds x β differentiable_at π f x
theorem
differentiable_at.fderiv_within
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s : set E} :
differentiable_at π f x β unique_diff_within_at π s x β fderiv_within π f s x = fderiv π f x
theorem
differentiable_on.mono
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{s t : set E} :
differentiable_on π f t β s β t β differentiable_on π f s
theorem
differentiable_on_univ
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F} :
differentiable_on π f set.univ β differentiable π f
theorem
differentiable.differentiable_on
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{s : set E} :
differentiable π f β differentiable_on π f s
theorem
differentiable_on_of_locally_differentiable_on
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{s : set E} :
(β (x : E), x β s β (β (u : set E), is_open u β§ x β u β§ differentiable_on π f (s β© u))) β differentiable_on π f s
theorem
fderiv_within_subset
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s t : set E} :
s β t β unique_diff_within_at π s x β differentiable_within_at π f t x β fderiv_within π f s x = fderiv_within π f t x
@[simp]
theorem
fderiv_within_univ
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F} :
fderiv_within π f set.univ = fderiv π f
theorem
fderiv_within_inter
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s t : set E} :
t β nhds x β unique_diff_within_at π s x β fderiv_within π f (s β© t) x = fderiv_within π f s x
Deducing continuity from differentiability
theorem
has_fderiv_at_filter.tendsto_nhds
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{L : filter E} :
L β€ nhds x β has_fderiv_at_filter f f' x L β filter.tendsto f L (nhds (f x))
theorem
has_fderiv_within_at.continuous_within_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{s : set E} :
has_fderiv_within_at f f' s x β continuous_within_at f s x
theorem
has_fderiv_at.continuous_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E} :
has_fderiv_at f f' x β continuous_at f x
theorem
differentiable_within_at.continuous_within_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s : set E} :
differentiable_within_at π f s x β continuous_within_at f s x
theorem
differentiable_at.continuous_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E} :
differentiable_at π f x β continuous_at f x
theorem
differentiable_on.continuous_on
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{s : set E} :
differentiable_on π f s β continuous_on f s
theorem
differentiable.continuous
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F} :
differentiable π f β continuous f
theorem
has_strict_fderiv_at.continuous_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E} :
has_strict_fderiv_at f f' x β continuous_at f x
theorem
has_strict_fderiv_at.is_O_sub_rev
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{f' : E βL[π] F} :
theorem
has_fderiv_at_filter.is_O_sub_rev
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{L : filter E}
{f' : E βL[π] F} :
has_fderiv_at_filter f βf' x L β asymptotics.is_O (Ξ» (x' : E), x' - x) (Ξ» (x' : E), f x' - f x) L
congr properties of the derivative
theorem
filter.eventually_eq.has_strict_fderiv_at_iff
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{fβ fβ : E β F}
{fβ' fβ' : E βL[π] F}
{x : E} :
fβ =αΆ [nhds x] fβ β (β (y : E), βfβ' y = βfβ' y) β (has_strict_fderiv_at fβ fβ' x β has_strict_fderiv_at fβ fβ' x)
theorem
has_strict_fderiv_at.congr_of_eventually_eq
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f fβ : E β F}
{f' : E βL[π] F}
{x : E} :
has_strict_fderiv_at f f' x β f =αΆ [nhds x] fβ β has_strict_fderiv_at fβ f' x
theorem
filter.eventually_eq.has_fderiv_at_filter_iff
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{fβ fβ : E β F}
{fβ' fβ' : E βL[π] F}
{x : E}
{L : filter E} :
fβ =αΆ [L] fβ β fβ x = fβ x β (β (x : E), βfβ' x = βfβ' x) β (has_fderiv_at_filter fβ fβ' x L β has_fderiv_at_filter fβ fβ' x L)
theorem
has_fderiv_at_filter.congr_of_eventually_eq
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f fβ : E β F}
{f' : E βL[π] F}
{x : E}
{L : filter E} :
has_fderiv_at_filter f f' x L β fβ =αΆ [L] f β fβ x = f x β has_fderiv_at_filter fβ f' x L
theorem
has_fderiv_within_at.congr_mono
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f fβ : E β F}
{f' : E βL[π] F}
{x : E}
{s t : set E} :
has_fderiv_within_at f f' s x β (β (x : E), x β t β fβ x = f x) β fβ x = f x β t β s β has_fderiv_within_at fβ f' t x
theorem
has_fderiv_within_at.congr
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f fβ : E β F}
{f' : E βL[π] F}
{x : E}
{s : set E} :
has_fderiv_within_at f f' s x β (β (x : E), x β s β fβ x = f x) β fβ x = f x β has_fderiv_within_at fβ f' s x
theorem
has_fderiv_within_at.congr_of_eventually_eq
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f fβ : E β F}
{f' : E βL[π] F}
{x : E}
{s : set E} :
has_fderiv_within_at f f' s x β fβ =αΆ [nhds_within x s] f β fβ x = f x β has_fderiv_within_at fβ f' s x
theorem
has_fderiv_at.congr_of_eventually_eq
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f fβ : E β F}
{f' : E βL[π] F}
{x : E} :
has_fderiv_at f f' x β fβ =αΆ [nhds x] f β has_fderiv_at fβ f' x
theorem
differentiable_within_at.congr_mono
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f fβ : E β F}
{x : E}
{s t : set E} :
differentiable_within_at π f s x β (β (x : E), x β t β fβ x = f x) β fβ x = f x β t β s β differentiable_within_at π fβ t x
theorem
differentiable_within_at.congr
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f fβ : E β F}
{x : E}
{s : set E} :
differentiable_within_at π f s x β (β (x : E), x β s β fβ x = f x) β fβ x = f x β differentiable_within_at π fβ s x
theorem
differentiable_within_at.congr_of_eventually_eq
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f fβ : E β F}
{x : E}
{s : set E} :
differentiable_within_at π f s x β fβ =αΆ [nhds_within x s] f β fβ x = f x β differentiable_within_at π fβ s x
theorem
differentiable_on.congr_mono
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f fβ : E β F}
{s t : set E} :
differentiable_on π f s β (β (x : E), x β t β fβ x = f x) β t β s β differentiable_on π fβ t
theorem
differentiable_on.congr
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f fβ : E β F}
{s : set E} :
differentiable_on π f s β (β (x : E), x β s β fβ x = f x) β differentiable_on π fβ s
theorem
differentiable_on_congr
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f fβ : E β F}
{s : set E} :
(β (x : E), x β s β fβ x = f x) β (differentiable_on π fβ s β differentiable_on π f s)
theorem
differentiable_at.congr_of_eventually_eq
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f fβ : E β F}
{x : E} :
differentiable_at π f x β fβ =αΆ [nhds x] f β differentiable_at π fβ x
theorem
differentiable_within_at.fderiv_within_congr_mono
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f fβ : E β F}
{x : E}
{s t : set E} :
differentiable_within_at π f s x β (β (x : E), x β t β fβ x = f x) β fβ x = f x β unique_diff_within_at π t x β t β s β fderiv_within π fβ t x = fderiv_within π f s x
theorem
filter.eventually_eq.fderiv_within_eq
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f fβ : E β F}
{x : E}
{s : set E} :
unique_diff_within_at π s x β fβ =αΆ [nhds_within x s] f β fβ x = f x β fderiv_within π fβ s x = fderiv_within π f s x
theorem
fderiv_within_congr
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f fβ : E β F}
{x : E}
{s : set E} :
unique_diff_within_at π s x β (β (y : E), y β s β fβ y = f y) β fβ x = f x β fderiv_within π fβ s x = fderiv_within π f s x
theorem
filter.eventually_eq.fderiv_eq
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f fβ : E β F}
{x : E} :
Derivative of the identity
theorem
has_strict_fderiv_at_id
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
(x : E) :
has_strict_fderiv_at id (continuous_linear_map.id π E) x
theorem
has_fderiv_at_filter_id
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
(x : E)
(L : filter E) :
has_fderiv_at_filter id (continuous_linear_map.id π E) x L
theorem
has_fderiv_within_at_id
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
(x : E)
(s : set E) :
has_fderiv_within_at id (continuous_linear_map.id π E) s x
theorem
has_fderiv_at_id
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
(x : E) :
has_fderiv_at id (continuous_linear_map.id π E) x
@[simp]
theorem
differentiable_at_id
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E} :
differentiable_at π id x
@[simp]
theorem
differentiable_at_id'
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E} :
differentiable_at π (Ξ» (x : E), x) x
theorem
differentiable_within_at_id
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{s : set E} :
differentiable_within_at π id s x
@[simp]
theorem
differentiable_id
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E] :
differentiable π id
@[simp]
theorem
differentiable_id'
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E] :
differentiable π (Ξ» (x : E), x)
theorem
differentiable_on_id
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{s : set E} :
differentiable_on π id s
theorem
fderiv_id
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E} :
fderiv π id x = continuous_linear_map.id π E
theorem
fderiv_id'
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E} :
fderiv π (Ξ» (x : E), x) x = continuous_linear_map.id π E
theorem
fderiv_within_id
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{s : set E} :
unique_diff_within_at π s x β fderiv_within π id s x = continuous_linear_map.id π E
theorem
fderiv_within_id'
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{s : set E} :
unique_diff_within_at π s x β fderiv_within π (Ξ» (x : E), x) s x = continuous_linear_map.id π E
derivative of a constant function
theorem
has_strict_fderiv_at_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[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}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[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}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[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}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
(c : F)
(x : E) :
has_fderiv_at (Ξ» (x : E), c) 0 x
@[simp]
theorem
differentiable_at_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
(c : F) :
differentiable_at π (Ξ» (x : E), c) x
theorem
differentiable_within_at_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
{s : set E}
(c : F) :
differentiable_within_at π (Ξ» (x : E), c) s x
theorem
fderiv_const_apply
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
(c : F) :
theorem
fderiv_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
(c : F) :
theorem
fderiv_within_const_apply
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
{s : set E}
(c : F) :
unique_diff_within_at π s x β fderiv_within π (Ξ» (y : E), c) s x = 0
@[simp]
theorem
differentiable_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
(c : F) :
differentiable π (Ξ» (x : E), c)
theorem
differentiable_on_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{s : set E}
(c : F) :
differentiable_on π (Ξ» (x : E), c) s
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.
theorem
continuous_linear_map.has_strict_fderiv_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
(e : E βL[π] F)
{x : E} :
has_strict_fderiv_at βe e x
theorem
continuous_linear_map.has_fderiv_at_filter
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
(e : E βL[π] F)
{x : E}
{L : filter E} :
has_fderiv_at_filter βe e x L
theorem
continuous_linear_map.has_fderiv_within_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
(e : E βL[π] F)
{x : E}
{s : set E} :
has_fderiv_within_at βe e s x
theorem
continuous_linear_map.has_fderiv_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
(e : E βL[π] F)
{x : E} :
has_fderiv_at βe e x
@[simp]
theorem
continuous_linear_map.differentiable_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
(e : E βL[π] F)
{x : E} :
differentiable_at π βe x
theorem
continuous_linear_map.differentiable_within_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
(e : E βL[π] F)
{x : E}
{s : set E} :
differentiable_within_at π βe s x
theorem
continuous_linear_map.fderiv
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
(e : E βL[π] F)
{x : E} :
theorem
continuous_linear_map.fderiv_within
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
(e : E βL[π] F)
{x : E}
{s : set E} :
unique_diff_within_at π s x β fderiv_within π βe s x = e
@[simp]
theorem
continuous_linear_map.differentiable
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
(e : E βL[π] F) :
differentiable π βe
theorem
continuous_linear_map.differentiable_on
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
(e : E βL[π] F)
{s : set E} :
differentiable_on π βe s
theorem
is_bounded_linear_map.has_fderiv_at_filter
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{L : filter E}
(h : is_bounded_linear_map π f) :
theorem
is_bounded_linear_map.has_fderiv_within_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s : set E}
(h : is_bounded_linear_map π f) :
theorem
is_bounded_linear_map.has_fderiv_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
(h : is_bounded_linear_map π f) :
theorem
is_bounded_linear_map.differentiable_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E} :
is_bounded_linear_map π f β differentiable_at π f x
theorem
is_bounded_linear_map.differentiable_within_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s : set E} :
is_bounded_linear_map π f β differentiable_within_at π f s x
theorem
is_bounded_linear_map.fderiv
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
(h : is_bounded_linear_map π f) :
fderiv π f x = h.to_continuous_linear_map
theorem
is_bounded_linear_map.fderiv_within
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s : set E}
(h : is_bounded_linear_map π f) :
unique_diff_within_at π s x β fderiv_within π f s x = h.to_continuous_linear_map
theorem
is_bounded_linear_map.differentiable
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F} :
is_bounded_linear_map π f β differentiable π f
theorem
is_bounded_linear_map.differentiable_on
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{s : set E} :
is_bounded_linear_map π f β differentiable_on π 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}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{f : E β F}
{f' : E βL[π] F}
(x : E)
{L : filter E}
{g : F β G}
{g' : F βL[π] G} :
has_fderiv_at_filter g g' (f x) (filter.map f L) β has_fderiv_at_filter f f' x L β has_fderiv_at_filter (g β f) (g'.comp f') x L
theorem
has_fderiv_within_at.comp
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[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} :
has_fderiv_within_at g g' t (f x) β has_fderiv_within_at f f' s x β s β f β»ΒΉ' t β has_fderiv_within_at (g β f) (g'.comp f') s x
theorem
has_fderiv_at.comp
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{f : E β F}
{f' : E βL[π] F}
(x : E)
{g : F β G}
{g' : F βL[π] G} :
has_fderiv_at g g' (f x) β has_fderiv_at f f' x β has_fderiv_at (g β f) (g'.comp f') x
The chain rule.
theorem
has_fderiv_at.comp_has_fderiv_within_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{f : E β F}
{f' : E βL[π] F}
(x : E)
{s : set E}
{g : F β G}
{g' : F βL[π] G} :
has_fderiv_at g g' (f x) β has_fderiv_within_at f f' s x β has_fderiv_within_at (g β f) (g'.comp f') s x
theorem
differentiable_within_at.comp
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{f : E β F}
(x : E)
{s : set E}
{g : F β G}
{t : set F} :
differentiable_within_at π g t (f x) β differentiable_within_at π f s x β s β f β»ΒΉ' t β differentiable_within_at π (g β f) s x
theorem
differentiable_within_at.comp'
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{f : E β F}
(x : E)
{s : set E}
{g : F β G}
{t : set F} :
differentiable_within_at π g t (f x) β differentiable_within_at π f s x β differentiable_within_at π (g β f) (s β© f β»ΒΉ' t) x
theorem
differentiable_at.comp
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{f : E β F}
(x : E)
{g : F β G} :
differentiable_at π g (f x) β differentiable_at π f x β differentiable_at π (g β f) x
theorem
differentiable_at.comp_differentiable_within_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{f : E β F}
(x : E)
{s : set E}
{g : F β G} :
differentiable_at π g (f x) β differentiable_within_at π f s x β differentiable_within_at π (g β f) s x
theorem
fderiv_within.comp
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{f : E β F}
(x : E)
{s : set E}
{g : F β G}
{t : set F} :
differentiable_within_at π g t (f x) β differentiable_within_at π f s x β set.maps_to f s t β unique_diff_within_at π s x β fderiv_within π (g β f) s x = (fderiv_within π g t (f x)).comp (fderiv_within π f s x)
theorem
fderiv.comp
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{f : E β F}
(x : E)
{g : F β G} :
differentiable_at π g (f x) β differentiable_at π f x β fderiv π (g β f) x = (fderiv π g (f x)).comp (fderiv π f x)
theorem
fderiv.comp_fderiv_within
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{f : E β F}
(x : E)
{s : set E}
{g : F β G} :
differentiable_at π g (f x) β differentiable_within_at π f s x β unique_diff_within_at π 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}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{f : E β F}
{s : set E}
{g : F β G}
{t : set F} :
differentiable_on π g t β differentiable_on π f s β s β f β»ΒΉ' t β differentiable_on π (g β f) s
theorem
differentiable.comp
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{f : E β F}
{g : F β G} :
differentiable π g β differentiable π f β differentiable π (g β f)
theorem
differentiable.comp_differentiable_on
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{f : E β F}
{s : set E}
{g : F β G} :
differentiable π g β differentiable_on π f s β differentiable_on π (g β f) s
theorem
has_strict_fderiv_at.comp
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{f : E β F}
{f' : E βL[π] F}
(x : E)
{g : F β G}
{g' : F βL[π] G} :
has_strict_fderiv_at g g' (f x) β has_strict_fderiv_at f f' 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.
theorem
differentiable.iterate
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{f : E β E}
(hf : differentiable π f)
(n : β) :
differentiable π f^[n]
theorem
differentiable_on.iterate
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{s : set E}
{f : E β E}
(hf : differentiable_on π f s)
(hs : set.maps_to f s s)
(n : β) :
differentiable_on π f^[n] s
theorem
has_fderiv_at_filter.iterate
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{L : filter E}
{f : E β E}
{f' : E βL[π] E}
(hf : has_fderiv_at_filter f f' x L)
(hL : filter.tendsto f L L)
(hx : f x = x)
(n : β) :
has_fderiv_at_filter f^[n] (f' ^ n) x L
theorem
has_fderiv_at.iterate
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{f : E β E}
{f' : E βL[π] E}
(hf : has_fderiv_at f f' x)
(hx : f x = x)
(n : β) :
has_fderiv_at f^[n] (f' ^ n) x
theorem
has_fderiv_within_at.iterate
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{s : set E}
{f : E β E}
{f' : E βL[π] E}
(hf : has_fderiv_within_at f f' s x)
(hx : f x = x)
(hs : set.maps_to f s s)
(n : β) :
has_fderiv_within_at f^[n] (f' ^ n) s x
theorem
has_strict_fderiv_at.iterate
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{f : E β E}
{f' : E βL[π] E}
(hf : has_strict_fderiv_at f f' x)
(hx : f x = x)
(n : β) :
has_strict_fderiv_at f^[n] (f' ^ n) x
theorem
differentiable_at.iterate
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{f : E β E}
(hf : differentiable_at π f x)
(hx : f x = x)
(n : β) :
differentiable_at π f^[n] x
theorem
differentiable_within_at.iterate
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{s : set E}
{f : E β E}
(hf : differentiable_within_at π f s x)
(hx : f x = x)
(hs : set.maps_to f s s)
(n : β) :
differentiable_within_at π f^[n] s x
Derivative of the cartesian product of two functions
theorem
has_strict_fderiv_at.prod
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{fβ : E β F}
{fβ' : E βL[π] F}
{x : E}
{fβ : E β G}
{fβ' : E βL[π] G} :
has_strict_fderiv_at fβ fβ' x β has_strict_fderiv_at fβ 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}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{fβ : E β F}
{fβ' : E βL[π] F}
{x : E}
{L : filter E}
{fβ : E β G}
{fβ' : E βL[π] G} :
has_fderiv_at_filter fβ fβ' x L β has_fderiv_at_filter fβ 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}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{fβ : E β F}
{fβ' : E βL[π] F}
{x : E}
{s : set E}
{fβ : E β G}
{fβ' : E βL[π] G} :
has_fderiv_within_at fβ fβ' s x β has_fderiv_within_at fβ 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}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{fβ : E β F}
{fβ' : E βL[π] F}
{x : E}
{fβ : E β G}
{fβ' : E βL[π] G} :
has_fderiv_at fβ fβ' x β has_fderiv_at fβ fβ' x β has_fderiv_at (Ξ» (x : E), (fβ x, fβ x)) (fβ'.prod fβ') x
theorem
differentiable_within_at.prod
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{fβ : E β F}
{x : E}
{s : set E}
{fβ : E β G} :
differentiable_within_at π fβ s x β differentiable_within_at π fβ s x β differentiable_within_at π (Ξ» (x : E), (fβ x, fβ x)) s x
@[simp]
theorem
differentiable_at.prod
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{fβ : E β F}
{x : E}
{fβ : E β G} :
differentiable_at π fβ x β differentiable_at π fβ x β differentiable_at π (Ξ» (x : E), (fβ x, fβ x)) x
theorem
differentiable_on.prod
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{fβ : E β F}
{s : set E}
{fβ : E β G} :
differentiable_on π fβ s β differentiable_on π fβ s β differentiable_on π (Ξ» (x : E), (fβ x, fβ x)) s
@[simp]
theorem
differentiable.prod
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{fβ : E β F}
{fβ : E β G} :
differentiable π fβ β differentiable π fβ β differentiable π (Ξ» (x : E), (fβ x, fβ x))
theorem
differentiable_at.fderiv_prod
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{fβ : E β F}
{x : E}
{fβ : E β G} :
differentiable_at π fβ x β differentiable_at π 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}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{fβ : E β F}
{x : E}
{s : set E}
{fβ : E β G} :
differentiable_within_at π fβ s x β differentiable_within_at π fβ s x β unique_diff_within_at π 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}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{p : E Γ F} :
has_strict_fderiv_at prod.fst (continuous_linear_map.fst π E F) p
theorem
has_strict_fderiv_at.fst
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{x : E}
{fβ : E β F Γ G}
{fβ' : E βL[π] F Γ G} :
has_strict_fderiv_at fβ fβ' x β has_strict_fderiv_at (Ξ» (x : E), (fβ x).fst) ((continuous_linear_map.fst π F G).comp fβ') x
theorem
has_fderiv_at_filter_fst
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{p : E Γ F}
{L : filter (E Γ F)} :
has_fderiv_at_filter prod.fst (continuous_linear_map.fst π E F) p L
theorem
has_fderiv_at_filter.fst
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{x : E}
{L : filter E}
{fβ : E β F Γ G}
{fβ' : E βL[π] F Γ G} :
has_fderiv_at_filter fβ fβ' x L β has_fderiv_at_filter (Ξ» (x : E), (fβ x).fst) ((continuous_linear_map.fst π F G).comp fβ') x L
theorem
has_fderiv_at_fst
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{p : E Γ F} :
has_fderiv_at prod.fst (continuous_linear_map.fst π E F) p
theorem
has_fderiv_at.fst
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{x : E}
{fβ : E β F Γ G}
{fβ' : E βL[π] F Γ G} :
has_fderiv_at fβ fβ' x β has_fderiv_at (Ξ» (x : E), (fβ x).fst) ((continuous_linear_map.fst π F G).comp fβ') x
theorem
has_fderiv_within_at_fst
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{p : E Γ F}
{s : set (E Γ F)} :
has_fderiv_within_at prod.fst (continuous_linear_map.fst π E F) s p
theorem
has_fderiv_within_at.fst
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{x : E}
{s : set E}
{fβ : E β F Γ G}
{fβ' : E βL[π] F Γ G} :
has_fderiv_within_at fβ fβ' s x β has_fderiv_within_at (Ξ» (x : E), (fβ x).fst) ((continuous_linear_map.fst π F G).comp fβ') s x
theorem
differentiable_at_fst
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{p : E Γ F} :
differentiable_at π prod.fst p
@[simp]
theorem
differentiable_at.fst
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{x : E}
{fβ : E β F Γ G} :
differentiable_at π fβ x β differentiable_at π (Ξ» (x : E), (fβ x).fst) x
theorem
differentiable_fst
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F] :
differentiable π prod.fst
@[simp]
theorem
differentiable.fst
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{fβ : E β F Γ G} :
differentiable π fβ β differentiable π (Ξ» (x : E), (fβ x).fst)
theorem
differentiable_within_at_fst
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{p : E Γ F}
{s : set (E Γ F)} :
differentiable_within_at π prod.fst s p
theorem
differentiable_within_at.fst
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{x : E}
{s : set E}
{fβ : E β F Γ G} :
differentiable_within_at π fβ s x β differentiable_within_at π (Ξ» (x : E), (fβ x).fst) s x
theorem
differentiable_on_fst
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{s : set (E Γ F)} :
differentiable_on π prod.fst s
theorem
differentiable_on.fst
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{s : set E}
{fβ : E β F Γ G} :
differentiable_on π fβ s β differentiable_on π (Ξ» (x : E), (fβ x).fst) s
theorem
fderiv_fst
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{p : E Γ F} :
fderiv π prod.fst p = continuous_linear_map.fst π E F
theorem
fderiv.fst
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{x : E}
{fβ : E β F Γ G} :
differentiable_at π fβ x β fderiv π (Ξ» (x : E), (fβ x).fst) x = (continuous_linear_map.fst π F G).comp (fderiv π fβ x)
theorem
fderiv_within_fst
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{p : E Γ F}
{s : set (E Γ F)} :
unique_diff_within_at π s p β fderiv_within π prod.fst s p = continuous_linear_map.fst π E F
theorem
fderiv_within.fst
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{x : E}
{s : set E}
{fβ : E β F Γ G} :
unique_diff_within_at π s x β differentiable_within_at π fβ s x β fderiv_within π (Ξ» (x : E), (fβ x).fst) s x = (continuous_linear_map.fst π F G).comp (fderiv_within π fβ s x)
theorem
has_strict_fderiv_at_snd
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{p : E Γ F} :
has_strict_fderiv_at prod.snd (continuous_linear_map.snd π E F) p
theorem
has_strict_fderiv_at.snd
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{x : E}
{fβ : E β F Γ G}
{fβ' : E βL[π] F Γ G} :
has_strict_fderiv_at fβ fβ' x β has_strict_fderiv_at (Ξ» (x : E), (fβ x).snd) ((continuous_linear_map.snd π F G).comp fβ') x
theorem
has_fderiv_at_filter_snd
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{p : E Γ F}
{L : filter (E Γ F)} :
has_fderiv_at_filter prod.snd (continuous_linear_map.snd π E F) p L
theorem
has_fderiv_at_filter.snd
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{x : E}
{L : filter E}
{fβ : E β F Γ G}
{fβ' : E βL[π] F Γ G} :
has_fderiv_at_filter fβ fβ' x L β has_fderiv_at_filter (Ξ» (x : E), (fβ x).snd) ((continuous_linear_map.snd π F G).comp fβ') x L
theorem
has_fderiv_at_snd
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{p : E Γ F} :
has_fderiv_at prod.snd (continuous_linear_map.snd π E F) p
theorem
has_fderiv_at.snd
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{x : E}
{fβ : E β F Γ G}
{fβ' : E βL[π] F Γ G} :
has_fderiv_at fβ fβ' x β has_fderiv_at (Ξ» (x : E), (fβ x).snd) ((continuous_linear_map.snd π F G).comp fβ') x
theorem
has_fderiv_within_at_snd
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{p : E Γ F}
{s : set (E Γ F)} :
has_fderiv_within_at prod.snd (continuous_linear_map.snd π E F) s p
theorem
has_fderiv_within_at.snd
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{x : E}
{s : set E}
{fβ : E β F Γ G}
{fβ' : E βL[π] F Γ G} :
has_fderiv_within_at fβ fβ' s x β has_fderiv_within_at (Ξ» (x : E), (fβ x).snd) ((continuous_linear_map.snd π F G).comp fβ') s x
theorem
differentiable_at_snd
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{p : E Γ F} :
differentiable_at π prod.snd p
@[simp]
theorem
differentiable_at.snd
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{x : E}
{fβ : E β F Γ G} :
differentiable_at π fβ x β differentiable_at π (Ξ» (x : E), (fβ x).snd) x
theorem
differentiable_snd
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F] :
differentiable π prod.snd
@[simp]
theorem
differentiable.snd
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{fβ : E β F Γ G} :
differentiable π fβ β differentiable π (Ξ» (x : E), (fβ x).snd)
theorem
differentiable_within_at_snd
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{p : E Γ F}
{s : set (E Γ F)} :
differentiable_within_at π prod.snd s p
theorem
differentiable_within_at.snd
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{x : E}
{s : set E}
{fβ : E β F Γ G} :
differentiable_within_at π fβ s x β differentiable_within_at π (Ξ» (x : E), (fβ x).snd) s x
theorem
differentiable_on_snd
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{s : set (E Γ F)} :
differentiable_on π prod.snd s
theorem
differentiable_on.snd
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{s : set E}
{fβ : E β F Γ G} :
differentiable_on π fβ s β differentiable_on π (Ξ» (x : E), (fβ x).snd) s
theorem
fderiv_snd
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{p : E Γ F} :
fderiv π prod.snd p = continuous_linear_map.snd π E F
theorem
fderiv.snd
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{x : E}
{fβ : E β F Γ G} :
differentiable_at π fβ x β fderiv π (Ξ» (x : E), (fβ x).snd) x = (continuous_linear_map.snd π F G).comp (fderiv π fβ x)
theorem
fderiv_within_snd
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{p : E Γ F}
{s : set (E Γ F)} :
unique_diff_within_at π s p β fderiv_within π prod.snd s p = continuous_linear_map.snd π E F
theorem
fderiv_within.snd
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{x : E}
{s : set E}
{fβ : E β F Γ G} :
unique_diff_within_at π s x β differentiable_within_at π fβ s x β fderiv_within π (Ξ» (x : E), (fβ x).snd) s x = (continuous_linear_map.snd π F G).comp (fderiv_within π fβ s x)
theorem
has_strict_fderiv_at.prod_map
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{G' : Type u_5}
[normed_group G']
[normed_space π G']
{f : E β F}
{f' : E βL[π] F}
{fβ : G β G'}
{fβ' : G βL[π] G'}
(p : E Γ G) :
has_strict_fderiv_at f f' p.fst β has_strict_fderiv_at fβ fβ' p.snd β has_strict_fderiv_at (Ξ» (p : E Γ G), (f p.fst, fβ p.snd)) (f'.prod_map fβ') p
theorem
has_fderiv_at.prod_map
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{G' : Type u_5}
[normed_group G']
[normed_space π G']
{f : E β F}
{f' : E βL[π] F}
{fβ : G β G'}
{fβ' : G βL[π] G'}
(p : E Γ G) :
has_fderiv_at f f' p.fst β has_fderiv_at fβ fβ' p.snd β has_fderiv_at (Ξ» (p : E Γ G), (f p.fst, fβ p.snd)) (f'.prod_map fβ') p
@[simp]
theorem
differentiable_at.prod_map
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{G' : Type u_5}
[normed_group G']
[normed_space π G']
{f : E β F}
{fβ : G β G'}
(p : E Γ G) :
differentiable_at π f p.fst β differentiable_at π fβ p.snd β differentiable_at π (Ξ» (p : E Γ G), (f p.fst, fβ p.snd)) p
Derivative of a function multiplied by a constant
theorem
has_strict_fderiv_at.const_smul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
(h : has_strict_fderiv_at f f' x)
(c : π) :
has_strict_fderiv_at (Ξ» (x : E), c β’ f x) (c β’ f') x
theorem
has_fderiv_at_filter.const_smul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{L : filter E}
(h : has_fderiv_at_filter f f' x L)
(c : π) :
has_fderiv_at_filter (Ξ» (x : E), c β’ f x) (c β’ f') x L
theorem
has_fderiv_within_at.const_smul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{s : set E}
(h : has_fderiv_within_at f f' s x)
(c : π) :
has_fderiv_within_at (Ξ» (x : E), c β’ f x) (c β’ f') s x
theorem
has_fderiv_at.const_smul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
(h : has_fderiv_at f f' x)
(c : π) :
has_fderiv_at (Ξ» (x : E), c β’ f x) (c β’ f') x
theorem
differentiable_within_at.const_smul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s : set E}
(h : differentiable_within_at π f s x)
(c : π) :
differentiable_within_at π (Ξ» (y : E), c β’ f y) s x
theorem
differentiable_at.const_smul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
(h : differentiable_at π f x)
(c : π) :
differentiable_at π (Ξ» (y : E), c β’ f y) x
theorem
differentiable_on.const_smul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{s : set E}
(h : differentiable_on π f s)
(c : π) :
differentiable_on π (Ξ» (y : E), c β’ f y) s
theorem
differentiable.const_smul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
(h : differentiable π f)
(c : π) :
differentiable π (Ξ» (y : E), c β’ f y)
theorem
fderiv_within_const_smul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s : set E}
(hxs : unique_diff_within_at π s x)
(h : differentiable_within_at π f s x)
(c : π) :
fderiv_within π (Ξ» (y : E), c β’ f y) s x = c β’ fderiv_within π f s x
theorem
fderiv_const_smul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
(h : differentiable_at π f x)
(c : π) :
Derivative of the sum of two functions
theorem
has_strict_fderiv_at.add
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f g : E β F}
{f' g' : E βL[π] F}
{x : E} :
has_strict_fderiv_at f f' x β has_strict_fderiv_at g g' x β has_strict_fderiv_at (Ξ» (y : E), f y + g y) (f' + g') x
theorem
has_fderiv_at_filter.add
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f g : E β F}
{f' g' : E βL[π] F}
{x : E}
{L : filter E} :
has_fderiv_at_filter f f' x L β has_fderiv_at_filter g g' x L β has_fderiv_at_filter (Ξ» (y : E), f y + g y) (f' + g') x L
theorem
has_fderiv_within_at.add
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f g : E β F}
{f' g' : E βL[π] F}
{x : E}
{s : set E} :
has_fderiv_within_at f f' s x β has_fderiv_within_at g g' s x β has_fderiv_within_at (Ξ» (y : E), f y + g y) (f' + g') s x
theorem
has_fderiv_at.add
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f g : E β F}
{f' g' : E βL[π] F}
{x : E} :
has_fderiv_at f f' x β has_fderiv_at g g' x β has_fderiv_at (Ξ» (x : E), f x + g x) (f' + g') x
theorem
differentiable_within_at.add
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f g : E β F}
{x : E}
{s : set E} :
differentiable_within_at π f s x β differentiable_within_at π g s x β differentiable_within_at π (Ξ» (y : E), f y + g y) s x
@[simp]
theorem
differentiable_at.add
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f g : E β F}
{x : E} :
differentiable_at π f x β differentiable_at π g x β differentiable_at π (Ξ» (y : E), f y + g y) x
theorem
differentiable_on.add
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f g : E β F}
{s : set E} :
differentiable_on π f s β differentiable_on π g s β differentiable_on π (Ξ» (y : E), f y + g y) s
@[simp]
theorem
differentiable.add
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f g : E β F} :
differentiable π f β differentiable π g β differentiable π (Ξ» (y : E), f y + g y)
theorem
fderiv_within_add
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f g : E β F}
{x : E}
{s : set E} :
unique_diff_within_at π s x β differentiable_within_at π f s x β differentiable_within_at π g s x β fderiv_within π (Ξ» (y : E), f y + g y) s x = fderiv_within π f s x + fderiv_within π g s x
theorem
fderiv_add
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f g : E β F}
{x : E} :
differentiable_at π f x β differentiable_at π g x β fderiv π (Ξ» (y : E), f y + g y) x = fderiv π f x + fderiv π g x
theorem
has_strict_fderiv_at.add_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
(hf : has_strict_fderiv_at f f' x)
(c : F) :
has_strict_fderiv_at (Ξ» (y : E), f y + c) f' x
theorem
has_fderiv_at_filter.add_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{L : filter E}
(hf : has_fderiv_at_filter f f' x L)
(c : F) :
has_fderiv_at_filter (Ξ» (y : E), f y + c) f' x L
theorem
has_fderiv_within_at.add_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{s : set E}
(hf : has_fderiv_within_at f f' s x)
(c : F) :
has_fderiv_within_at (Ξ» (y : E), f y + c) f' s x
theorem
has_fderiv_at.add_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
(hf : has_fderiv_at f f' x)
(c : F) :
has_fderiv_at (Ξ» (x : E), f x + c) f' x
theorem
differentiable_within_at.add_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s : set E}
(hf : differentiable_within_at π f s x)
(c : F) :
differentiable_within_at π (Ξ» (y : E), f y + c) s x
theorem
differentiable_at.add_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
(hf : differentiable_at π f x)
(c : F) :
differentiable_at π (Ξ» (y : E), f y + c) x
theorem
differentiable_on.add_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{s : set E}
(hf : differentiable_on π f s)
(c : F) :
differentiable_on π (Ξ» (y : E), f y + c) s
theorem
differentiable.add_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
(hf : differentiable π f)
(c : F) :
differentiable π (Ξ» (y : E), f y + c)
theorem
fderiv_within_add_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s : set E}
(hxs : unique_diff_within_at π s x)
(hf : differentiable_within_at π f s x)
(c : F) :
fderiv_within π (Ξ» (y : E), f y + c) s x = fderiv_within π f s x
theorem
fderiv_add_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
(hf : differentiable_at π f x)
(c : F) :
theorem
has_strict_fderiv_at.const_add
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
(hf : has_strict_fderiv_at f f' x)
(c : F) :
has_strict_fderiv_at (Ξ» (y : E), c + f y) f' x
theorem
has_fderiv_at_filter.const_add
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{L : filter E}
(hf : has_fderiv_at_filter f f' x L)
(c : F) :
has_fderiv_at_filter (Ξ» (y : E), c + f y) f' x L
theorem
has_fderiv_within_at.const_add
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{s : set E}
(hf : has_fderiv_within_at f f' s x)
(c : F) :
has_fderiv_within_at (Ξ» (y : E), c + f y) f' s x
theorem
has_fderiv_at.const_add
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
(hf : has_fderiv_at f f' x)
(c : F) :
has_fderiv_at (Ξ» (x : E), c + f x) f' x
theorem
differentiable_within_at.const_add
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s : set E}
(hf : differentiable_within_at π f s x)
(c : F) :
differentiable_within_at π (Ξ» (y : E), c + f y) s x
theorem
differentiable_at.const_add
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
(hf : differentiable_at π f x)
(c : F) :
differentiable_at π (Ξ» (y : E), c + f y) x
theorem
differentiable_on.const_add
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{s : set E}
(hf : differentiable_on π f s)
(c : F) :
differentiable_on π (Ξ» (y : E), c + f y) s
theorem
differentiable.const_add
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
(hf : differentiable π f)
(c : F) :
differentiable π (Ξ» (y : E), c + f y)
theorem
fderiv_within_const_add
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s : set E}
(hxs : unique_diff_within_at π s x)
(hf : differentiable_within_at π f s x)
(c : F) :
fderiv_within π (Ξ» (y : E), c + f y) s x = fderiv_within π f s x
theorem
fderiv_const_add
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
(hf : differentiable_at π f x)
(c : F) :
Derivative of a finite sum of functions
theorem
has_strict_fderiv_at.sum
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
{ΞΉ : Type u_6}
{u : finset ΞΉ}
{A : ΞΉ β E β F}
{A' : ΞΉ β (E βL[π] F)} :
(β (i : ΞΉ), i β u β has_strict_fderiv_at (A i) (A' i) x) β has_strict_fderiv_at (Ξ» (y : E), u.sum (Ξ» (i : ΞΉ), A i y)) (u.sum (Ξ» (i : ΞΉ), A' i)) x
theorem
has_fderiv_at_filter.sum
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
{L : filter E}
{ΞΉ : Type u_6}
{u : finset ΞΉ}
{A : ΞΉ β E β F}
{A' : ΞΉ β (E βL[π] F)} :
(β (i : ΞΉ), i β u β has_fderiv_at_filter (A i) (A' i) x L) β has_fderiv_at_filter (Ξ» (y : E), u.sum (Ξ» (i : ΞΉ), A i y)) (u.sum (Ξ» (i : ΞΉ), A' i)) x L
theorem
has_fderiv_within_at.sum
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
{s : set E}
{ΞΉ : Type u_6}
{u : finset ΞΉ}
{A : ΞΉ β E β F}
{A' : ΞΉ β (E βL[π] F)} :
(β (i : ΞΉ), i β u β has_fderiv_within_at (A i) (A' i) s x) β has_fderiv_within_at (Ξ» (y : E), u.sum (Ξ» (i : ΞΉ), A i y)) (u.sum (Ξ» (i : ΞΉ), A' i)) s x
theorem
has_fderiv_at.sum
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
{ΞΉ : Type u_6}
{u : finset ΞΉ}
{A : ΞΉ β E β F}
{A' : ΞΉ β (E βL[π] F)} :
(β (i : ΞΉ), i β u β has_fderiv_at (A i) (A' i) x) β has_fderiv_at (Ξ» (y : E), u.sum (Ξ» (i : ΞΉ), A i y)) (u.sum (Ξ» (i : ΞΉ), A' i)) x
theorem
differentiable_within_at.sum
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
{s : set E}
{ΞΉ : Type u_6}
{u : finset ΞΉ}
{A : ΞΉ β E β F} :
(β (i : ΞΉ), i β u β differentiable_within_at π (A i) s x) β differentiable_within_at π (Ξ» (y : E), u.sum (Ξ» (i : ΞΉ), A i y)) s x
@[simp]
theorem
differentiable_at.sum
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
{ΞΉ : Type u_6}
{u : finset ΞΉ}
{A : ΞΉ β E β F} :
(β (i : ΞΉ), i β u β differentiable_at π (A i) x) β differentiable_at π (Ξ» (y : E), u.sum (Ξ» (i : ΞΉ), A i y)) x
theorem
differentiable_on.sum
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{s : set E}
{ΞΉ : Type u_6}
{u : finset ΞΉ}
{A : ΞΉ β E β F} :
(β (i : ΞΉ), i β u β differentiable_on π (A i) s) β differentiable_on π (Ξ» (y : E), u.sum (Ξ» (i : ΞΉ), A i y)) s
@[simp]
theorem
differentiable.sum
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{ΞΉ : Type u_6}
{u : finset ΞΉ}
{A : ΞΉ β E β F} :
(β (i : ΞΉ), i β u β differentiable π (A i)) β differentiable π (Ξ» (y : E), u.sum (Ξ» (i : ΞΉ), A i y))
theorem
fderiv_within_sum
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
{s : set E}
{ΞΉ : Type u_6}
{u : finset ΞΉ}
{A : ΞΉ β E β F} :
unique_diff_within_at π s x β (β (i : ΞΉ), i β u β differentiable_within_at π (A i) s x) β fderiv_within π (Ξ» (y : E), u.sum (Ξ» (i : ΞΉ), A i y)) s x = u.sum (Ξ» (i : ΞΉ), fderiv_within π (A i) s x)
theorem
fderiv_sum
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
{ΞΉ : Type u_6}
{u : finset ΞΉ}
{A : ΞΉ β E β F} :
Derivative of the negative of a function
theorem
has_strict_fderiv_at.neg
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E} :
has_strict_fderiv_at f f' x β has_strict_fderiv_at (Ξ» (x : E), -f x) (-f') x
theorem
has_fderiv_at_filter.neg
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{L : filter E} :
has_fderiv_at_filter f f' x L β has_fderiv_at_filter (Ξ» (x : E), -f x) (-f') x L
theorem
has_fderiv_within_at.neg
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{s : set E} :
has_fderiv_within_at f f' s x β has_fderiv_within_at (Ξ» (x : E), -f x) (-f') s x
theorem
has_fderiv_at.neg
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E} :
has_fderiv_at f f' x β has_fderiv_at (Ξ» (x : E), -f x) (-f') x
theorem
differentiable_within_at.neg
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s : set E} :
differentiable_within_at π f s x β differentiable_within_at π (Ξ» (y : E), -f y) s x
@[simp]
theorem
differentiable_at.neg
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E} :
differentiable_at π f x β differentiable_at π (Ξ» (y : E), -f y) x
theorem
differentiable_on.neg
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{s : set E} :
differentiable_on π f s β differentiable_on π (Ξ» (y : E), -f y) s
@[simp]
theorem
differentiable.neg
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F} :
differentiable π f β differentiable π (Ξ» (y : E), -f y)
theorem
fderiv_within_neg
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s : set E} :
unique_diff_within_at π s x β differentiable_within_at π f s x β fderiv_within π (Ξ» (y : E), -f y) s x = -fderiv_within π f s x
theorem
fderiv_neg
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E} :
Derivative of the difference of two functions
theorem
has_strict_fderiv_at.sub
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f g : E β F}
{f' g' : E βL[π] F}
{x : E} :
has_strict_fderiv_at f f' x β has_strict_fderiv_at g g' x β has_strict_fderiv_at (Ξ» (x : E), f x - g x) (f' - g') x
theorem
has_fderiv_at_filter.sub
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f g : E β F}
{f' g' : E βL[π] F}
{x : E}
{L : filter E} :
has_fderiv_at_filter f f' x L β has_fderiv_at_filter g g' x L β has_fderiv_at_filter (Ξ» (x : E), f x - g x) (f' - g') x L
theorem
has_fderiv_within_at.sub
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f g : E β F}
{f' g' : E βL[π] F}
{x : E}
{s : set E} :
has_fderiv_within_at f f' s x β has_fderiv_within_at g g' s x β has_fderiv_within_at (Ξ» (x : E), f x - g x) (f' - g') s x
theorem
has_fderiv_at.sub
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f g : E β F}
{f' g' : E βL[π] F}
{x : E} :
has_fderiv_at f f' x β has_fderiv_at g g' x β has_fderiv_at (Ξ» (x : E), f x - g x) (f' - g') x
theorem
differentiable_within_at.sub
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f g : E β F}
{x : E}
{s : set E} :
differentiable_within_at π f s x β differentiable_within_at π g s x β differentiable_within_at π (Ξ» (y : E), f y - g y) s x
@[simp]
theorem
differentiable_at.sub
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f g : E β F}
{x : E} :
differentiable_at π f x β differentiable_at π g x β differentiable_at π (Ξ» (y : E), f y - g y) x
theorem
differentiable_on.sub
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f g : E β F}
{s : set E} :
differentiable_on π f s β differentiable_on π g s β differentiable_on π (Ξ» (y : E), f y - g y) s
@[simp]
theorem
differentiable.sub
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f g : E β F} :
differentiable π f β differentiable π g β differentiable π (Ξ» (y : E), f y - g y)
theorem
fderiv_within_sub
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f g : E β F}
{x : E}
{s : set E} :
unique_diff_within_at π s x β differentiable_within_at π f s x β differentiable_within_at π g s x β fderiv_within π (Ξ» (y : E), f y - g y) s x = fderiv_within π f s x - fderiv_within π g s x
theorem
fderiv_sub
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f g : E β F}
{x : E} :
differentiable_at π f x β differentiable_at π g x β fderiv π (Ξ» (y : E), f y - g y) x = fderiv π f x - fderiv π g x
theorem
has_strict_fderiv_at.sub_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
(hf : has_strict_fderiv_at f f' x)
(c : F) :
has_strict_fderiv_at (Ξ» (x : E), f x - c) f' x
theorem
has_fderiv_at_filter.sub_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{L : filter E}
(hf : has_fderiv_at_filter f f' x L)
(c : F) :
has_fderiv_at_filter (Ξ» (x : E), f x - c) f' x L
theorem
has_fderiv_within_at.sub_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{s : set E}
(hf : has_fderiv_within_at f f' s x)
(c : F) :
has_fderiv_within_at (Ξ» (x : E), f x - c) f' s x
theorem
has_fderiv_at.sub_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
(hf : has_fderiv_at f f' x)
(c : F) :
has_fderiv_at (Ξ» (x : E), f x - c) f' x
theorem
differentiable_within_at.sub_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s : set E}
(hf : differentiable_within_at π f s x)
(c : F) :
differentiable_within_at π (Ξ» (y : E), f y - c) s x
theorem
differentiable_at.sub_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
(hf : differentiable_at π f x)
(c : F) :
differentiable_at π (Ξ» (y : E), f y - c) x
theorem
differentiable_on.sub_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{s : set E}
(hf : differentiable_on π f s)
(c : F) :
differentiable_on π (Ξ» (y : E), f y - c) s
theorem
differentiable.sub_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
(hf : differentiable π f)
(c : F) :
differentiable π (Ξ» (y : E), f y - c)
theorem
fderiv_within_sub_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s : set E}
(hxs : unique_diff_within_at π s x)
(hf : differentiable_within_at π f s x)
(c : F) :
fderiv_within π (Ξ» (y : E), f y - c) s x = fderiv_within π f s x
theorem
fderiv_sub_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
(hf : differentiable_at π f x)
(c : F) :
theorem
has_strict_fderiv_at.const_sub
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
(hf : has_strict_fderiv_at f f' x)
(c : F) :
has_strict_fderiv_at (Ξ» (x : E), c - f x) (-f') x
theorem
has_fderiv_at_filter.const_sub
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{L : filter E}
(hf : has_fderiv_at_filter f f' x L)
(c : F) :
has_fderiv_at_filter (Ξ» (x : E), c - f x) (-f') x L
theorem
has_fderiv_within_at.const_sub
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{s : set E}
(hf : has_fderiv_within_at f f' s x)
(c : F) :
has_fderiv_within_at (Ξ» (x : E), c - f x) (-f') s x
theorem
has_fderiv_at.const_sub
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
(hf : has_fderiv_at f f' x)
(c : F) :
has_fderiv_at (Ξ» (x : E), c - f x) (-f') x
theorem
differentiable_within_at.const_sub
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s : set E}
(hf : differentiable_within_at π f s x)
(c : F) :
differentiable_within_at π (Ξ» (y : E), c - f y) s x
theorem
differentiable_at.const_sub
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
(hf : differentiable_at π f x)
(c : F) :
differentiable_at π (Ξ» (y : E), c - f y) x
theorem
differentiable_on.const_sub
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{s : set E}
(hf : differentiable_on π f s)
(c : F) :
differentiable_on π (Ξ» (y : E), c - f y) s
theorem
differentiable.const_sub
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
(hf : differentiable π f)
(c : F) :
differentiable π (Ξ» (y : E), c - f y)
theorem
fderiv_within_const_sub
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s : set E}
(hxs : unique_diff_within_at π s x)
(hf : differentiable_within_at π f s x)
(c : F) :
fderiv_within π (Ξ» (y : E), c - f y) s x = -fderiv_within π f s x
theorem
fderiv_const_sub
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
(hf : differentiable_at π f x)
(c : F) :
Derivative of a bounded bilinear map
theorem
is_bounded_bilinear_map.has_strict_fderiv_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{b : E Γ F β G}
(h : is_bounded_bilinear_map π b)
(p : E Γ F) :
has_strict_fderiv_at b (h.deriv p) p
theorem
is_bounded_bilinear_map.has_fderiv_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{b : E Γ F β G}
(h : is_bounded_bilinear_map π b)
(p : E Γ F) :
has_fderiv_at b (h.deriv p) p
theorem
is_bounded_bilinear_map.has_fderiv_within_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{b : E Γ F β G}
{u : set (E Γ F)}
(h : is_bounded_bilinear_map π b)
(p : E Γ F) :
has_fderiv_within_at b (h.deriv p) u p
theorem
is_bounded_bilinear_map.differentiable_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{b : E Γ F β G}
(h : is_bounded_bilinear_map π b)
(p : E Γ F) :
differentiable_at π b p
theorem
is_bounded_bilinear_map.differentiable_within_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{b : E Γ F β G}
{u : set (E Γ F)}
(h : is_bounded_bilinear_map π b)
(p : E Γ F) :
differentiable_within_at π b u p
theorem
is_bounded_bilinear_map.fderiv
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{b : E Γ F β G}
(h : is_bounded_bilinear_map π b)
(p : E Γ F) :
theorem
is_bounded_bilinear_map.fderiv_within
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{b : E Γ F β G}
{u : set (E Γ F)}
(h : is_bounded_bilinear_map π b)
(p : E Γ F) :
unique_diff_within_at π u p β fderiv_within π b u p = h.deriv p
theorem
is_bounded_bilinear_map.differentiable
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{b : E Γ F β G} :
is_bounded_bilinear_map π b β differentiable π b
theorem
is_bounded_bilinear_map.differentiable_on
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{b : E Γ F β G}
{u : set (E Γ F)} :
is_bounded_bilinear_map π b β differentiable_on π b u
theorem
is_bounded_bilinear_map.continuous
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{b : E Γ F β G} :
is_bounded_bilinear_map π b β continuous b
theorem
is_bounded_bilinear_map.continuous_left
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{b : E Γ F β G}
(h : is_bounded_bilinear_map π b)
{f : F} :
continuous (Ξ» (e : E), b (e, f))
theorem
is_bounded_bilinear_map.continuous_right
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
{b : E Γ F β G}
(h : is_bounded_bilinear_map π b)
{e : E} :
continuous (Ξ» (f : F), b (e, f))
Derivative of the product of a scalar-valued function and a vector-valued function
theorem
has_strict_fderiv_at.smul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{c : E β π}
{c' : E βL[π] π} :
has_strict_fderiv_at c c' x β has_strict_fderiv_at f f' x β has_strict_fderiv_at (Ξ» (y : E), c y β’ f y) (c x β’ f' + c'.smul_right (f x)) x
theorem
has_fderiv_within_at.smul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{s : set E}
{c : E β π}
{c' : E βL[π] π} :
has_fderiv_within_at c c' s x β has_fderiv_within_at f f' s x β has_fderiv_within_at (Ξ» (y : E), c y β’ f y) (c x β’ f' + c'.smul_right (f x)) s x
theorem
has_fderiv_at.smul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{x : E}
{c : E β π}
{c' : E βL[π] π} :
has_fderiv_at c c' x β has_fderiv_at f f' x β has_fderiv_at (Ξ» (y : E), c y β’ f y) (c x β’ f' + c'.smul_right (f x)) x
theorem
differentiable_within_at.smul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s : set E}
{c : E β π} :
differentiable_within_at π c s x β differentiable_within_at π f s x β differentiable_within_at π (Ξ» (y : E), c y β’ f y) s x
@[simp]
theorem
differentiable_at.smul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{c : E β π} :
differentiable_at π c x β differentiable_at π f x β differentiable_at π (Ξ» (y : E), c y β’ f y) x
theorem
differentiable_on.smul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{s : set E}
{c : E β π} :
differentiable_on π c s β differentiable_on π f s β differentiable_on π (Ξ» (y : E), c y β’ f y) s
@[simp]
theorem
differentiable.smul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{c : E β π} :
differentiable π c β differentiable π f β differentiable π (Ξ» (y : E), c y β’ f y)
theorem
fderiv_within_smul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{s : set E}
{c : E β π} :
unique_diff_within_at π s x β differentiable_within_at π c s x β differentiable_within_at π f s x β fderiv_within π (Ξ» (y : E), c y β’ f y) s x = c x β’ fderiv_within π f s x + (fderiv_within π c s x).smul_right (f x)
theorem
fderiv_smul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{x : E}
{c : E β π} :
differentiable_at π c x β differentiable_at π f x β fderiv π (Ξ» (y : E), c y β’ f y) x = c x β’ fderiv π f x + (fderiv π c x).smul_right (f x)
theorem
has_strict_fderiv_at.smul_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
{c : E β π}
{c' : E βL[π] π}
(hc : has_strict_fderiv_at c c' x)
(f : F) :
has_strict_fderiv_at (Ξ» (y : E), c y β’ f) (c'.smul_right f) x
theorem
has_fderiv_within_at.smul_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
{s : set E}
{c : E β π}
{c' : E βL[π] π}
(hc : has_fderiv_within_at c c' s x)
(f : F) :
has_fderiv_within_at (Ξ» (y : E), c y β’ f) (c'.smul_right f) s x
theorem
has_fderiv_at.smul_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
{c : E β π}
{c' : E βL[π] π}
(hc : has_fderiv_at c c' x)
(f : F) :
has_fderiv_at (Ξ» (y : E), c y β’ f) (c'.smul_right f) x
theorem
differentiable_within_at.smul_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
{s : set E}
{c : E β π}
(hc : differentiable_within_at π c s x)
(f : F) :
differentiable_within_at π (Ξ» (y : E), c y β’ f) s x
theorem
differentiable_at.smul_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
{c : E β π}
(hc : differentiable_at π c x)
(f : F) :
differentiable_at π (Ξ» (y : E), c y β’ f) x
theorem
differentiable_on.smul_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{s : set E}
{c : E β π}
(hc : differentiable_on π c s)
(f : F) :
differentiable_on π (Ξ» (y : E), c y β’ f) s
theorem
differentiable.smul_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{c : E β π}
(hc : differentiable π c)
(f : F) :
differentiable π (Ξ» (y : E), c y β’ f)
theorem
fderiv_within_smul_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
{s : set E}
{c : E β π}
(hxs : unique_diff_within_at π s x)
(hc : differentiable_within_at π c s x)
(f : F) :
fderiv_within π (Ξ» (y : E), c y β’ f) s x = (fderiv_within π c s x).smul_right f
theorem
fderiv_smul_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
{c : E β π}
(hc : differentiable_at π c x)
(f : F) :
fderiv π (Ξ» (y : E), c y β’ f) x = (fderiv π c x).smul_right f
Derivative of the product of two scalar-valued functions
theorem
has_strict_fderiv_at.mul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{c d : E β π}
{c' d' : E βL[π] π} :
has_strict_fderiv_at c c' x β has_strict_fderiv_at d d' x β has_strict_fderiv_at (Ξ» (y : E), c y * d y) (c x β’ d' + d x β’ c') x
theorem
has_fderiv_within_at.mul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{s : set E}
{c d : E β π}
{c' d' : E βL[π] π} :
has_fderiv_within_at c c' s x β has_fderiv_within_at d d' s x β has_fderiv_within_at (Ξ» (y : E), c y * d y) (c x β’ d' + d x β’ c') s x
theorem
has_fderiv_at.mul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{c d : E β π}
{c' d' : E βL[π] π} :
has_fderiv_at c c' x β has_fderiv_at d d' x β has_fderiv_at (Ξ» (y : E), c y * d y) (c x β’ d' + d x β’ c') x
theorem
differentiable_within_at.mul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{s : set E}
{c d : E β π} :
differentiable_within_at π c s x β differentiable_within_at π d s x β differentiable_within_at π (Ξ» (y : E), c y * d y) s x
@[simp]
theorem
differentiable_at.mul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{c d : E β π} :
differentiable_at π c x β differentiable_at π d x β differentiable_at π (Ξ» (y : E), c y * d y) x
theorem
differentiable_on.mul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{s : set E}
{c d : E β π} :
differentiable_on π c s β differentiable_on π d s β differentiable_on π (Ξ» (y : E), c y * d y) s
@[simp]
theorem
differentiable.mul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{c d : E β π} :
differentiable π c β differentiable π d β differentiable π (Ξ» (y : E), c y * d y)
theorem
fderiv_within_mul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{s : set E}
{c d : E β π} :
unique_diff_within_at π s x β differentiable_within_at π c s x β differentiable_within_at π d s x β fderiv_within π (Ξ» (y : E), c y * d y) s x = c x β’ fderiv_within π d s x + d x β’ fderiv_within π c s x
theorem
fderiv_mul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{c d : E β π} :
differentiable_at π c x β differentiable_at π d x β fderiv π (Ξ» (y : E), c y * d y) x = c x β’ fderiv π d x + d x β’ fderiv π c x
theorem
has_strict_fderiv_at.mul_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{c : E β π}
{c' : E βL[π] π}
(hc : has_strict_fderiv_at c c' x)
(d : π) :
has_strict_fderiv_at (Ξ» (y : E), c y * d) (d β’ c') x
theorem
has_fderiv_within_at.mul_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{s : set E}
{c : E β π}
{c' : E βL[π] π}
(hc : has_fderiv_within_at c c' s x)
(d : π) :
has_fderiv_within_at (Ξ» (y : E), c y * d) (d β’ c') s x
theorem
has_fderiv_at.mul_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{c : E β π}
{c' : E βL[π] π}
(hc : has_fderiv_at c c' x)
(d : π) :
has_fderiv_at (Ξ» (y : E), c y * d) (d β’ c') x
theorem
differentiable_within_at.mul_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{s : set E}
{c : E β π}
(hc : differentiable_within_at π c s x)
(d : π) :
differentiable_within_at π (Ξ» (y : E), c y * d) s x
theorem
differentiable_at.mul_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{c : E β π}
(hc : differentiable_at π c x)
(d : π) :
differentiable_at π (Ξ» (y : E), c y * d) x
theorem
differentiable_on.mul_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{s : set E}
{c : E β π}
(hc : differentiable_on π c s)
(d : π) :
differentiable_on π (Ξ» (y : E), c y * d) s
theorem
differentiable.mul_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{c : E β π}
(hc : differentiable π c)
(d : π) :
differentiable π (Ξ» (y : E), c y * d)
theorem
fderiv_within_mul_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{s : set E}
{c : E β π}
(hxs : unique_diff_within_at π s x)
(hc : differentiable_within_at π c s x)
(d : π) :
fderiv_within π (Ξ» (y : E), c y * d) s x = d β’ fderiv_within π c s x
theorem
fderiv_mul_const
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{c : E β π}
(hc : differentiable_at π c x)
(d : π) :
theorem
has_strict_fderiv_at.const_mul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{c : E β π}
{c' : E βL[π] π}
(hc : has_strict_fderiv_at c c' x)
(d : π) :
has_strict_fderiv_at (Ξ» (y : E), d * c y) (d β’ c') x
theorem
has_fderiv_within_at.const_mul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{s : set E}
{c : E β π}
{c' : E βL[π] π}
(hc : has_fderiv_within_at c c' s x)
(d : π) :
has_fderiv_within_at (Ξ» (y : E), d * c y) (d β’ c') s x
theorem
has_fderiv_at.const_mul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{c : E β π}
{c' : E βL[π] π}
(hc : has_fderiv_at c c' x)
(d : π) :
has_fderiv_at (Ξ» (y : E), d * c y) (d β’ c') x
theorem
differentiable_within_at.const_mul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{s : set E}
{c : E β π}
(hc : differentiable_within_at π c s x)
(d : π) :
differentiable_within_at π (Ξ» (y : E), d * c y) s x
theorem
differentiable_at.const_mul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{c : E β π}
(hc : differentiable_at π c x)
(d : π) :
differentiable_at π (Ξ» (y : E), d * c y) x
theorem
differentiable_on.const_mul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{s : set E}
{c : E β π}
(hc : differentiable_on π c s)
(d : π) :
differentiable_on π (Ξ» (y : E), d * c y) s
theorem
differentiable.const_mul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{c : E β π}
(hc : differentiable π c)
(d : π) :
differentiable π (Ξ» (y : E), d * c y)
theorem
fderiv_within_const_mul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{s : set E}
{c : E β π}
(hxs : unique_diff_within_at π s x)
(hc : differentiable_within_at π c s x)
(d : π) :
fderiv_within π (Ξ» (y : E), d * c y) s x = d β’ fderiv_within π c s x
theorem
fderiv_const_mul
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{x : E}
{c : E β π}
(hc : differentiable_at π c x)
(d : π) :
theorem
has_fderiv_at_inverse
{π : Type u_1}
[nondiscrete_normed_field π]
{R : Type u_6}
[normed_ring R]
[normed_algebra π R]
[complete_space R]
(x : units R) :
has_fderiv_at ring.inverse (-(continuous_linear_map.lmul_right π R βxβ»ΒΉ).comp (continuous_linear_map.lmul_left π R βxβ»ΒΉ)) βx
At an invertible element x of a normed algebra R, the FrΓ©chet derivative of the inversion
operation is the linear map Ξ» t, - xβ»ΒΉ * t * xβ»ΒΉ.
theorem
differentiable_at_inverse
{π : Type u_1}
[nondiscrete_normed_field π]
{R : Type u_6}
[normed_ring R]
[normed_algebra π R]
[complete_space R]
(x : units R) :
differentiable_at π ring.inverse βx
theorem
fderiv_inverse
{π : Type u_1}
[nondiscrete_normed_field π]
{R : Type u_6}
[normed_ring R]
[normed_algebra π R]
[complete_space R]
(x : units R) :
fderiv π ring.inverse βx = -(continuous_linear_map.lmul_right π R βxβ»ΒΉ).comp (continuous_linear_map.lmul_left π R βxβ»ΒΉ)
Differentiability of linear equivs, and invariance of differentiability
theorem
continuous_linear_equiv.has_strict_fderiv_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
(iso : E βL[π] F) :
has_strict_fderiv_at βiso βiso x
theorem
continuous_linear_equiv.has_fderiv_within_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
{s : set E}
(iso : E βL[π] F) :
has_fderiv_within_at βiso βiso s x
theorem
continuous_linear_equiv.has_fderiv_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
(iso : E βL[π] F) :
has_fderiv_at βiso βiso x
theorem
continuous_linear_equiv.differentiable_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
(iso : E βL[π] F) :
differentiable_at π βiso x
theorem
continuous_linear_equiv.differentiable_within_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
{s : set E}
(iso : E βL[π] F) :
differentiable_within_at π βiso s x
theorem
continuous_linear_equiv.fderiv
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
(iso : E βL[π] F) :
theorem
continuous_linear_equiv.fderiv_within
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{x : E}
{s : set E}
(iso : E βL[π] F) :
unique_diff_within_at π s x β fderiv_within π βiso s x = βiso
theorem
continuous_linear_equiv.differentiable
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
(iso : E βL[π] F) :
differentiable π βiso
theorem
continuous_linear_equiv.differentiable_on
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{s : set E}
(iso : E βL[π] F) :
differentiable_on π βiso s
theorem
continuous_linear_equiv.comp_differentiable_within_at_iff
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
(iso : E βL[π] F)
{f : G β E}
{s : set G}
{x : G} :
differentiable_within_at π (βiso β f) s x β differentiable_within_at π f s x
theorem
continuous_linear_equiv.comp_differentiable_at_iff
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
(iso : E βL[π] F)
{f : G β E}
{x : G} :
differentiable_at π (βiso β f) x β differentiable_at π f x
theorem
continuous_linear_equiv.comp_differentiable_on_iff
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
(iso : E βL[π] F)
{f : G β E}
{s : set G} :
differentiable_on π (βiso β f) s β differentiable_on π f s
theorem
continuous_linear_equiv.comp_differentiable_iff
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
(iso : E βL[π] F)
{f : G β E} :
differentiable π (βiso β f) β differentiable π f
theorem
continuous_linear_equiv.comp_has_fderiv_within_at_iff
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
(iso : E βL[π] F)
{f : G β E}
{s : set G}
{x : G}
{f' : G βL[π] E} :
has_fderiv_within_at (βiso β f) (βiso.comp f') s x β has_fderiv_within_at f f' s x
theorem
continuous_linear_equiv.comp_has_strict_fderiv_at_iff
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
(iso : E βL[π] F)
{f : G β E}
{x : G}
{f' : G βL[π] E} :
has_strict_fderiv_at (βiso β f) (βiso.comp f') x β has_strict_fderiv_at f f' x
theorem
continuous_linear_equiv.comp_has_fderiv_at_iff
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
(iso : E βL[π] F)
{f : G β E}
{x : G}
{f' : G βL[π] E} :
has_fderiv_at (βiso β f) (βiso.comp f') x β has_fderiv_at f f' x
theorem
continuous_linear_equiv.comp_has_fderiv_within_at_iff'
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
(iso : E βL[π] F)
{f : G β E}
{s : set G}
{x : G}
{f' : G βL[π] F} :
has_fderiv_within_at (βiso β f) f' s x β has_fderiv_within_at f (β(iso.symm).comp f') s x
theorem
continuous_linear_equiv.comp_has_fderiv_at_iff'
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
(iso : E βL[π] F)
{f : G β E}
{x : G}
{f' : G βL[π] F} :
has_fderiv_at (βiso β f) f' x β has_fderiv_at f (β(iso.symm).comp f') x
theorem
continuous_linear_equiv.comp_fderiv_within
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
(iso : E βL[π] F)
{f : G β E}
{s : set G}
{x : G} :
unique_diff_within_at π s x β fderiv_within π (βiso β f) s x = βiso.comp (fderiv_within π f s x)
theorem
continuous_linear_equiv.comp_fderiv
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{G : Type u_4}
[normed_group G]
[normed_space π G]
(iso : E βL[π] F)
{f : G β E}
{x : G} :
theorem
has_strict_fderiv_at.of_local_left_inverse
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{g : F β E}
{a : F} :
continuous_at g a β has_strict_fderiv_at f βf' (g a) β (βαΆ (y : F) in nhds a, f (g y) = y) β has_strict_fderiv_at g β(f'.symm) a
If f (g y) = y for y in some neighborhood of a, g is continuous at a, and f has an
invertible derivative f' at g a in the strict sense, then g has the derivative f'β»ΒΉ at a
in the strict sense.
This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.
theorem
has_fderiv_at.of_local_left_inverse
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{f' : E βL[π] F}
{g : F β E}
{a : F} :
continuous_at g a β has_fderiv_at f βf' (g a) β (βαΆ (y : F) in nhds a, f (g y) = y) β has_fderiv_at g β(f'.symm) a
If f (g y) = y for y in some neighborhood of a, g is continuous at a, and f has an
invertible derivative f' at g a, then g has the derivative f'β»ΒΉ at a.
This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.
theorem
has_fderiv_at_filter_real_equiv
{E : Type u_1}
[normed_group E]
[normed_space β E]
{F : Type u_2}
[normed_group F]
[normed_space β F]
{f : E β F}
{f' : E βL[β] F}
{x : E}
{L : filter E} :
theorem
has_fderiv_at.lim_real
{E : Type u_1}
[normed_group E]
[normed_space β E]
{F : Type u_2}
[normed_group F]
[normed_space β F]
{f : E β F}
{f' : E βL[β] F}
{x : E}
(hf : has_fderiv_at f f' x)
(v : E) :
filter.tendsto (Ξ» (c : β), c β’ (f (x + cβ»ΒΉ β’ v) - f x)) filter.at_top (nhds (βf' v))
theorem
has_fderiv_within_at.maps_to_tangent_cone
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{s : set E}
{f' : E βL[π] F}
{x : E} :
has_fderiv_within_at f f' s x β set.maps_to βf' (tangent_cone_at π s x) (tangent_cone_at π (f '' s) (f x))
The image of a tangent cone under the differential of a map is included in the tangent cone to the image.
theorem
has_fderiv_within_at.unique_diff_within_at
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{s : set E}
{f' : E βL[π] F}
{x : E} :
has_fderiv_within_at f f' s x β unique_diff_within_at π s x β closure (set.range βf') = set.univ β unique_diff_within_at π (f '' s) (f x)
If a set has the unique differentiability property at a point x, then the image of this set under a map with onto derivative has also the unique differentiability property at the image point.
theorem
has_fderiv_within_at.unique_diff_within_at_of_continuous_linear_equiv
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{f : E β F}
{s : set E}
{x : E}
(e' : E βL[π] F) :
has_fderiv_within_at f βe' s x β unique_diff_within_at π s x β unique_diff_within_at π (f '' s) (f x)
theorem
continuous_linear_equiv.unique_diff_on_preimage_iff
{π : Type u_1}
[nondiscrete_normed_field π]
{E : Type u_2}
[normed_group E]
[normed_space π E]
{F : Type u_3}
[normed_group F]
[normed_space π F]
{s : set E}
(e : F βL[π] E) :
unique_diff_on π (βe β»ΒΉ' s) β unique_diff_on π s
Restricting from β to β, or generally from π' to π
If a function is differentiable over β, then it is differentiable over β. In this paragraph,
we give variants of this statement, in the general situation where β and β are replaced
respectively by π' and π where π' is a normed algebra over π.
theorem
has_strict_fderiv_at.restrict_scalars
(π : Type u_1)
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π' E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : semimodule.restrict_scalars π π' E β semimodule.restrict_scalars π π' F}
{f' : semimodule.restrict_scalars π π' E βL[π'] semimodule.restrict_scalars π π' F}
{x : E} :
has_strict_fderiv_at f f' x β has_strict_fderiv_at f (continuous_linear_map.restrict_scalars π f') x
theorem
has_fderiv_at.restrict_scalars
(π : Type u_1)
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π' E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : semimodule.restrict_scalars π π' E β semimodule.restrict_scalars π π' F}
{f' : semimodule.restrict_scalars π π' E βL[π'] semimodule.restrict_scalars π π' F}
{x : E} :
has_fderiv_at f f' x β has_fderiv_at f (continuous_linear_map.restrict_scalars π f') x
theorem
has_fderiv_within_at.restrict_scalars
(π : Type u_1)
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π' E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : semimodule.restrict_scalars π π' E β semimodule.restrict_scalars π π' F}
{f' : semimodule.restrict_scalars π π' E βL[π'] semimodule.restrict_scalars π π' F}
{s : set E}
{x : E} :
has_fderiv_within_at f f' s x β has_fderiv_within_at f (continuous_linear_map.restrict_scalars π f') s x
theorem
differentiable_at.restrict_scalars
(π : Type u_1)
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π' E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : semimodule.restrict_scalars π π' E β semimodule.restrict_scalars π π' F}
{x : E} :
differentiable_at π' f x β differentiable_at π f x
theorem
differentiable_within_at.restrict_scalars
(π : Type u_1)
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π' E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : semimodule.restrict_scalars π π' E β semimodule.restrict_scalars π π' F}
{s : set E}
{x : E} :
differentiable_within_at π' f s x β differentiable_within_at π f s x
theorem
differentiable_on.restrict_scalars
(π : Type u_1)
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π' E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : semimodule.restrict_scalars π π' E β semimodule.restrict_scalars π π' F}
{s : set E} :
differentiable_on π' f s β differentiable_on π f s
theorem
differentiable.restrict_scalars
(π : Type u_1)
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π' E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : semimodule.restrict_scalars π π' E β semimodule.restrict_scalars π π' F} :
differentiable π' f β differentiable π f
Multiplying by a complex function respects real differentiability
Consider two functions c : E β β and f : E β F where F is a complex vector space. If both
c and f are differentiable over β, then so is their product. This paragraph proves this
statement, in the general version where β is replaced by a field π, and β is replaced
by a normed algebra π' over π.
theorem
has_strict_fderiv_at.smul_algebra
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : E β semimodule.restrict_scalars π π' F}
{f' : E βL[π] semimodule.restrict_scalars π π' F}
{x : E}
{c : E β π'}
{c' : E βL[π] π'} :
has_strict_fderiv_at c c' x β has_strict_fderiv_at f f' x β has_strict_fderiv_at (Ξ» (y : E), c y β’ f y) (c x β’ f' + c'.smul_algebra_right (f x)) x
theorem
has_fderiv_within_at.smul_algebra
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : E β semimodule.restrict_scalars π π' F}
{f' : E βL[π] semimodule.restrict_scalars π π' F}
{s : set E}
{x : E}
{c : E β π'}
{c' : E βL[π] π'} :
has_fderiv_within_at c c' s x β has_fderiv_within_at f f' s x β has_fderiv_within_at (Ξ» (y : E), c y β’ f y) (c x β’ f' + c'.smul_algebra_right (f x)) s x
theorem
has_fderiv_at.smul_algebra
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : E β semimodule.restrict_scalars π π' F}
{f' : E βL[π] semimodule.restrict_scalars π π' F}
{x : E}
{c : E β π'}
{c' : E βL[π] π'} :
has_fderiv_at c c' x β has_fderiv_at f f' x β has_fderiv_at (Ξ» (y : E), c y β’ f y) (c x β’ f' + c'.smul_algebra_right (f x)) x
theorem
differentiable_within_at.smul_algebra
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : E β semimodule.restrict_scalars π π' F}
{s : set E}
{x : E}
{c : E β π'} :
differentiable_within_at π c s x β differentiable_within_at π f s x β differentiable_within_at π (Ξ» (y : E), c y β’ f y) s x
@[simp]
theorem
differentiable_at.smul_algebra
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : E β semimodule.restrict_scalars π π' F}
{x : E}
{c : E β π'} :
differentiable_at π c x β differentiable_at π f x β differentiable_at π (Ξ» (y : E), c y β’ f y) x
theorem
differentiable_on.smul_algebra
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : E β semimodule.restrict_scalars π π' F}
{s : set E}
{c : E β π'} :
differentiable_on π c s β differentiable_on π f s β differentiable_on π (Ξ» (y : E), c y β’ f y) s
@[simp]
theorem
differentiable.smul_algebra
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : E β semimodule.restrict_scalars π π' F}
{c : E β π'} :
differentiable π c β differentiable π f β differentiable π (Ξ» (y : E), c y β’ f y)
theorem
fderiv_within_smul_algebra
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : E β semimodule.restrict_scalars π π' F}
{s : set E}
{x : E}
{c : E β π'} :
unique_diff_within_at π s x β differentiable_within_at π c s x β differentiable_within_at π f s x β fderiv_within π (Ξ» (y : E), c y β’ f y) s x = c x β’ fderiv_within π f s x + (fderiv_within π c s x).smul_algebra_right (f x)
theorem
fderiv_smul_algebra
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : E β semimodule.restrict_scalars π π' F}
{x : E}
{c : E β π'} :
differentiable_at π c x β differentiable_at π f x β fderiv π (Ξ» (y : E), c y β’ f y) x = c x β’ fderiv π f x + (fderiv π c x).smul_algebra_right (f x)
theorem
has_strict_fderiv_at.smul_algebra_const
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{x : E}
{c : E β π'}
{c' : E βL[π] π'}
(hc : has_strict_fderiv_at c c' x)
(f : semimodule.restrict_scalars π π' F) :
has_strict_fderiv_at (Ξ» (y : E), c y β’ f) (c'.smul_algebra_right f) x
theorem
has_fderiv_within_at.smul_algebra_const
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{s : set E}
{x : E}
{c : E β π'}
{c' : E βL[π] π'}
(hc : has_fderiv_within_at c c' s x)
(f : semimodule.restrict_scalars π π' F) :
has_fderiv_within_at (Ξ» (y : E), c y β’ f) (c'.smul_algebra_right f) s x
theorem
has_fderiv_at.smul_algebra_const
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{x : E}
{c : E β π'}
{c' : E βL[π] π'}
(hc : has_fderiv_at c c' x)
(f : semimodule.restrict_scalars π π' F) :
has_fderiv_at (Ξ» (y : E), c y β’ f) (c'.smul_algebra_right f) x
theorem
differentiable_within_at.smul_algebra_const
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{s : set E}
{x : E}
{c : E β π'}
(hc : differentiable_within_at π c s x)
(f : semimodule.restrict_scalars π π' F) :
differentiable_within_at π (Ξ» (y : E), c y β’ f) s x
theorem
differentiable_at.smul_algebra_const
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{x : E}
{c : E β π'}
(hc : differentiable_at π c x)
(f : semimodule.restrict_scalars π π' F) :
differentiable_at π (Ξ» (y : E), c y β’ f) x
theorem
differentiable_on.smul_algebra_const
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{s : set E}
{c : E β π'}
(hc : differentiable_on π c s)
(f : semimodule.restrict_scalars π π' F) :
differentiable_on π (Ξ» (y : E), c y β’ f) s
theorem
differentiable.smul_algebra_const
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{c : E β π'}
(hc : differentiable π c)
(f : semimodule.restrict_scalars π π' F) :
differentiable π (Ξ» (y : E), c y β’ f)
theorem
fderiv_within_smul_algebra_const
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{s : set E}
{x : E}
{c : E β π'}
(hxs : unique_diff_within_at π s x)
(hc : differentiable_within_at π c s x)
(f : semimodule.restrict_scalars π π' F) :
fderiv_within π (Ξ» (y : E), c y β’ f) s x = (fderiv_within π c s x).smul_algebra_right f
theorem
fderiv_smul_algebra_const
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{x : E}
{c : E β π'}
(hc : differentiable_at π c x)
(f : semimodule.restrict_scalars π π' F) :
fderiv π (Ξ» (y : E), c y β’ f) x = (fderiv π c x).smul_algebra_right f
theorem
has_strict_fderiv_at.const_smul_algebra
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : E β semimodule.restrict_scalars π π' F}
{f' : E βL[π] semimodule.restrict_scalars π π' F}
{x : E}
(h : has_strict_fderiv_at f f' x)
(c : π') :
has_strict_fderiv_at (Ξ» (x : E), c β’ f x) (c β’ f') x
theorem
has_fderiv_at_filter.const_smul_algebra
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : E β semimodule.restrict_scalars π π' F}
{f' : E βL[π] semimodule.restrict_scalars π π' F}
{x : E}
{L : filter E}
(h : has_fderiv_at_filter f f' x L)
(c : π') :
has_fderiv_at_filter (Ξ» (x : E), c β’ f x) (c β’ f') x L
theorem
has_fderiv_within_at.const_smul_algebra
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : E β semimodule.restrict_scalars π π' F}
{f' : E βL[π] semimodule.restrict_scalars π π' F}
{s : set E}
{x : E}
(h : has_fderiv_within_at f f' s x)
(c : π') :
has_fderiv_within_at (Ξ» (x : E), c β’ f x) (c β’ f') s x
theorem
has_fderiv_at.const_smul_algebra
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : E β semimodule.restrict_scalars π π' F}
{f' : E βL[π] semimodule.restrict_scalars π π' F}
{x : E}
(h : has_fderiv_at f f' x)
(c : π') :
has_fderiv_at (Ξ» (x : E), c β’ f x) (c β’ f') x
theorem
differentiable_within_at.const_smul_algebra
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : E β semimodule.restrict_scalars π π' F}
{s : set E}
{x : E}
(h : differentiable_within_at π f s x)
(c : π') :
differentiable_within_at π (Ξ» (y : E), c β’ f y) s x
theorem
differentiable_at.const_smul_algebra
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : E β semimodule.restrict_scalars π π' F}
{x : E}
(h : differentiable_at π f x)
(c : π') :
differentiable_at π (Ξ» (y : E), c β’ f y) x
theorem
differentiable_on.const_smul_algebra
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : E β semimodule.restrict_scalars π π' F}
{s : set E}
(h : differentiable_on π f s)
(c : π') :
differentiable_on π (Ξ» (y : E), c β’ f y) s
theorem
differentiable.const_smul_algebra
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : E β semimodule.restrict_scalars π π' F}
(h : differentiable π f)
(c : π') :
differentiable π (Ξ» (y : E), c β’ f y)
theorem
fderiv_within_const_smul_algebra
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : E β semimodule.restrict_scalars π π' F}
{s : set E}
{x : E}
(hxs : unique_diff_within_at π s x)
(h : differentiable_within_at π f s x)
(c : π') :
fderiv_within π (Ξ» (y : E), c β’ f y) s x = c β’ fderiv_within π f s x
theorem
fderiv_const_smul_algebra
{π : Type u_1}
[nondiscrete_normed_field π]
{π' : Type u_2}
[nondiscrete_normed_field π']
[normed_algebra π π']
{E : Type u_3}
[normed_group E]
[normed_space π E]
{F : Type u_4}
[normed_group F]
[normed_space π' F]
{f : E β semimodule.restrict_scalars π π' F}
{x : E}
(h : differentiable_at π f x)
(c : π') :