mathlib3 documentation

analysis.calculus.fderiv.add

Additive 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 a function multiplied by a constant #

theorem has_strict_fderiv_at.const_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} {R : Type u_6} [semiring R] [module R F] [smul_comm_class 𝕜 R F] [has_continuous_const_smul R F] (h : has_strict_fderiv_at f f' x) (c : R) :
has_strict_fderiv_at (λ (x : E), c f x) (c f') x
theorem has_fderiv_at_filter.const_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} {L : filter E} {R : Type u_6} [semiring R] [module R F] [smul_comm_class 𝕜 R F] [has_continuous_const_smul R F] (h : has_fderiv_at_filter f f' x L) (c : R) :
has_fderiv_at_filter (λ (x : E), c f x) (c f') x L
theorem has_fderiv_within_at.const_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} {R : Type u_6} [semiring R] [module R F] [smul_comm_class 𝕜 R F] [has_continuous_const_smul R F] (h : has_fderiv_within_at f f' s x) (c : R) :
has_fderiv_within_at (λ (x : E), c f x) (c f') s x
theorem has_fderiv_at.const_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} {R : Type u_6} [semiring R] [module R F] [smul_comm_class 𝕜 R F] [has_continuous_const_smul R F] (h : has_fderiv_at f f' x) (c : R) :
has_fderiv_at (λ (x : E), c f x) (c f') x
theorem differentiable_within_at.const_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} {R : Type u_6} [semiring R] [module R F] [smul_comm_class 𝕜 R F] [has_continuous_const_smul R F] (h : differentiable_within_at 𝕜 f s x) (c : R) :
differentiable_within_at 𝕜 (λ (y : E), c f y) s x
theorem differentiable_at.const_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} {R : Type u_6} [semiring R] [module R F] [smul_comm_class 𝕜 R F] [has_continuous_const_smul R F] (h : differentiable_at 𝕜 f x) (c : R) :
differentiable_at 𝕜 (λ (y : E), c f y) x
theorem differentiable_on.const_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} {R : Type u_6} [semiring R] [module R F] [smul_comm_class 𝕜 R F] [has_continuous_const_smul R F] (h : differentiable_on 𝕜 f s) (c : R) :
differentiable_on 𝕜 (λ (y : E), c f y) s
theorem differentiable.const_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} {R : Type u_6} [semiring R] [module R F] [smul_comm_class 𝕜 R F] [has_continuous_const_smul R F] (h : differentiable 𝕜 f) (c : R) :
differentiable 𝕜 (λ (y : E), c f y)
theorem fderiv_within_const_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} {R : Type u_6} [semiring R] [module R F] [smul_comm_class 𝕜 R F] [has_continuous_const_smul R F] (hxs : unique_diff_within_at 𝕜 s x) (h : differentiable_within_at 𝕜 f s x) (c : R) :
fderiv_within 𝕜 (λ (y : E), c f y) s x = c fderiv_within 𝕜 f s x
theorem fderiv_const_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} {R : Type u_6} [semiring R] [module R F] [smul_comm_class 𝕜 R F] [has_continuous_const_smul R F] (h : differentiable_at 𝕜 f x) (c : R) :
fderiv 𝕜 (λ (y : E), c f y) x = c fderiv 𝕜 f x

Derivative of the sum of two functions #

