One-dimensional derivatives of sums etc

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 HasDerivAtFilter.add {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {x : 𝕜} {L : Filter 𝕜} (hf : HasDerivAtFilter f f' x L) (hg : HasDerivAtFilter g g' x L) : HasDerivAtFilter (fun (y : 𝕜) => f y + g y) (f' + g') x L

theorem HasStrictDerivAt.add {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {x : 𝕜} (hf : HasStrictDerivAt f f' x) (hg : HasStrictDerivAt g g' x) : HasStrictDerivAt (fun (y : 𝕜) => f y + g y) (f' + g') x

theorem HasDerivWithinAt.add {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {x : 𝕜} {s : Set 𝕜} (hf : HasDerivWithinAt f f' s x) (hg : HasDerivWithinAt g g' s x) : HasDerivWithinAt (fun (y : 𝕜) => f y + g y) (f' + g') s x

theorem HasDerivAt.add {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {x : 𝕜} (hf : HasDerivAt f f' x) (hg : HasDerivAt g g' x) : HasDerivAt (fun (x : 𝕜) => f x + g x) (f' + g') x

theorem derivWithin_add {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} (hf : DifferentiableWithinAt 𝕜 f s x) (hg : DifferentiableWithinAt 𝕜 g s x) : derivWithin (fun (y : 𝕜) => f y + g y) s x = derivWithin f s x + derivWithin g s x

@[simp]

theorem deriv_add {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : 𝕜 → F} {x : 𝕜} (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) : deriv (fun (y : 𝕜) => f y + g y) x = deriv f x + deriv g x

@[simp]

theorem hasDerivAtFilter_add_const_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {L : Filter 𝕜} (c : F) : HasDerivAtFilter (fun (x : 𝕜) => f x + c) f' x L ↔ HasDerivAtFilter f f' x L

theorem HasDerivAtFilter.add_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {L : Filter 𝕜} (c : F) : HasDerivAtFilter f f' x L → HasDerivAtFilter (fun (x : 𝕜) => f x + c) f' x L

Alias of the reverse direction of hasDerivAtFilter_add_const_iff.

@[simp]

theorem hasStrictDerivAt_add_const_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (c : F) : HasStrictDerivAt (fun (x : 𝕜) => f x + c) f' x ↔ HasStrictDerivAt f f' x

theorem HasStrictDerivAt.add_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (c : F) : HasStrictDerivAt f f' x → HasStrictDerivAt (fun (x : 𝕜) => f x + c) f' x

Alias of the reverse direction of hasStrictDerivAt_add_const_iff.

@[simp]

theorem hasDerivWithinAt_add_const_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜} (c : F) : HasDerivWithinAt (fun (x : 𝕜) => f x + c) f' s x ↔ HasDerivWithinAt f f' s x

theorem HasDerivWithinAt.add_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜} (c : F) : HasDerivWithinAt f f' s x → HasDerivWithinAt (fun (x : 𝕜) => f x + c) f' s x

Alias of the reverse direction of hasDerivWithinAt_add_const_iff.

@[simp]

theorem hasDerivAt_add_const_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (c : F) : HasDerivAt (fun (x : 𝕜) => f x + c) f' x ↔ HasDerivAt f f' x

theorem HasDerivAt.add_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (c : F) : HasDerivAt f f' x → HasDerivAt (fun (x : 𝕜) => f x + c) f' x

Alias of the reverse direction of hasDerivAt_add_const_iff.

theorem derivWithin_add_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} (c : F) : derivWithin (fun (y : 𝕜) => f y + c) s x = derivWithin f s x

theorem deriv_add_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} (c : F) : deriv (fun (y : 𝕜) => f y + c) x = deriv f x

@[simp]

theorem deriv_add_const' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} (c : F) : (deriv fun (y : 𝕜) => f y + c) = deriv f

theorem hasDerivAtFilter_const_add_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {L : Filter 𝕜} (c : F) : HasDerivAtFilter (fun (x : 𝕜) => c + f x) f' x L ↔ HasDerivAtFilter f f' x L

