# 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

• sum of finitely many functions
• multiplication of a function by a scalar constant
• negative of a function
• subtraction of two functions

### Derivative of a function multiplied by a constant #

theorem has_strict_fderiv_at.const_smul {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {f' : E →L[𝕜] F} {x : E} {R : Type u_6} [semiring R] [ F] [ F] (h : 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} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {f' : E →L[𝕜] F} {x : E} {L : filter E} {R : Type u_6} [semiring R] [ F] [ F] (h : 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} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {f' : E →L[𝕜] F} {x : E} {s : set E} {R : Type u_6} [semiring R] [ F] [ F] (h : 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} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {f' : E →L[𝕜] F} {x : E} {R : Type u_6} [semiring R] [ F] [ F] (h : f' x) (c : R) :
has_fderiv_at (λ (x : E), c f x) (c f') x
theorem differentiable_within_at.const_smul {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s : set E} {R : Type u_6} [semiring R] [ F] [ F] (h : x) (c : R) :
(λ (y : E), c f y) s x
theorem differentiable_at.const_smul {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {R : Type u_6} [semiring R] [ F] [ F] (h : x) (c : R) :
(λ (y : E), c f y) x
theorem differentiable_on.const_smul {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {s : set E} {R : Type u_6} [semiring R] [ F] [ F] (h : s) (c : R) :
(λ (y : E), c f y) s
theorem differentiable.const_smul {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {R : Type u_6} [semiring R] [ F] [ F] (h : f) (c : R) :
(λ (y : E), c f y)
theorem fderiv_within_const_smul {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s : set E} {R : Type u_6} [semiring R] [ F] [ F] (hxs : x) (h : x) (c : R) :
(λ (y : E), c f y) s x = c s x
theorem fderiv_const_smul {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {R : Type u_6} [semiring R] [ F] [ F] (h : x) (c : R) :
(λ (y : E), c f y) x = c f x

### Derivative of the sum of two functions #

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

### Derivative of a finite sum of functions #

theorem has_strict_fderiv_at.sum {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ 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} {E : Type u_2} [ E] {F : Type u_3} [ 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} {E : Type u_2} [ E] {F : Type u_3} [ 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} {E : Type u_2} [ E] {F : Type u_3} [ 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} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} {s : set E} {ι : Type u_6} {u : finset ι} {A : ι E F} (h : (i : ι), i u (A i) s x) :
(λ (y : E), u.sum (λ (i : ι), A i y)) s x
@[simp]
theorem differentiable_at.sum {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} {ι : Type u_6} {u : finset ι} {A : ι E F} (h : (i : ι), i u (A i) x) :
(λ (y : E), u.sum (λ (i : ι), A i y)) x
theorem differentiable_on.sum {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {s : set E} {ι : Type u_6} {u : finset ι} {A : ι E F} (h : (i : ι), i u (A i) s) :
(λ (y : E), u.sum (λ (i : ι), A i y)) s
@[simp]
theorem differentiable.sum {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {ι : Type u_6} {u : finset ι} {A : ι E F} (h : (i : ι), i u (A i)) :
(λ (y : E), u.sum (λ (i : ι), A i y))
theorem fderiv_within_sum {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} {s : set E} {ι : Type u_6} {u : finset ι} {A : ι E F} (hxs : x) (h : (i : ι), i u (A i) s x) :
(λ (y : E), u.sum (λ (i : ι), A i y)) s x = u.sum (λ (i : ι), (A i) s x)
theorem fderiv_sum {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} {ι : Type u_6} {u : finset ι} {A : ι E F} (h : (i : ι), i u (A i) x) :
(λ (y : E), u.sum (λ (i : ι), A i y)) x = u.sum (λ (i : ι), (A i) x)

### Derivative of the negative of a function #

theorem has_strict_fderiv_at.neg {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {f' : E →L[𝕜] F} {x : E} (h : x) :
has_strict_fderiv_at (λ (x : E), -f x) (-f') x
theorem has_fderiv_at_filter.neg {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {f' : E →L[𝕜] F} {x : E} {L : filter E} (h : x L) :
has_fderiv_at_filter (λ (x : E), -f x) (-f') x L
theorem has_fderiv_within_at.neg {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {f' : E →L[𝕜] F} {x : E} {s : set E} (h : s x) :
has_fderiv_within_at (λ (x : E), -f x) (-f') s x
theorem has_fderiv_at.neg {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {f' : E →L[𝕜] F} {x : E} (h : f' x) :
has_fderiv_at (λ (x : E), -f x) (-f') x
theorem differentiable_within_at.neg {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s : set E} (h : x) :
(λ (y : E), -f y) s x
@[simp]
theorem differentiable_within_at_neg_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s : set E} :
(λ (y : E), -f y) s x x
theorem differentiable_at.neg {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} (h : x) :
(λ (y : E), -f y) x
@[simp]
theorem differentiable_at_neg_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} :
(λ (y : E), -f y) x x
theorem differentiable_on.neg {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {s : set E} (h : s) :
(λ (y : E), -f y) s
@[simp]
theorem differentiable_on_neg_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {s : set E} :
(λ (y : E), -f y) s s
theorem differentiable.neg {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} (h : f) :
(λ (y : E), -f y)
@[simp]
theorem differentiable_neg_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} :
(λ (y : E), -f y)
theorem fderiv_within_neg {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s : set E} (hxs : x) :
(λ (y : E), -f y) s x = - s x
@[simp]
theorem fderiv_neg {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} :
(λ (y : E), -f y) x = - f x

### Derivative of the difference of two functions #

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