theorem has_strict_fderiv_at.add {𝕜 : 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 g : E F} {f' g' : E →L[𝕜] F} {x : E} (hf : has_strict_fderiv_at f f' x) (hg : 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} [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 g : E F} {f' g' : E →L[𝕜] F} {x : E} {L : filter E} (hf : has_fderiv_at_filter f f' x L) (hg : 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} [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 g : E F} {f' g' : E →L[𝕜] F} {x : E} {s : set E} (hf : has_fderiv_within_at f f' s x) (hg : 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} [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 g : E F} {f' g' : E →L[𝕜] F} {x : E} (hf : has_fderiv_at f f' x) (hg : 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} [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 g : E F} {x : E} {s : set E} (hf : differentiable_within_at 𝕜 f s x) (hg : 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} [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 g : E F} {x : E} (hf : differentiable_at 𝕜 f x) (hg : differentiable_at 𝕜 g x) :
differentiable_at 𝕜 (λ (y : E), f y + g y) x
theorem differentiable_on.add {𝕜 : 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 g : E F} {s : set E} (hf : differentiable_on 𝕜 f s) (hg : differentiable_on 𝕜 g s) :
differentiable_on 𝕜 (λ (y : E), f y + g y) s
@[simp]
theorem differentiable.add {𝕜 : 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 g : E F} (hf : differentiable 𝕜 f) (hg : differentiable 𝕜 g) :
differentiable 𝕜 (λ (y : E), f y + g y)
theorem fderiv_within_add {𝕜 : 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 g : E F} {x : E} {s : set E} (hxs : unique_diff_within_at 𝕜 s x) (hf : differentiable_within_at 𝕜 f s x) (hg : 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} [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 g : E F} {x : E} (hf : differentiable_at 𝕜 f x) (hg : 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} [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} (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} [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} {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} [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} (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} [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} (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} [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} (hf : differentiable_within_at 𝕜 f s x) (c : F) :
differentiable_within_at 𝕜 (λ (y : E), f y + c) s x
@[simp]
theorem differentiable_within_at_add_const_iff {𝕜 : 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} (c : F) :
differentiable_within_at 𝕜 (λ (y : E), f y + c) s x differentiable_within_at 𝕜 f s x
theorem differentiable_at.add_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] {f : E F} {x : E} (hf : differentiable_at 𝕜 f x) (c : F) :
differentiable_at 𝕜 (λ (y : E), f y + c) x
@[simp]
theorem differentiable_at_add_const_iff {𝕜 : 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} (c : F) :
differentiable_at 𝕜 (λ (y : E), f y + c) x differentiable_at 𝕜 f x
theorem differentiable_on.add_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] {f : E F} {s : set E} (hf : differentiable_on 𝕜 f s) (c : F) :
differentiable_on 𝕜 (λ (y : E), f y + c) s
@[simp]
theorem differentiable_on_add_const_iff {𝕜 : 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} (c : F) :
differentiable_on 𝕜 (λ (y : E), f y + c) s differentiable_on 𝕜 f s
theorem differentiable.add_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] {f : E F} (hf : differentiable 𝕜 f) (c : F) :
differentiable 𝕜 (λ (y : E), f y + c)
@[simp]
theorem differentiable_add_const_iff {𝕜 : 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} (c : F) :
differentiable 𝕜 (λ (y : E), f y + c) differentiable 𝕜 f
theorem fderiv_within_add_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] {f : E F} {x : E} {s : set E} (hxs : unique_diff_within_at 𝕜 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} [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} (c : F) :
fderiv 𝕜 (λ (y : E), f y + c) x = fderiv 𝕜 f x
theorem has_strict_fderiv_at.const_add {𝕜 : 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} (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} [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} {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} [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} (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} [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} (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} [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} (hf : differentiable_within_at 𝕜 f s x) (c : F) :
differentiable_within_at 𝕜 (λ (y : E), c + f y) s x
@[simp]
theorem differentiable_within_at_const_add_iff {𝕜 : 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} (c : F) :
differentiable_within_at 𝕜 (λ (y : E), c + f y) s x differentiable_within_at 𝕜 f s x
theorem differentiable_at.const_add {𝕜 : 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} (hf : differentiable_at 𝕜 f x) (c : F) :
differentiable_at 𝕜 (λ (y : E), c + f y) x
@[simp]
theorem differentiable_at_const_add_iff {𝕜 : 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} (c : F) :
differentiable_at 𝕜 (λ (y : E), c + f y) x differentiable_at 𝕜 f x
theorem differentiable_on.const_add {𝕜 : 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} (hf : differentiable_on 𝕜 f s) (c : F) :
differentiable_on 𝕜 (λ (y : E), c + f y) s
@[simp]
theorem differentiable_on_const_add_iff {𝕜 : 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} (c : F) :
differentiable_on 𝕜 (λ (y : E), c + f y) s differentiable_on 𝕜 f s
theorem differentiable.const_add {𝕜 : 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} (hf : differentiable 𝕜 f) (c : F) :
differentiable 𝕜 (λ (y : E), c + f y)
@[simp]
theorem differentiable_const_add_iff {𝕜 : 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} (c : F) :
differentiable 𝕜 (λ (y : E), c + f y) differentiable 𝕜 f
theorem fderiv_within_const_add {𝕜 : 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} (hxs : unique_diff_within_at 𝕜 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} [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} (c : F) :
fderiv 𝕜 (λ (y : E), c + f y) x = fderiv 𝕜 f x

Derivative of a finite sum of functions #

