mathlib3 documentation

analysis.calculus.fderiv.mul

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

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) :
fderiv 𝕜 (λ (y : E), (c y).comp (d y)) x = ((continuous_linear_map.compL 𝕜 F G H) (c x)).comp (fderiv 𝕜 d x) + (((continuous_linear_map.compL 𝕜 F G H).flip) (d x)).comp (fderiv 𝕜 c 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) :
has_strict_fderiv_at (λ (y : E), (c y) (u y)) ((c x).comp u' + (c'.flip) (u x)) 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) :
has_fderiv_within_at (λ (y : E), (c y) (u y)) ((c x).comp u' + (c'.flip) (u x)) 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) :
has_fderiv_at (λ (y : E), (c y) (u y)) ((c x).comp u' + (c'.flip) (u x)) 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) :
fderiv 𝕜 (λ (y : E), (c y) (u y)) x = (c x).comp (fderiv 𝕜 u x) + ((fderiv 𝕜 c x).flip) (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) :
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} [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) :
fderiv 𝕜 (λ (y : E), a y * b y) x = a x fderiv 𝕜 b x + (fderiv 𝕜 a x).smul_right (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) :
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} [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 : 𝔸') :
fderiv 𝕜 (λ (y : E), c y * d) x = d fderiv 𝕜 c x
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 : 𝔸) :
fderiv 𝕜 (λ (y : E), b * a y) x = b fderiv 𝕜 a 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_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.

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

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

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)⁻¹)