# One-dimensional derivatives of sums etc #

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

In this file we prove formulas about derivatives of f + g, -f, f - g, and ∑ i, f i x for functions from the base field to a normed space over this field.

For a more detailed overview of one-dimensional derivatives in mathlib, see the module docstring of analysis/calculus/deriv/basic.

## Keywords #

derivative

### Derivative of the sum of two functions #

theorem has_deriv_at_filter.add {𝕜 : Type u} {F : Type v} [ F] {f g : 𝕜 F} {f' g' : F} {x : 𝕜} {L : filter 𝕜} (hf : x L) (hg : x L) :
has_deriv_at_filter (λ (y : 𝕜), f y + g y) (f' + g') x L
theorem has_strict_deriv_at.add {𝕜 : Type u} {F : Type v} [ F] {f g : 𝕜 F} {f' g' : F} {x : 𝕜} (hf : x) (hg : x) :
has_strict_deriv_at (λ (y : 𝕜), f y + g y) (f' + g') x
theorem has_deriv_within_at.add {𝕜 : Type u} {F : Type v} [ F] {f g : 𝕜 F} {f' g' : F} {x : 𝕜} {s : set 𝕜} (hf : s x) (hg : s x) :
has_deriv_within_at (λ (y : 𝕜), f y + g y) (f' + g') s x
theorem has_deriv_at.add {𝕜 : Type u} {F : Type v} [ F] {f g : 𝕜 F} {f' g' : F} {x : 𝕜} (hf : f' x) (hg : g' x) :
has_deriv_at (λ (x : 𝕜), f x + g x) (f' + g') x
theorem deriv_within_add {𝕜 : Type u} {F : Type v} [ F] {f g : 𝕜 F} {x : 𝕜} {s : set 𝕜} (hxs : x) (hf : x) (hg : x) :
deriv_within (λ (y : 𝕜), f y + g y) s x = s x + s x
@[simp]
theorem deriv_add {𝕜 : Type u} {F : Type v} [ F] {f g : 𝕜 F} {x : 𝕜} (hf : x) (hg : x) :
deriv (λ (y : 𝕜), f y + g y) x = x + x
theorem has_deriv_at_filter.add_const {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} {L : filter 𝕜} (hf : x L) (c : F) :
has_deriv_at_filter (λ (y : 𝕜), f y + c) f' x L
theorem has_deriv_within_at.add_const {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} {s : set 𝕜} (hf : s x) (c : F) :
has_deriv_within_at (λ (y : 𝕜), f y + c) f' s x
theorem has_deriv_at.add_const {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} (hf : f' x) (c : F) :
has_deriv_at (λ (x : 𝕜), f x + c) f' x
theorem deriv_within_add_const {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {x : 𝕜} {s : set 𝕜} (hxs : x) (c : F) :
deriv_within (λ (y : 𝕜), f y + c) s x = s x
theorem deriv_add_const {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {x : 𝕜} (c : F) :
deriv (λ (y : 𝕜), f y + c) x = x
@[simp]
theorem deriv_add_const' {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} (c : F) :
deriv (λ (y : 𝕜), f y + c) =
theorem has_deriv_at_filter.const_add {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} {L : filter 𝕜} (c : F) (hf : x L) :
has_deriv_at_filter (λ (y : 𝕜), c + f y) f' x L
theorem has_deriv_within_at.const_add {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} {s : set 𝕜} (c : F) (hf : s x) :
has_deriv_within_at (λ (y : 𝕜), c + f y) f' s x
theorem has_deriv_at.const_add {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} (c : F) (hf : f' x) :
has_deriv_at (λ (x : 𝕜), c + f x) f' x
theorem deriv_within_const_add {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {x : 𝕜} {s : set 𝕜} (hxs : x) (c : F) :
deriv_within (λ (y : 𝕜), c + f y) s x = s x
theorem deriv_const_add {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {x : 𝕜} (c : F) :
deriv (λ (y : 𝕜), c + f y) x = x
@[simp]
theorem deriv_const_add' {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} (c : F) :
deriv (λ (y : 𝕜), c + f y) =

### Derivative of a finite sum of functions #

theorem has_deriv_at_filter.sum {𝕜 : Type u} {F : Type v} [ F] {x : 𝕜} {L : filter 𝕜} {ι : Type u_1} {u : finset ι} {A : ι 𝕜 F} {A' : ι F} (h : (i : ι), i u has_deriv_at_filter (A i) (A' i) x L) :
has_deriv_at_filter (λ (y : 𝕜), u.sum (λ (i : ι), A i y)) (u.sum (λ (i : ι), A' i)) x L
theorem has_strict_deriv_at.sum {𝕜 : Type u} {F : Type v} [ F] {x : 𝕜} {ι : Type u_1} {u : finset ι} {A : ι 𝕜 F} {A' : ι F} (h : (i : ι), i u has_strict_deriv_at (A i) (A' i) x) :
has_strict_deriv_at (λ (y : 𝕜), u.sum (λ (i : ι), A i y)) (u.sum (λ (i : ι), A' i)) x
theorem has_deriv_within_at.sum {𝕜 : Type u} {F : Type v} [ F] {x : 𝕜} {s : set 𝕜} {ι : Type u_1} {u : finset ι} {A : ι 𝕜 F} {A' : ι F} (h : (i : ι), i u has_deriv_within_at (A i) (A' i) s x) :
has_deriv_within_at (λ (y : 𝕜), u.sum (λ (i : ι), A i y)) (u.sum (λ (i : ι), A' i)) s x
theorem has_deriv_at.sum {𝕜 : Type u} {F : Type v} [ F] {x : 𝕜} {ι : Type u_1} {u : finset ι} {A : ι 𝕜 F} {A' : ι F} (h : (i : ι), i u has_deriv_at (A i) (A' i) x) :
has_deriv_at (λ (y : 𝕜), u.sum (λ (i : ι), A i y)) (u.sum (λ (i : ι), A' i)) x
theorem deriv_within_sum {𝕜 : Type u} {F : Type v} [ F] {x : 𝕜} {s : set 𝕜} {ι : Type u_1} {u : finset ι} {A : ι 𝕜 F} (hxs : x) (h : (i : ι), i u (A i) s x) :
deriv_within (λ (y : 𝕜), u.sum (λ (i : ι), A i y)) s x = u.sum (λ (i : ι), deriv_within (A i) s x)
@[simp]
theorem deriv_sum {𝕜 : Type u} {F : Type v} [ F] {x : 𝕜} {ι : Type u_1} {u : finset ι} {A : ι 𝕜 F} (h : (i : ι), i u (A i) x) :
deriv (λ (y : 𝕜), u.sum (λ (i : ι), A i y)) x = u.sum (λ (i : ι), deriv (A i) x)

### Derivative of the negative of a function #

theorem has_deriv_at_filter.neg {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} {L : filter 𝕜} (h : x L) :
has_deriv_at_filter (λ (x : 𝕜), -f x) (-f') x L
theorem has_deriv_within_at.neg {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} {s : set 𝕜} (h : s x) :
has_deriv_within_at (λ (x : 𝕜), -f x) (-f') s x
theorem has_deriv_at.neg {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} (h : f' x) :
has_deriv_at (λ (x : 𝕜), -f x) (-f') x
theorem has_strict_deriv_at.neg {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} (h : x) :
has_strict_deriv_at (λ (x : 𝕜), -f x) (-f') x
theorem deriv_within.neg {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {x : 𝕜} {s : set 𝕜} (hxs : x) :
deriv_within (λ (y : 𝕜), -f y) s x = - s x
theorem deriv.neg {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {x : 𝕜} :
deriv (λ (y : 𝕜), -f y) x = - x
@[simp]
theorem deriv.neg' {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} :
deriv (λ (y : 𝕜), -f y) = λ (x : 𝕜), - x

### Derivative of the negation function (i.e has_neg.neg) #

theorem has_deriv_at_filter_neg {𝕜 : Type u} (x : 𝕜) (L : filter 𝕜) :
L
theorem has_deriv_within_at_neg {𝕜 : Type u} (x : 𝕜) (s : set 𝕜) :
x
theorem has_deriv_at_neg {𝕜 : Type u} (x : 𝕜) :
x
theorem has_deriv_at_neg' {𝕜 : Type u} (x : 𝕜) :
has_deriv_at (λ (x : 𝕜), -x) (-1) x
theorem has_strict_deriv_at_neg {𝕜 : Type u} (x : 𝕜) :
theorem deriv_neg {𝕜 : Type u} (x : 𝕜) :
= -1
@[simp]
theorem deriv_neg' {𝕜 : Type u}  :
= λ (_x : 𝕜), -1
@[simp]
theorem deriv_neg'' {𝕜 : Type u} (x : 𝕜) :
deriv (λ (x : 𝕜), -x) x = -1
theorem deriv_within_neg {𝕜 : Type u} (x : 𝕜) (s : set 𝕜) (hxs : x) :
= -1
theorem differentiable_neg {𝕜 : Type u}  :
theorem differentiable_on_neg {𝕜 : Type u} (s : set 𝕜) :

### Derivative of the difference of two functions #

theorem has_deriv_at_filter.sub {𝕜 : Type u} {F : Type v} [ F] {f g : 𝕜 F} {f' g' : F} {x : 𝕜} {L : filter 𝕜} (hf : x L) (hg : x L) :
has_deriv_at_filter (λ (x : 𝕜), f x - g x) (f' - g') x L
theorem has_deriv_within_at.sub {𝕜 : Type u} {F : Type v} [ F] {f g : 𝕜 F} {f' g' : F} {x : 𝕜} {s : set 𝕜} (hf : s x) (hg : s x) :
has_deriv_within_at (λ (x : 𝕜), f x - g x) (f' - g') s x
theorem has_deriv_at.sub {𝕜 : Type u} {F : Type v} [ F] {f g : 𝕜 F} {f' g' : F} {x : 𝕜} (hf : f' x) (hg : g' x) :
has_deriv_at (λ (x : 𝕜), f x - g x) (f' - g') x
theorem has_strict_deriv_at.sub {𝕜 : Type u} {F : Type v} [ F] {f g : 𝕜 F} {f' g' : F} {x : 𝕜} (hf : x) (hg : x) :
has_strict_deriv_at (λ (x : 𝕜), f x - g x) (f' - g') x
theorem deriv_within_sub {𝕜 : Type u} {F : Type v} [ F] {f g : 𝕜 F} {x : 𝕜} {s : set 𝕜} (hxs : x) (hf : x) (hg : x) :
deriv_within (λ (y : 𝕜), f y - g y) s x = s x - s x
@[simp]
theorem deriv_sub {𝕜 : Type u} {F : Type v} [ F] {f g : 𝕜 F} {x : 𝕜} (hf : x) (hg : x) :
deriv (λ (y : 𝕜), f y - g y) x = x - x
theorem has_deriv_at_filter.sub_const {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} {L : filter 𝕜} (hf : x L) (c : F) :
has_deriv_at_filter (λ (x : 𝕜), f x - c) f' x L
theorem has_deriv_within_at.sub_const {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} {s : set 𝕜} (hf : s x) (c : F) :
has_deriv_within_at (λ (x : 𝕜), f x - c) f' s x
theorem has_deriv_at.sub_const {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} (hf : f' x) (c : F) :
has_deriv_at (λ (x : 𝕜), f x - c) f' x
theorem deriv_within_sub_const {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {x : 𝕜} {s : set 𝕜} (hxs : x) (c : F) :
deriv_within (λ (y : 𝕜), f y - c) s x = s x
theorem deriv_sub_const {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {x : 𝕜} (c : F) :
deriv (λ (y : 𝕜), f y - c) x = x
theorem has_deriv_at_filter.const_sub {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} {L : filter 𝕜} (c : F) (hf : x L) :
has_deriv_at_filter (λ (x : 𝕜), c - f x) (-f') x L
theorem has_deriv_within_at.const_sub {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} {s : set 𝕜} (c : F) (hf : s x) :
has_deriv_within_at (λ (x : 𝕜), c - f x) (-f') s x
theorem has_strict_deriv_at.const_sub {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} (c : F) (hf : x) :
has_strict_deriv_at (λ (x : 𝕜), c - f x) (-f') x
theorem has_deriv_at.const_sub {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} (c : F) (hf : f' x) :
has_deriv_at (λ (x : 𝕜), c - f x) (-f') x
theorem deriv_within_const_sub {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {x : 𝕜} {s : set 𝕜} (hxs : x) (c : F) :
deriv_within (λ (y : 𝕜), c - f y) s x = - s x
theorem deriv_const_sub {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {x : 𝕜} (c : F) :
deriv (λ (y : 𝕜), c - f y) x = - x