theorem has_strict_fderiv_at.sum {𝕜 : 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} {u : finset ι} {A : ι E F} {A' : ι (E →L[𝕜] F)} (h : (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} [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} {L : filter E} {ι : Type u_6} {u : finset ι} {A : ι E F} {A' : ι (E →L[𝕜] F)} (h : (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} [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} {u : finset ι} {A : ι E F} {A' : ι (E →L[𝕜] F)} (h : (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} [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} {u : finset ι} {A : ι E F} {A' : ι (E →L[𝕜] F)} (h : (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} [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} {u : finset ι} {A : ι E F} (h : (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} [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} {u : finset ι} {A : ι E F} (h : (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} [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} {u : finset ι} {A : ι E F} (h : (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} [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} {u : finset ι} {A : ι E F} (h : (i : ι), i u differentiable 𝕜 (A i)) :
differentiable 𝕜 (λ (y : E), u.sum (λ (i : ι), A i y))
theorem fderiv_within_sum {𝕜 : 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} {u : finset ι} {A : ι E F} (hxs : unique_diff_within_at 𝕜 s x) (h : (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} [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} {u : finset ι} {A : ι E F} (h : (i : ι), i u differentiable_at 𝕜 (A i) x) :
fderiv 𝕜 (λ (y : E), u.sum (λ (i : ι), A i y)) x = u.sum (λ (i : ι), fderiv 𝕜 (A i) x)

Derivative of the negative of a function #

theorem has_strict_fderiv_at.neg {𝕜 : 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} (h : 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} [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} {L : filter E} (h : 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} [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} (h : 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} [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} (h : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), -f x) (-f') x
theorem differentiable_within_at.neg {𝕜 : 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} (h : differentiable_within_at 𝕜 f s x) :
differentiable_within_at 𝕜 (λ (y : E), -f y) s x
@[simp]
theorem differentiable_within_at_neg_iff {𝕜 : 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} :
differentiable_within_at 𝕜 (λ (y : E), -f y) s x differentiable_within_at 𝕜 f s x
theorem differentiable_at.neg {𝕜 : 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} (h : differentiable_at 𝕜 f x) :
differentiable_at 𝕜 (λ (y : E), -f y) x
@[simp]
theorem differentiable_at_neg_iff {𝕜 : 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} :
differentiable_at 𝕜 (λ (y : E), -f y) x differentiable_at 𝕜 f x
theorem differentiable_on.neg {𝕜 : 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} (h : differentiable_on 𝕜 f s) :
differentiable_on 𝕜 (λ (y : E), -f y) s
@[simp]
theorem differentiable_on_neg_iff {𝕜 : 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} :
differentiable_on 𝕜 (λ (y : E), -f y) s differentiable_on 𝕜 f s
theorem differentiable.neg {𝕜 : 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} (h : differentiable 𝕜 f) :
differentiable 𝕜 (λ (y : E), -f y)
@[simp]
theorem differentiable_neg_iff {𝕜 : 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} :
differentiable 𝕜 (λ (y : E), -f y) differentiable 𝕜 f
theorem fderiv_within_neg {𝕜 : 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} (hxs : unique_diff_within_at 𝕜 s x) :
fderiv_within 𝕜 (λ (y : E), -f y) s x = -fderiv_within 𝕜 f s x
@[simp]
theorem fderiv_neg {𝕜 : 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} :
fderiv 𝕜 (λ (y : E), -f y) x = -fderiv 𝕜 f x

Derivative of the difference of two functions #

theorem has_strict_fderiv_at.sub {𝕜 : 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 g : E F} {f' g' : E →L[𝕜] F} {x : E} (hf : has_strict_fderiv_at f f' x) (hg : 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} [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 g : E F} {f' g' : E →L[𝕜] F} {x : E} {L : filter E} (hf : has_fderiv_at_filter f f' x L) (hg : 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} [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 g : E F} {f' g' : E →L[𝕜] F} {x : E} {s : set E} (hf : has_fderiv_within_at f f' s x) (hg : 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} [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 g : E F} {f' g' : E →L[𝕜] F} {x : E} (hf : has_fderiv_at f f' x) (hg : 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} [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 g : E F} {x : E} {s : set E} (hf : differentiable_within_at 𝕜 f s x) (hg : 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} [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 g : E F} {x : E} (hf : differentiable_at 𝕜 f x) (hg : differentiable_at 𝕜 g x) :
differentiable_at 𝕜 (λ (y : E), f y - g y) x
theorem differentiable_on.sub {𝕜 : 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 g : E F} {s : set E} (hf : differentiable_on 𝕜 f s) (hg : differentiable_on 𝕜 g s) :
differentiable_on 𝕜 (λ (y : E), f y - g y) s
@[simp]
theorem differentiable.sub {𝕜 : 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 g : E F} (hf : differentiable 𝕜 f) (hg : differentiable 𝕜 g) :
differentiable 𝕜 (λ (y : E), f y - g y)
theorem fderiv_within_sub {𝕜 : 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 g : E F} {x : E} {s : set E} (hxs : unique_diff_within_at 𝕜 s x) (hf : differentiable_within_at 𝕜 f s x) (hg : 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} [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 g : E F} {x : E} (hf : differentiable_at 𝕜 f x) (hg : 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} [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} (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} [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} {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} [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} (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} [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} (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} [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} (hf : differentiable_within_at 𝕜 f s x) (c : F) :
differentiable_within_at 𝕜 (λ (y : E), f y - c) s x
@[simp]
theorem differentiable_within_at_sub_const_iff {𝕜 : 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} (c : F) :
differentiable_within_at 𝕜 (λ (y : E), f y - c) s x differentiable_within_at 𝕜 f s x
theorem differentiable_at.sub_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] {f : E F} {x : E} (hf : differentiable_at 𝕜 f x) (c : F) :
differentiable_at 𝕜 (λ (y : E), f y - c) x
@[simp]
theorem differentiable_at_sub_const_iff {𝕜 : 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} (c : F) :
differentiable_at 𝕜 (λ (y : E), f y - c) x differentiable_at 𝕜 f x
theorem differentiable_on.sub_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] {f : E F} {s : set E} (hf : differentiable_on 𝕜 f s) (c : F) :
differentiable_on 𝕜 (λ (y : E), f y - c) s
@[simp]
theorem differentiable_on_sub_const_iff {𝕜 : 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} (c : F) :
differentiable_on 𝕜 (λ (y : E), f y - c) s differentiable_on 𝕜 f s
theorem differentiable.sub_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] {f : E F} (hf : differentiable 𝕜 f) (c : F) :
differentiable 𝕜 (λ (y : E), f y - c)
@[simp]
theorem differentiable_sub_const_iff {𝕜 : 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} (c : F) :
differentiable 𝕜 (λ (y : E), f y - c) differentiable 𝕜 f
theorem fderiv_within_sub_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] {f : E F} {x : E} {s : set E} (hxs : unique_diff_within_at 𝕜 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} [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} (c : F) :
fderiv 𝕜 (λ (y : E), f y - c) x = fderiv 𝕜 f x
theorem has_strict_fderiv_at.const_sub {𝕜 : 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} (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} [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} {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} [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} (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} [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} (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} [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} (hf : differentiable_within_at 𝕜 f s x) (c : F) :
differentiable_within_at 𝕜 (λ (y : E), c - f y) s x
@[simp]
theorem differentiable_within_at_const_sub_iff {𝕜 : 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} (c : F) :
differentiable_within_at 𝕜 (λ (y : E), c - f y) s x differentiable_within_at 𝕜 f s x
theorem differentiable_at.const_sub {𝕜 : 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} (hf : differentiable_at 𝕜 f x) (c : F) :
differentiable_at 𝕜 (λ (y : E), c - f y) x
@[simp]
theorem differentiable_at_const_sub_iff {𝕜 : 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} (c : F) :
differentiable_at 𝕜 (λ (y : E), c - f y) x differentiable_at 𝕜 f x
theorem differentiable_on.const_sub {𝕜 : 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} (hf : differentiable_on 𝕜 f s) (c : F) :
differentiable_on 𝕜 (λ (y : E), c - f y) s
@[simp]
theorem differentiable_on_const_sub_iff {𝕜 : 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} (c : F) :
differentiable_on 𝕜 (λ (y : E), c - f y) s differentiable_on 𝕜 f s
theorem differentiable.const_sub {𝕜 : 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} (hf : differentiable 𝕜 f) (c : F) :
differentiable 𝕜 (λ (y : E), c - f y)
@[simp]
theorem differentiable_const_sub_iff {𝕜 : 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} (c : F) :
differentiable 𝕜 (λ (y : E), c - f y) differentiable 𝕜 f
theorem fderiv_within_const_sub {𝕜 : 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} (hxs : unique_diff_within_at 𝕜 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} [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} (c : F) :
fderiv 𝕜 (λ (y : E), c - f y) x = -fderiv 𝕜 f x