theorem HasDerivAtFilter.const_add {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {L : Filter 𝕜} (c : F) : HasDerivAtFilter f f' x L → HasDerivAtFilter (fun (x : 𝕜) => c + f x) f' x L

Alias of the reverse direction of hasDerivAtFilter_const_add_iff.

@[simp]

theorem hasStrictDerivAt_const_add_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (c : F) : HasStrictDerivAt (fun (x : 𝕜) => c + f x) f' x ↔ HasStrictDerivAt f f' x

theorem HasStrictDerivAt.const_add {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (c : F) : HasStrictDerivAt f f' x → HasStrictDerivAt (fun (x : 𝕜) => c + f x) f' x

Alias of the reverse direction of hasStrictDerivAt_const_add_iff.

@[simp]

theorem hasDerivWithinAt_const_add_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜} (c : F) : HasDerivWithinAt (fun (x : 𝕜) => c + f x) f' s x ↔ HasDerivWithinAt f f' s x

theorem HasDerivWithinAt.const_add {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜} (c : F) : HasDerivWithinAt f f' s x → HasDerivWithinAt (fun (x : 𝕜) => c + f x) f' s x

Alias of the reverse direction of hasDerivWithinAt_const_add_iff.

@[simp]

theorem hasDerivAt_const_add_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (c : F) : HasDerivAt (fun (x : 𝕜) => c + f x) f' x ↔ HasDerivAt f f' x

theorem HasDerivAt.const_add {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (c : F) : HasDerivAt f f' x → HasDerivAt (fun (x : 𝕜) => c + f x) f' x

Alias of the reverse direction of hasDerivAt_const_add_iff.

theorem derivWithin_const_add {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} (c : F) : derivWithin (fun (x : 𝕜) => c + f x) s x = derivWithin f s x

@[simp]

theorem derivWithin_const_add_fun {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} (c : F) : (derivWithin fun (x : 𝕜) => c + f x) = derivWithin f

theorem deriv_const_add {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} (c : F) : deriv (fun (x : 𝕜) => c + f x) x = deriv f x

@[simp]

theorem deriv_const_add' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} (c : F) : (deriv fun (x : 𝕜) => c + f x) = deriv f

theorem differentiableAt_comp_const_add {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {a b : 𝕜} : DifferentiableAt 𝕜 (fun (x : 𝕜) => f (b + x)) a ↔ DifferentiableAt 𝕜 f (b + a)

theorem differentiableAt_comp_add_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {a b : 𝕜} : DifferentiableAt 𝕜 (fun (x : 𝕜) => f (x + b)) a ↔ DifferentiableAt 𝕜 f (a + b)

theorem differentiableAt_iff_comp_const_add {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {a b : 𝕜} : DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun (x : 𝕜) => f (b + x)) (-b + a)

theorem differentiableAt_iff_comp_add_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {a b : 𝕜} : DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun (x : 𝕜) => f (x + b)) (a - b)

Derivative of a finite sum of functions

theorem HasDerivAtFilter.sum {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {L : Filter 𝕜} {ι : Type u_1} {u : Finset ι} {A : ι → 𝕜 → F} {A' : ι → F} (h : ∀ i ∈ u, HasDerivAtFilter (A i) (A' i) x L) : HasDerivAtFilter (fun (y : 𝕜) => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x L

theorem HasStrictDerivAt.sum {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {ι : Type u_1} {u : Finset ι} {A : ι → 𝕜 → F} {A' : ι → F} (h : ∀ i ∈ u, HasStrictDerivAt (A i) (A' i) x) : HasStrictDerivAt (fun (y : 𝕜) => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x

theorem HasDerivWithinAt.sum {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} {ι : Type u_1} {u : Finset ι} {A : ι → 𝕜 → F} {A' : ι → F} (h : ∀ i ∈ u, HasDerivWithinAt (A i) (A' i) s x) : HasDerivWithinAt (fun (y : 𝕜) => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) s x

theorem HasDerivAt.sum {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {ι : Type u_1} {u : Finset ι} {A : ι → 𝕜 → F} {A' : ι → F} (h : ∀ i ∈ u, HasDerivAt (A i) (A' i) x) : HasDerivAt (fun (y : 𝕜) => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x

theorem derivWithin_sum {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} {ι : Type u_1} {u : Finset ι} {A : ι → 𝕜 → F} (h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x) : derivWithin (fun (y : 𝕜) => ∑ i ∈ u, A i y) s x = ∑ i ∈ u, derivWithin (A i) s x

@[simp]

theorem deriv_sum {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {ι : Type u_1} {u : Finset ι} {A : ι → 𝕜 → F} (h : ∀ i ∈ u, DifferentiableAt 𝕜 (A i) x) : deriv (fun (y : 𝕜) => ∑ i ∈ u, A i y) x = ∑ i ∈ u, deriv (A i) x

Derivative of the negative of a function

theorem HasDerivAtFilter.neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {L : Filter 𝕜} (h : HasDerivAtFilter f f' x L) : HasDerivAtFilter (fun (x : 𝕜) => -f x) (-f') x L

theorem HasDerivWithinAt.neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜} (h : HasDerivWithinAt f f' s x) : HasDerivWithinAt (fun (x : 𝕜) => -f x) (-f') s x

theorem HasDerivAt.neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (h : HasDerivAt f f' x) : HasDerivAt (fun (x : 𝕜) => -f x) (-f') x

theorem HasStrictDerivAt.neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (h : HasStrictDerivAt f f' x) : HasStrictDerivAt (fun (x : 𝕜) => -f x) (-f') x

theorem derivWithin.neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} : derivWithin (fun (y : 𝕜) => -f y) s x = -derivWithin f s x

theorem deriv.neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} : deriv (fun (y : 𝕜) => -f y) x = -deriv f x

@[simp]

theorem deriv.neg' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} : (deriv fun (y : 𝕜) => -f y) = fun (x : 𝕜) => -deriv f x

Derivative of the negation function (i.e Neg.neg)

theorem hasDerivAtFilter_neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) (L : Filter 𝕜) : HasDerivAtFilter Neg.neg (-1) x L

theorem hasDerivWithinAt_neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) (s : Set 𝕜) : HasDerivWithinAt Neg.neg (-1) s x

