Multiplicative operations on derivatives #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
For detailed documentation of the Fréchet derivative,
see the module docstring of analysis/calculus/fderiv/basic.lean.
This file contains the usual formulas (and existence assertions) for the derivative of
- multiplication of a function by a scalar function
- multiplication of two scalar functions
- inverse function (assuming that it exists; the inverse function theorem is in
../inverse.lean)
Derivative of the pointwise composition/application of continuous linear maps #
theorem
has_strict_fderiv_at.clm_comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{H : Type u_6}
[normed_add_comm_group H]
[normed_space 𝕜 H]
{c : E → (G →L[𝕜] H)}
{c' : E →L[𝕜] G →L[𝕜] H}
{d : E → (F →L[𝕜] G)}
{d' : E →L[𝕜] F →L[𝕜] G}
(hc : has_strict_fderiv_at c c' x)
(hd : has_strict_fderiv_at d d' x) :
has_strict_fderiv_at (λ (y : E), (c y).comp (d y)) ((⇑(continuous_linear_map.compL 𝕜 F G H) (c x)).comp d' + (⇑((continuous_linear_map.compL 𝕜 F G H).flip) (d x)).comp c') x
theorem
has_fderiv_within_at.clm_comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{s : set E}
{H : Type u_6}
[normed_add_comm_group H]
[normed_space 𝕜 H]
{c : E → (G →L[𝕜] H)}
{c' : E →L[𝕜] G →L[𝕜] H}
{d : E → (F →L[𝕜] G)}
{d' : E →L[𝕜] F →L[𝕜] G}
(hc : has_fderiv_within_at c c' s x)
(hd : has_fderiv_within_at d d' s x) :
has_fderiv_within_at (λ (y : E), (c y).comp (d y)) ((⇑(continuous_linear_map.compL 𝕜 F G H) (c x)).comp d' + (⇑((continuous_linear_map.compL 𝕜 F G H).flip) (d x)).comp c') s x
theorem
has_fderiv_at.clm_comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{H : Type u_6}
[normed_add_comm_group H]
[normed_space 𝕜 H]
{c : E → (G →L[𝕜] H)}
{c' : E →L[𝕜] G →L[𝕜] H}
{d : E → (F →L[𝕜] G)}
{d' : E →L[𝕜] F →L[𝕜] G}
(hc : has_fderiv_at c c' x)
(hd : has_fderiv_at d d' x) :
has_fderiv_at (λ (y : E), (c y).comp (d y)) ((⇑(continuous_linear_map.compL 𝕜 F G H) (c x)).comp d' + (⇑((continuous_linear_map.compL 𝕜 F G H).flip) (d x)).comp c') x
theorem
differentiable_within_at.clm_comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{s : set E}
{H : Type u_6}
[normed_add_comm_group H]
[normed_space 𝕜 H]
{c : E → (G →L[𝕜] H)}
{d : E → (F →L[𝕜] G)}
(hc : differentiable_within_at 𝕜 c s x)
(hd : differentiable_within_at 𝕜 d s x) :
differentiable_within_at 𝕜 (λ (y : E), (c y).comp (d y)) s x
theorem
differentiable_at.clm_comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{H : Type u_6}
[normed_add_comm_group H]
[normed_space 𝕜 H]
{c : E → (G →L[𝕜] H)}
{d : E → (F →L[𝕜] G)}
(hc : differentiable_at 𝕜 c x)
(hd : differentiable_at 𝕜 d x) :
differentiable_at 𝕜 (λ (y : E), (c y).comp (d y)) x
theorem
differentiable_on.clm_comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{s : set E}
{H : Type u_6}
[normed_add_comm_group H]
[normed_space 𝕜 H]
{c : E → (G →L[𝕜] H)}
{d : E → (F →L[𝕜] G)}
(hc : differentiable_on 𝕜 c s)
(hd : differentiable_on 𝕜 d s) :
differentiable_on 𝕜 (λ (y : E), (c y).comp (d y)) s
theorem
differentiable.clm_comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{H : Type u_6}
[normed_add_comm_group H]
[normed_space 𝕜 H]
{c : E → (G →L[𝕜] H)}
{d : E → (F →L[𝕜] G)}
(hc : differentiable 𝕜 c)
(hd : differentiable 𝕜 d) :
differentiable 𝕜 (λ (y : E), (c y).comp (d y))
theorem
fderiv_within_clm_comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{s : set E}
{H : Type u_6}
[normed_add_comm_group H]
[normed_space 𝕜 H]
{c : E → (G →L[𝕜] H)}
{d : E → (F →L[𝕜] G)}
(hxs : unique_diff_within_at 𝕜 s x)
(hc : differentiable_within_at 𝕜 c s x)
(hd : differentiable_within_at 𝕜 d s x) :
fderiv_within 𝕜 (λ (y : E), (c y).comp (d y)) s x = (⇑(continuous_linear_map.compL 𝕜 F G H) (c x)).comp (fderiv_within 𝕜 d s x) + (⇑((continuous_linear_map.compL 𝕜 F G H).flip) (d x)).comp (fderiv_within 𝕜 c s x)
theorem
fderiv_clm_comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{H : Type u_6}
[normed_add_comm_group H]
[normed_space 𝕜 H]
{c : E → (G →L[𝕜] H)}
{d : E → (F →L[𝕜] G)}
(hc : differentiable_at 𝕜 c x)
(hd : differentiable_at 𝕜 d x) :
theorem
has_strict_fderiv_at.clm_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{H : Type u_6}
[normed_add_comm_group H]
[normed_space 𝕜 H]
{c : E → (G →L[𝕜] H)}
{c' : E →L[𝕜] G →L[𝕜] H}
{u : E → G}
{u' : E →L[𝕜] G}
(hc : has_strict_fderiv_at c c' x)
(hu : has_strict_fderiv_at u u' x) :
theorem
has_fderiv_within_at.clm_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{s : set E}
{H : Type u_6}
[normed_add_comm_group H]
[normed_space 𝕜 H]
{c : E → (G →L[𝕜] H)}
{c' : E →L[𝕜] G →L[𝕜] H}
{u : E → G}
{u' : E →L[𝕜] G}
(hc : has_fderiv_within_at c c' s x)
(hu : has_fderiv_within_at u u' s x) :
theorem
has_fderiv_at.clm_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{H : Type u_6}
[normed_add_comm_group H]
[normed_space 𝕜 H]
{c : E → (G →L[𝕜] H)}
{c' : E →L[𝕜] G →L[𝕜] H}
{u : E → G}
{u' : E →L[𝕜] G}
(hc : has_fderiv_at c c' x)
(hu : has_fderiv_at u u' x) :
theorem
differentiable_within_at.clm_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{s : set E}
{H : Type u_6}
[normed_add_comm_group H]
[normed_space 𝕜 H]
{c : E → (G →L[𝕜] H)}
{u : E → G}
(hc : differentiable_within_at 𝕜 c s x)
(hu : differentiable_within_at 𝕜 u s x) :
differentiable_within_at 𝕜 (λ (y : E), ⇑(c y) (u y)) s x
theorem
differentiable_at.clm_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{H : Type u_6}
[normed_add_comm_group H]
[normed_space 𝕜 H]
{c : E → (G →L[𝕜] H)}
{u : E → G}
(hc : differentiable_at 𝕜 c x)
(hu : differentiable_at 𝕜 u x) :
differentiable_at 𝕜 (λ (y : E), ⇑(c y) (u y)) x
theorem
differentiable_on.clm_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{s : set E}
{H : Type u_6}
[normed_add_comm_group H]
[normed_space 𝕜 H]
{c : E → (G →L[𝕜] H)}
{u : E → G}
(hc : differentiable_on 𝕜 c s)
(hu : differentiable_on 𝕜 u s) :
differentiable_on 𝕜 (λ (y : E), ⇑(c y) (u y)) s
theorem
differentiable.clm_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{H : Type u_6}
[normed_add_comm_group H]
[normed_space 𝕜 H]
{c : E → (G →L[𝕜] H)}
{u : E → G}
(hc : differentiable 𝕜 c)
(hu : differentiable 𝕜 u) :
differentiable 𝕜 (λ (y : E), ⇑(c y) (u y))
theorem
fderiv_within_clm_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{s : set E}
{H : Type u_6}
[normed_add_comm_group H]
[normed_space 𝕜 H]
{c : E → (G →L[𝕜] H)}
{u : E → G}
(hxs : unique_diff_within_at 𝕜 s x)
(hc : differentiable_within_at 𝕜 c s x)
(hu : differentiable_within_at 𝕜 u s x) :
fderiv_within 𝕜 (λ (y : E), ⇑(c y) (u y)) s x = (c x).comp (fderiv_within 𝕜 u s x) + ⇑((fderiv_within 𝕜 c s x).flip) (u x)
theorem
fderiv_clm_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{H : Type u_6}
[normed_add_comm_group H]
[normed_space 𝕜 H]
{c : E → (G →L[𝕜] H)}
{u : E → G}
(hc : differentiable_at 𝕜 c x)
(hu : differentiable_at 𝕜 u x) :
Derivative of the product of a scalar-valued function and a vector-valued function #
If c is a differentiable scalar-valued function and f is a differentiable vector-valued
function, then λ x, c x • f x is differentiable as well. Lemmas in this section works for
function c taking values in the base field, as well as in a normed algebra over the base
field: e.g., they work for c : E → ℂ and f : E → F provided that F is a complex
normed vector space.
theorem
has_strict_fderiv_at.smul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
{f' : E →L[𝕜] F}
{x : E}
{𝕜' : Type u_6}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{c : E → 𝕜'}
{c' : E →L[𝕜] 𝕜'}
(hc : has_strict_fderiv_at c c' x)
(hf : 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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
{f' : E →L[𝕜] F}
{x : E}
{s : set E}
{𝕜' : Type u_6}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{c : E → 𝕜'}
{c' : E →L[𝕜] 𝕜'}
(hc : has_fderiv_within_at c c' s x)
(hf : 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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
{f' : E →L[𝕜] F}
{x : E}
{𝕜' : Type u_6}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{c : E → 𝕜'}
{c' : E →L[𝕜] 𝕜'}
(hc : has_fderiv_at c c' x)
(hf : 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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
{x : E}
{s : set E}
{𝕜' : Type u_6}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hc : differentiable_within_at 𝕜 c s x)
(hf : 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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
{x : E}
{𝕜' : Type u_6}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hc : differentiable_at 𝕜 c x)
(hf : differentiable_at 𝕜 f x) :
differentiable_at 𝕜 (λ (y : E), c y • f y) x
theorem
differentiable_on.smul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
{s : set E}
{𝕜' : Type u_6}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hc : differentiable_on 𝕜 c s)
(hf : differentiable_on 𝕜 f s) :
differentiable_on 𝕜 (λ (y : E), c y • f y) s
@[simp]
theorem
differentiable.smul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
{𝕜' : Type u_6}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hc : differentiable 𝕜 c)
(hf : differentiable 𝕜 f) :
differentiable 𝕜 (λ (y : E), c y • f y)
theorem
fderiv_within_smul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
{x : E}
{s : set E}
{𝕜' : Type u_6}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hxs : unique_diff_within_at 𝕜 s x)
(hc : differentiable_within_at 𝕜 c s x)
(hf : 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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
{x : E}
{𝕜' : Type u_6}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hc : differentiable_at 𝕜 c x)
(hf : differentiable_at 𝕜 f x) :
theorem
has_strict_fderiv_at.smul_const
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : E}
{𝕜' : Type u_6}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : E}
{s : set E}
{𝕜' : Type u_6}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : E}
{𝕜' : Type u_6}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : E}
{s : set E}
{𝕜' : Type u_6}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : E}
{𝕜' : Type u_6}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{s : set E}
{𝕜' : Type u_6}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hc : differentiable_on 𝕜 c s)
(f : F) :
differentiable_on 𝕜 (λ (y : E), c y • f) s
theorem
differentiable.smul_const
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{𝕜' : Type u_6}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hc : differentiable 𝕜 c)
(f : F) :
differentiable 𝕜 (λ (y : E), c y • f)
theorem
fderiv_within_smul_const
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : E}
{s : set E}
{𝕜' : Type u_6}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : E}
{𝕜' : Type u_6}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{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 functions #
theorem
has_strict_fderiv_at.mul'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a b : E → 𝔸}
{a' b' : E →L[𝕜] 𝔸}
{x : E}
(ha : has_strict_fderiv_at a a' x)
(hb : has_strict_fderiv_at b b' x) :
has_strict_fderiv_at (λ (y : E), a y * b y) (a x • b' + a'.smul_right (b x)) x
theorem
has_strict_fderiv_at.mul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{𝔸' : Type u_7}
[normed_comm_ring 𝔸']
[normed_algebra 𝕜 𝔸']
{c d : E → 𝔸'}
{c' d' : E →L[𝕜] 𝔸'}
(hc : has_strict_fderiv_at c c' x)
(hd : 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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{s : set E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a b : E → 𝔸}
{a' b' : E →L[𝕜] 𝔸}
(ha : has_fderiv_within_at a a' s x)
(hb : has_fderiv_within_at b b' s x) :
has_fderiv_within_at (λ (y : E), a y * b y) (a x • b' + a'.smul_right (b x)) s x
theorem
has_fderiv_within_at.mul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{s : set E}
{𝔸' : Type u_7}
[normed_comm_ring 𝔸']
[normed_algebra 𝕜 𝔸']
{c d : E → 𝔸'}
{c' d' : E →L[𝕜] 𝔸'}
(hc : has_fderiv_within_at c c' s x)
(hd : 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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a b : E → 𝔸}
{a' b' : E →L[𝕜] 𝔸}
(ha : has_fderiv_at a a' x)
(hb : has_fderiv_at b b' x) :
has_fderiv_at (λ (y : E), a y * b y) (a x • b' + a'.smul_right (b x)) x
theorem
has_fderiv_at.mul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{𝔸' : Type u_7}
[normed_comm_ring 𝔸']
[normed_algebra 𝕜 𝔸']
{c d : E → 𝔸'}
{c' d' : E →L[𝕜] 𝔸'}
(hc : has_fderiv_at c c' x)
(hd : 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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{s : set E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a b : E → 𝔸}
(ha : differentiable_within_at 𝕜 a s x)
(hb : differentiable_within_at 𝕜 b s x) :
differentiable_within_at 𝕜 (λ (y : E), a y * b y) s x
@[simp]
theorem
differentiable_at.mul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a b : E → 𝔸}
(ha : differentiable_at 𝕜 a x)
(hb : differentiable_at 𝕜 b x) :
differentiable_at 𝕜 (λ (y : E), a y * b y) x
theorem
differentiable_on.mul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{s : set E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a b : E → 𝔸}
(ha : differentiable_on 𝕜 a s)
(hb : differentiable_on 𝕜 b s) :
differentiable_on 𝕜 (λ (y : E), a y * b y) s
@[simp]
theorem
differentiable.mul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a b : E → 𝔸}
(ha : differentiable 𝕜 a)
(hb : differentiable 𝕜 b) :
differentiable 𝕜 (λ (y : E), a y * b y)
theorem
differentiable_within_at.pow
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{s : set E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a : E → 𝔸}
(ha : differentiable_within_at 𝕜 a s x)
(n : ℕ) :
differentiable_within_at 𝕜 (λ (x : E), a x ^ n) s x
@[simp]
theorem
differentiable_at.pow
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a : E → 𝔸}
(ha : differentiable_at 𝕜 a x)
(n : ℕ) :
differentiable_at 𝕜 (λ (x : E), a x ^ n) x
theorem
differentiable_on.pow
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{s : set E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a : E → 𝔸}
(ha : differentiable_on 𝕜 a s)
(n : ℕ) :
differentiable_on 𝕜 (λ (x : E), a x ^ n) s
@[simp]
theorem
differentiable.pow
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a : E → 𝔸}
(ha : differentiable 𝕜 a)
(n : ℕ) :
differentiable 𝕜 (λ (x : E), a x ^ n)
theorem
fderiv_within_mul'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{s : set E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a b : E → 𝔸}
(hxs : unique_diff_within_at 𝕜 s x)
(ha : differentiable_within_at 𝕜 a s x)
(hb : differentiable_within_at 𝕜 b s x) :
fderiv_within 𝕜 (λ (y : E), a y * b y) s x = a x • fderiv_within 𝕜 b s x + (fderiv_within 𝕜 a s x).smul_right (b x)
theorem
fderiv_within_mul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{s : set E}
{𝔸' : Type u_7}
[normed_comm_ring 𝔸']
[normed_algebra 𝕜 𝔸']
{c d : E → 𝔸'}
(hxs : unique_diff_within_at 𝕜 s x)
(hc : differentiable_within_at 𝕜 c s x)
(hd : 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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a b : E → 𝔸}
(ha : differentiable_at 𝕜 a x)
(hb : differentiable_at 𝕜 b x) :
theorem
fderiv_mul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{𝔸' : Type u_7}
[normed_comm_ring 𝔸']
[normed_algebra 𝕜 𝔸']
{c d : E → 𝔸'}
(hc : differentiable_at 𝕜 c x)
(hd : differentiable_at 𝕜 d x) :
theorem
has_strict_fderiv_at.mul_const'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a : E → 𝔸}
{a' : E →L[𝕜] 𝔸}
(ha : has_strict_fderiv_at a a' x)
(b : 𝔸) :
has_strict_fderiv_at (λ (y : E), a y * b) (a'.smul_right b) x
theorem
has_strict_fderiv_at.mul_const
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{𝔸' : Type u_7}
[normed_comm_ring 𝔸']
[normed_algebra 𝕜 𝔸']
{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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{s : set E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a : E → 𝔸}
{a' : E →L[𝕜] 𝔸}
(ha : has_fderiv_within_at a a' s x)
(b : 𝔸) :
has_fderiv_within_at (λ (y : E), a y * b) (a'.smul_right b) s x
theorem
has_fderiv_within_at.mul_const
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{s : set E}
{𝔸' : Type u_7}
[normed_comm_ring 𝔸']
[normed_algebra 𝕜 𝔸']
{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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a : E → 𝔸}
{a' : E →L[𝕜] 𝔸}
(ha : has_fderiv_at a a' x)
(b : 𝔸) :
has_fderiv_at (λ (y : E), a y * b) (a'.smul_right b) x
theorem
has_fderiv_at.mul_const
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{𝔸' : Type u_7}
[normed_comm_ring 𝔸']
[normed_algebra 𝕜 𝔸']
{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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{s : set E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a : E → 𝔸}
(ha : differentiable_within_at 𝕜 a s x)
(b : 𝔸) :
differentiable_within_at 𝕜 (λ (y : E), a y * b) s x
theorem
differentiable_at.mul_const
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a : E → 𝔸}
(ha : differentiable_at 𝕜 a x)
(b : 𝔸) :
differentiable_at 𝕜 (λ (y : E), a y * b) x
theorem
differentiable_on.mul_const
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{s : set E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a : E → 𝔸}
(ha : differentiable_on 𝕜 a s)
(b : 𝔸) :
differentiable_on 𝕜 (λ (y : E), a y * b) s
theorem
differentiable.mul_const
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a : E → 𝔸}
(ha : differentiable 𝕜 a)
(b : 𝔸) :
differentiable 𝕜 (λ (y : E), a y * b)
theorem
fderiv_within_mul_const'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{s : set E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a : E → 𝔸}
(hxs : unique_diff_within_at 𝕜 s x)
(ha : differentiable_within_at 𝕜 a s x)
(b : 𝔸) :
fderiv_within 𝕜 (λ (y : E), a y * b) s x = (fderiv_within 𝕜 a s x).smul_right b
theorem
fderiv_within_mul_const
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{s : set E}
{𝔸' : Type u_7}
[normed_comm_ring 𝔸']
[normed_algebra 𝕜 𝔸']
{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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a : E → 𝔸}
(ha : differentiable_at 𝕜 a x)
(b : 𝔸) :
fderiv 𝕜 (λ (y : E), a y * b) x = (fderiv 𝕜 a x).smul_right b
theorem
fderiv_mul_const
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{𝔸' : Type u_7}
[normed_comm_ring 𝔸']
[normed_algebra 𝕜 𝔸']
{c : E → 𝔸'}
(hc : differentiable_at 𝕜 c x)
(d : 𝔸') :
theorem
has_strict_fderiv_at.const_mul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a : E → 𝔸}
{a' : E →L[𝕜] 𝔸}
(ha : has_strict_fderiv_at a a' x)
(b : 𝔸) :
has_strict_fderiv_at (λ (y : E), b * a y) (b • a') x
theorem
has_fderiv_within_at.const_mul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{s : set E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a : E → 𝔸}
{a' : E →L[𝕜] 𝔸}
(ha : has_fderiv_within_at a a' s x)
(b : 𝔸) :
has_fderiv_within_at (λ (y : E), b * a y) (b • a') s x
theorem
has_fderiv_at.const_mul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a : E → 𝔸}
{a' : E →L[𝕜] 𝔸}
(ha : has_fderiv_at a a' x)
(b : 𝔸) :
has_fderiv_at (λ (y : E), b * a y) (b • a') x
theorem
differentiable_within_at.const_mul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{s : set E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a : E → 𝔸}
(ha : differentiable_within_at 𝕜 a s x)
(b : 𝔸) :
differentiable_within_at 𝕜 (λ (y : E), b * a y) s x
theorem
differentiable_at.const_mul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a : E → 𝔸}
(ha : differentiable_at 𝕜 a x)
(b : 𝔸) :
differentiable_at 𝕜 (λ (y : E), b * a y) x
theorem
differentiable_on.const_mul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{s : set E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a : E → 𝔸}
(ha : differentiable_on 𝕜 a s)
(b : 𝔸) :
differentiable_on 𝕜 (λ (y : E), b * a y) s
theorem
differentiable.const_mul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a : E → 𝔸}
(ha : differentiable 𝕜 a)
(b : 𝔸) :
differentiable 𝕜 (λ (y : E), b * a y)
theorem
fderiv_within_const_mul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{s : set E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a : E → 𝔸}
(hxs : unique_diff_within_at 𝕜 s x)
(ha : differentiable_within_at 𝕜 a s x)
(b : 𝔸) :
fderiv_within 𝕜 (λ (y : E), b * a y) s x = b • fderiv_within 𝕜 a s x
theorem
fderiv_const_mul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{𝔸 : Type u_6}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{a : E → 𝔸}
(ha : differentiable_at 𝕜 a x)
(b : 𝔸) :
theorem
has_fderiv_at_ring_inverse
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{R : Type u_6}
[normed_ring R]
[normed_algebra 𝕜 R]
[complete_space R]
(x : Rˣ) :
has_fderiv_at ring.inverse (-⇑(⇑(continuous_linear_map.mul_left_right 𝕜 R) ↑x⁻¹) ↑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}
[nontrivially_normed_field 𝕜]
{R : Type u_6}
[normed_ring R]
[normed_algebra 𝕜 R]
[complete_space R]
{x : R}
(hx : is_unit x) :
theorem
differentiable_within_at_inverse
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{R : Type u_6}
[normed_ring R]
[normed_algebra 𝕜 R]
[complete_space R]
{x : R}
(hx : is_unit x)
(s : set R) :
theorem
differentiable_on_inverse
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{R : Type u_6}
[normed_ring R]
[normed_algebra 𝕜 R]
[complete_space R] :
differentiable_on 𝕜 ring.inverse {x : R | is_unit x}
theorem
fderiv_inverse
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{R : Type u_6}
[normed_ring R]
[normed_algebra 𝕜 R]
[complete_space R]
(x : Rˣ) :
theorem
differentiable_within_at.inverse
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{R : Type u_6}
[normed_ring R]
[normed_algebra 𝕜 R]
[complete_space R]
{h : E → R}
{z : E}
{S : set E}
(hf : differentiable_within_at 𝕜 h S z)
(hz : is_unit (h z)) :
differentiable_within_at 𝕜 (λ (x : E), ring.inverse (h x)) S z
@[simp]
theorem
differentiable_at.inverse
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{R : Type u_6}
[normed_ring R]
[normed_algebra 𝕜 R]
[complete_space R]
{h : E → R}
{z : E}
(hf : differentiable_at 𝕜 h z)
(hz : is_unit (h z)) :
differentiable_at 𝕜 (λ (x : E), ring.inverse (h x)) z
theorem
differentiable_on.inverse
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{R : Type u_6}
[normed_ring R]
[normed_algebra 𝕜 R]
[complete_space R]
{h : E → R}
{S : set E}
(hf : differentiable_on 𝕜 h S)
(hz : ∀ (x : E), x ∈ S → is_unit (h x)) :
differentiable_on 𝕜 (λ (x : E), ring.inverse (h x)) S
@[simp]
theorem
differentiable.inverse
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{R : Type u_6}
[normed_ring R]
[normed_algebra 𝕜 R]
[complete_space R]
{h : E → R}
(hf : differentiable 𝕜 h)
(hz : ∀ (x : E), is_unit (h x)) :
differentiable 𝕜 (λ (x : E), ring.inverse (h x))
Derivative of the inverse in a division ring #
Note these lemmas are primed as they need complete_space R, whereas the other lemmas in
deriv/inv.lean do not, but instead need nontrivially_normed_field R.
theorem
has_fderiv_at_inv'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{R : Type u_6}
[normed_division_ring R]
[normed_algebra 𝕜 R]
[complete_space R]
{x : R}
(hx : x ≠ 0) :
has_fderiv_at has_inv.inv (-⇑(⇑(continuous_linear_map.mul_left_right 𝕜 R) x⁻¹) x⁻¹) x
At an invertible element x of a normed division algebra R, the Fréchet derivative of the
inversion operation is the linear map λ t, - x⁻¹ * t * x⁻¹.
theorem
differentiable_at_inv'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{R : Type u_6}
[normed_division_ring R]
[normed_algebra 𝕜 R]
[complete_space R]
{x : R}
(hx : x ≠ 0) :
theorem
differentiable_within_at_inv'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{R : Type u_6}
[normed_division_ring R]
[normed_algebra 𝕜 R]
[complete_space R]
{x : R}
(hx : x ≠ 0)
(s : set R) :
differentiable_within_at 𝕜 (λ (x : R), x⁻¹) s x
theorem
differentiable_on_inv'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{R : Type u_6}
[normed_division_ring R]
[normed_algebra 𝕜 R]
[complete_space R] :
differentiable_on 𝕜 (λ (x : R), x⁻¹) {x : R | x ≠ 0}
theorem
fderiv_inv'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{R : Type u_6}
[normed_division_ring R]
[normed_algebra 𝕜 R]
[complete_space R]
{x : R}
(hx : x ≠ 0) :
fderiv 𝕜 has_inv.inv x = -⇑(⇑(continuous_linear_map.mul_left_right 𝕜 R) x⁻¹) x⁻¹
Non-commutative version of fderiv_inv
theorem
fderiv_within_inv'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{R : Type u_6}
[normed_division_ring R]
[normed_algebra 𝕜 R]
[complete_space R]
{s : set R}
{x : R}
(hx : x ≠ 0)
(hxs : unique_diff_within_at 𝕜 s x) :
fderiv_within 𝕜 (λ (x : R), x⁻¹) s x = -⇑(⇑(continuous_linear_map.mul_left_right 𝕜 R) x⁻¹) x⁻¹
Non-commutative version of fderiv_within_inv
theorem
differentiable_within_at.inv'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{R : Type u_6}
[normed_division_ring R]
[normed_algebra 𝕜 R]
[complete_space R]
{h : E → R}
{z : E}
{S : set E}
(hf : differentiable_within_at 𝕜 h S z)
(hz : h z ≠ 0) :
differentiable_within_at 𝕜 (λ (x : E), (h x)⁻¹) S z
@[simp]
theorem
differentiable_at.inv'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{R : Type u_6}
[normed_division_ring R]
[normed_algebra 𝕜 R]
[complete_space R]
{h : E → R}
{z : E}
(hf : differentiable_at 𝕜 h z)
(hz : h z ≠ 0) :
differentiable_at 𝕜 (λ (x : E), (h x)⁻¹) z
theorem
differentiable_on.inv'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{R : Type u_6}
[normed_division_ring R]
[normed_algebra 𝕜 R]
[complete_space R]
{h : E → R}
{S : set E}
(hf : differentiable_on 𝕜 h S)
(hz : ∀ (x : E), x ∈ S → h x ≠ 0) :
differentiable_on 𝕜 (λ (x : E), (h x)⁻¹) S
@[simp]
theorem
differentiable.inv'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{R : Type u_6}
[normed_division_ring R]
[normed_algebra 𝕜 R]
[complete_space R]
{h : E → R}
(hf : differentiable 𝕜 h)
(hz : ∀ (x : E), h x ≠ 0) :
differentiable 𝕜 (λ (x : E), (h x)⁻¹)