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