theorem hasDerivAt_neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) : HasDerivAt Neg.neg (-1) x

theorem hasDerivAt_neg' {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) : HasDerivAt (fun (x : 𝕜) => -x) (-1) x

theorem hasStrictDerivAt_neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) : HasStrictDerivAt Neg.neg (-1) x

theorem deriv_neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) : deriv Neg.neg x = -1

@[simp]

theorem deriv_neg' {𝕜 : Type u} [NontriviallyNormedField 𝕜] : deriv Neg.neg = fun (x : 𝕜) => -1

@[simp]

theorem deriv_neg'' {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) : deriv (fun (x : 𝕜) => -x) x = -1

theorem derivWithin_neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) (s : Set 𝕜) (hxs : UniqueDiffWithinAt 𝕜 s x) : derivWithin Neg.neg s x = -1

theorem differentiable_neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] : Differentiable 𝕜 Neg.neg

theorem differentiableOn_neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] (s : Set 𝕜) : DifferentiableOn 𝕜 Neg.neg s

theorem differentiableAt_comp_neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {a : 𝕜} : DifferentiableAt 𝕜 (fun (x : 𝕜) => f (-x)) a ↔ DifferentiableAt 𝕜 f (-a)

theorem differentiableAt_iff_comp_neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {a : 𝕜} : DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun (x : 𝕜) => f (-x)) (-a)

Derivative of the difference of two functions

theorem HasDerivAtFilter.sub {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {x : 𝕜} {L : Filter 𝕜} (hf : HasDerivAtFilter f f' x L) (hg : HasDerivAtFilter g g' x L) : HasDerivAtFilter (fun (x : 𝕜) => f x - g x) (f' - g') x L

theorem HasDerivWithinAt.sub {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {x : 𝕜} {s : Set 𝕜} (hf : HasDerivWithinAt f f' s x) (hg : HasDerivWithinAt g g' s x) : HasDerivWithinAt (fun (x : 𝕜) => f x - g x) (f' - g') s x

theorem HasDerivAt.sub {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {x : 𝕜} (hf : HasDerivAt f f' x) (hg : HasDerivAt g g' x) : HasDerivAt (fun (x : 𝕜) => f x - g x) (f' - g') x

theorem HasStrictDerivAt.sub {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {x : 𝕜} (hf : HasStrictDerivAt f f' x) (hg : HasStrictDerivAt g g' x) : HasStrictDerivAt (fun (x : 𝕜) => f x - g x) (f' - g') x

theorem derivWithin_sub {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} (hf : DifferentiableWithinAt 𝕜 f s x) (hg : DifferentiableWithinAt 𝕜 g s x) : derivWithin (fun (y : 𝕜) => f y - g y) s x = derivWithin f s x - derivWithin g s x

@[simp]

theorem deriv_sub {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : 𝕜 → F} {x : 𝕜} (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) : deriv (fun (y : 𝕜) => f y - g y) x = deriv f x - deriv g x

@[simp]

theorem hasDerivAtFilter_sub_const_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {L : Filter 𝕜} (c : F) : HasDerivAtFilter (fun (x : 𝕜) => f x - c) f' x L ↔ HasDerivAtFilter f f' x L

theorem HasDerivAtFilter.sub_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {L : Filter 𝕜} (c : F) : HasDerivAtFilter f f' x L → HasDerivAtFilter (fun (x : 𝕜) => f x - c) f' x L

Alias of the reverse direction of hasDerivAtFilter_sub_const_iff.

@[simp]

theorem hasDerivWithinAt_sub_const_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜} (c : F) : HasDerivWithinAt (fun (x : 𝕜) => f x - c) f' s x ↔ HasDerivWithinAt f f' s x

theorem HasDerivWithinAt.sub_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜} (c : F) : HasDerivWithinAt f f' s x → HasDerivWithinAt (fun (x : 𝕜) => f x - c) f' s x

Alias of the reverse direction of hasDerivWithinAt_sub_const_iff.

@[simp]

theorem hasDerivAt_sub_const_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (c : F) : HasDerivAt (fun (x : 𝕜) => f x - c) f' x ↔ HasDerivAt f f' x

theorem HasDerivAt.sub_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (c : F) : HasDerivAt f f' x → HasDerivAt (fun (x : 𝕜) => f x - c) f' x

Alias of the reverse direction of hasDerivAt_sub_const_iff.

theorem derivWithin_sub_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} (c : F) : derivWithin (fun (y : 𝕜) => f y - c) s x = derivWithin f s x

@[simp]

theorem derivWithin_sub_const_fun {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} (c : F) : (derivWithin fun (x : 𝕜) => f x - c) = derivWithin f

theorem deriv_sub_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} (c : F) : deriv (fun (y : 𝕜) => f y - c) x = deriv f x

@[simp]

theorem deriv_sub_const_fun {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} (c : F) : (deriv fun (x : 𝕜) => f x - c) = deriv f

theorem HasDerivAtFilter.const_sub {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {L : Filter 𝕜} (c : F) (hf : HasDerivAtFilter f f' x L) : HasDerivAtFilter (fun (x : 𝕜) => c - f x) (-f') x L

theorem HasDerivWithinAt.const_sub {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜} (c : F) (hf : HasDerivWithinAt f f' s x) : HasDerivWithinAt (fun (x : 𝕜) => c - f x) (-f') s x

theorem HasStrictDerivAt.const_sub {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (c : F) (hf : HasStrictDerivAt f f' x) : HasStrictDerivAt (fun (x : 𝕜) => c - f x) (-f') x

theorem HasDerivAt.const_sub {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (c : F) (hf : HasDerivAt f f' x) : HasDerivAt (fun (x : 𝕜) => c - f x) (-f') x

theorem derivWithin_const_sub {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} (c : F) : derivWithin (fun (y : 𝕜) => c - f y) s x = -derivWithin f s x

theorem deriv_const_sub {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} (c : F) : deriv (fun (y : 𝕜) => c - f y) x = -deriv f x

theorem differentiableAt_comp_sub_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {a b : 𝕜} : DifferentiableAt 𝕜 (fun (x : 𝕜) => f (x - b)) a ↔ DifferentiableAt 𝕜 f (a - b)

theorem differentiableAt_comp_const_sub {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {a b : 𝕜} : DifferentiableAt 𝕜 (fun (x : 𝕜) => f (b - x)) a ↔ DifferentiableAt 𝕜 f (b - a)

theorem differentiableAt_iff_comp_sub_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {a b : 𝕜} : DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun (x : 𝕜) => f (x - b)) (a + b)

theorem differentiableAt_iff_comp_const_sub {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {a b : 𝕜} : DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun (x : 𝕜) => f (b - x)) (b - a)