Mathlib.Analysis.Calculus.FDeriv.Add

HasStrictFDerivAt.const_smul theorem

(h : HasStrictFDerivAt f f' x) (c : R) : HasStrictFDerivAt (fun x => c • f x) (c • f') x

Full source

@[fun_prop]
theorem HasStrictFDerivAt.const_smul (h : HasStrictFDerivAt f f' x) (c : R) :
    HasStrictFDerivAt (fun x => c • f x) (c • f') x :=
  (c • (1 : F →L[𝕜] F)).hasStrictFDerivAt.comp x h

Strict Fréchet derivative of scalar multiplication: $(c \cdot f)'(x) = c \cdot f'(x)$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function that has strict Fréchet derivative $f'$ at $x \in E$. Then for any scalar $c \in R$, the function $x \mapsto c \cdot f(x)$ has strict Fréchet derivative $c \cdot f'$ at $x$.

HasFDerivAtFilter.const_smul theorem

(h : HasFDerivAtFilter f f' x L) (c : R) : HasFDerivAtFilter (fun x => c • f x) (c • f') x L

Full source

theorem HasFDerivAtFilter.const_smul (h : HasFDerivAtFilter f f' x L) (c : R) :
    HasFDerivAtFilter (fun x => c • f x) (c • f') x L :=
  (c • (1 : F →L[𝕜] F)).hasFDerivAtFilter.comp x h tendsto_map

Scalar Multiplication Preserves Fréchet Differentiability Along a Filter

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function that has Fréchet derivative $f'$ at $x \in E$ along the filter $L$ on $E$. Then for any scalar $c \in R$, the function $x \mapsto c \cdot f(x)$ has Fréchet derivative $c \cdot f'$ at $x$ along the filter $L$.

HasFDerivWithinAt.const_smul theorem

(h : HasFDerivWithinAt f f' s x) (c : R) : HasFDerivWithinAt (fun x => c • f x) (c • f') s x

Full source

@[fun_prop]
nonrec theorem HasFDerivWithinAt.const_smul (h : HasFDerivWithinAt f f' s x) (c : R) :
    HasFDerivWithinAt (fun x => c • f x) (c • f') s x :=
  h.const_smul c

Scalar Multiplication Preserves Fréchet Differentiability Within a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function that has Fréchet derivative $f'$ at $x \in E$ within a set $s \subseteq E$. Then for any scalar $c \in R$, the function $x \mapsto c \cdot f(x)$ has Fréchet derivative $c \cdot f'$ at $x$ within $s$.

HasFDerivAt.const_smul theorem

(h : HasFDerivAt f f' x) (c : R) : HasFDerivAt (fun x => c • f x) (c • f') x

Full source

@[fun_prop]
nonrec theorem HasFDerivAt.const_smul (h : HasFDerivAt f f' x) (c : R) :
    HasFDerivAt (fun x => c • f x) (c • f') x :=
  h.const_smul c

Scalar Multiplication Preserves Fréchet Differentiability at a Point

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function that has Fréchet derivative $f'$ at $x \in E$. Then for any scalar $c \in R$, the function $x \mapsto c \cdot f(x)$ has Fréchet derivative $c \cdot f'$ at $x$.

DifferentiableWithinAt.const_smul theorem

(h : DifferentiableWithinAt 𝕜 f s x) (c : R) : DifferentiableWithinAt 𝕜 (fun y => c • f y) s x

Full source

@[fun_prop]
theorem DifferentiableWithinAt.const_smul (h : DifferentiableWithinAt 𝕜 f s x) (c : R) :
    DifferentiableWithinAt 𝕜 (fun y => c • f y) s x :=
  (h.hasFDerivWithinAt.const_smul c).differentiableWithinAt

Differentiability of Scalar Multiple Within a Set

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, and let $f : E \to F$ be a function differentiable at a point $x \in E$ within a subset $s \subseteq E$. Then for any scalar $c \in R$, the function $y \mapsto c \cdot f(y)$ is differentiable at $x$ within $s$.

DifferentiableAt.const_smul theorem

(h : DifferentiableAt 𝕜 f x) (c : R) : DifferentiableAt 𝕜 (fun y => c • f y) x

Full source

@[fun_prop]
theorem DifferentiableAt.const_smul (h : DifferentiableAt 𝕜 f x) (c : R) :
    DifferentiableAt 𝕜 (fun y => c • f y) x :=
  (h.hasFDerivAt.const_smul c).differentiableAt

Scalar Multiplication Preserves Differentiability at a Point

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function differentiable at a point $x \in E$. Then for any scalar $c \in R$, the function $y \mapsto c \cdot f(y)$ is differentiable at $x$.

DifferentiableOn.const_smul theorem

(h : DifferentiableOn 𝕜 f s) (c : R) : DifferentiableOn 𝕜 (fun y => c • f y) s

Full source

@[fun_prop]
theorem DifferentiableOn.const_smul (h : DifferentiableOn 𝕜 f s) (c : R) :
    DifferentiableOn 𝕜 (fun y => c • f y) s := fun x hx => (h x hx).const_smul c

Differentiability of Scalar Multiple on a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function differentiable on a set $s \subseteq E$. Then for any scalar $c \in R$, the function $y \mapsto c \cdot f(y)$ is differentiable on $s$.

Differentiable.const_smul theorem

(h : Differentiable 𝕜 f) (c : R) : Differentiable 𝕜 fun y => c • f y

Full source

@[fun_prop]
theorem Differentiable.const_smul (h : Differentiable 𝕜 f) (c : R) :
    Differentiable 𝕜 fun y => c • f y := fun x => (h x).const_smul c

Differentiability is preserved under scalar multiplication

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a differentiable function. Then for any scalar $c \in R$, the function $y \mapsto c \cdot f(y)$ is differentiable.

fderivWithin_const_smul theorem

 (hxs : UniqueDiffWithinAt 𝕜 s x) (h : DifferentiableWithinAt 𝕜 f s x) (c : R) :
  fderivWithin 𝕜 (fun y => c • f y) s x = c • fderivWithin 𝕜 f s x

Full source

theorem fderivWithin_const_smul (hxs : UniqueDiffWithinAt 𝕜 s x)
    (h : DifferentiableWithinAt 𝕜 f s x) (c : R) :
    fderivWithin 𝕜 (fun y => c • f y) s x = c • fderivWithin 𝕜 f s x :=
  (h.hasFDerivWithinAt.const_smul c).fderivWithin hxs

Fréchet Derivative of Scalar Multiple within a Set: $\text{fderivWithin}_{\mathbb{K}} (c \cdot f) s x = c \cdot \text{fderivWithin}_{\mathbb{K}} f s x$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function differentiable at a point $x \in E$ within a set $s \subseteq E$. If $s$ is uniquely differentiable at $x$ (i.e., the tangent cone at $x$ spans a dense subspace of $E$), then for any scalar $c \in R$, the Fréchet derivative of the function $y \mapsto c \cdot f(y)$ at $x$ within $s$ is equal to $c$ times the Fréchet derivative of $f$ at $x$ within $s$, i.e., \[ \text{fderivWithin}_{\mathbb{K}} (c \cdot f) s x = c \cdot \text{fderivWithin}_{\mathbb{K}} f s x. \]

fderivWithin_const_smul' theorem

 (hxs : UniqueDiffWithinAt 𝕜 s x) (h : DifferentiableWithinAt 𝕜 f s x) (c : R) :
  fderivWithin 𝕜 (c • f) s x = c • fderivWithin 𝕜 f s x

Full source

/-- Version of `fderivWithin_const_smul` written with `c • f` instead of `fun y ↦ c • f y`. -/
theorem fderivWithin_const_smul' (hxs : UniqueDiffWithinAt 𝕜 s x)
    (h : DifferentiableWithinAt 𝕜 f s x) (c : R) :
    fderivWithin 𝕜 (c • f) s x = c • fderivWithin 𝕜 f s x :=
  fderivWithin_const_smul hxs h c

Fréchet Derivative of Scalar Multiple within a Set: $\text{fderivWithin}_{\mathbb{K}} (c \cdot f) s x = c \cdot \text{fderivWithin}_{\mathbb{K}} f s x$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function differentiable at a point $x \in E$ within a set $s \subseteq E$. If $s$ is uniquely differentiable at $x$ (i.e., the tangent cone at $x$ spans a dense subspace of $E$), then for any scalar $c \in R$, the Fréchet derivative of the scalar multiple $c \cdot f$ at $x$ within $s$ is equal to $c$ times the Fréchet derivative of $f$ at $x$ within $s$, i.e., \[ \text{fderivWithin}_{\mathbb{K}} (c \cdot f) s x = c \cdot \text{fderivWithin}_{\mathbb{K}} f s x. \]

fderiv_const_smul theorem

(h : DifferentiableAt 𝕜 f x) (c : R) : fderiv 𝕜 (fun y => c • f y) x = c • fderiv 𝕜 f x

Full source

theorem fderiv_const_smul (h : DifferentiableAt 𝕜 f x) (c : R) :
    fderiv 𝕜 (fun y => c • f y) x = c • fderiv 𝕜 f x :=
  (h.hasFDerivAt.const_smul c).fderiv

Fréchet Derivative of Scalar Multiple: $\text{fderiv}_{\mathbb{K}} (c \cdot f) x = c \cdot \text{fderiv}_{\mathbb{K}} f x$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function differentiable at a point $x \in E$. Then for any scalar $c \in R$, the Fréchet derivative of the function $y \mapsto c \cdot f(y)$ at $x$ is equal to $c$ times the Fréchet derivative of $f$ at $x$, i.e., \[ \text{fderiv}_{\mathbb{K}} (c \cdot f) x = c \cdot \text{fderiv}_{\mathbb{K}} f x. \]

fderiv_const_smul' theorem

(h : DifferentiableAt 𝕜 f x) (c : R) : fderiv 𝕜 (c • f) x = c • fderiv 𝕜 f x

Full source

/-- Version of `fderiv_const_smul` written with `c • f` instead of `fun y ↦ c • f y`. -/
theorem fderiv_const_smul' (h : DifferentiableAt 𝕜 f x) (c : R) :
    fderiv 𝕜 (c • f) x = c • fderiv 𝕜 f x :=
  (h.hasFDerivAt.const_smul c).fderiv

Scalar Multiplication Rule for Fréchet Derivatives: $\text{fderiv}(c \cdot f) = c \cdot \text{fderiv} f$

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, and let $f : E \to F$ be a function differentiable at a point $x \in E$. Then for any scalar $c \in R$, the Fréchet derivative of the function $c \cdot f$ at $x$ is equal to $c$ times the Fréchet derivative of $f$ at $x$, i.e., \[ \text{fderiv}_{\mathbb{K}} (c \cdot f) x = c \cdot \text{fderiv}_{\mathbb{K}} f x. \]

HasStrictFDerivAt.add theorem

(hf : HasStrictFDerivAt f f' x) (hg : HasStrictFDerivAt g g' x) : HasStrictFDerivAt (fun y => f y + g y) (f' + g') x

Full source

@[fun_prop]
nonrec theorem HasStrictFDerivAt.add (hf : HasStrictFDerivAt f f' x)
    (hg : HasStrictFDerivAt g g' x) : HasStrictFDerivAt (fun y => f y + g y) (f' + g') x :=
   .of_isLittleO <| (hf.isLittleO.add hg.isLittleO).congr_left fun y => by
    simp only [LinearMap.sub_apply, LinearMap.add_apply, map_sub, map_add, add_apply]
    abel

Strict Fréchet Differentiability of Sum of Functions

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$. Suppose $f, g : E \to F$ are functions that have strict Fréchet derivatives $f'$ and $g'$ at a point $x \in E$, respectively. Then the sum $f + g$ has a strict Fréchet derivative at $x$ given by $f' + g'$.

HasFDerivAtFilter.add theorem

 (hf : HasFDerivAtFilter f f' x L) (hg : HasFDerivAtFilter g g' x L) :
  HasFDerivAtFilter (fun y => f y + g y) (f' + g') x L

Full source

theorem HasFDerivAtFilter.add (hf : HasFDerivAtFilter f f' x L)
    (hg : HasFDerivAtFilter g g' x L) : HasFDerivAtFilter (fun y => f y + g y) (f' + g') x L :=
  .of_isLittleO <| (hf.isLittleO.add hg.isLittleO).congr_left fun _ => by
    simp only [LinearMap.sub_apply, LinearMap.add_apply, map_sub, map_add, add_apply]
    abel

Sum Rule for Fréchet Derivatives Along a Filter

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$. Let $f, g : E \to F$ be functions, $x \in E$, and $L$ a filter on $E$. If $f$ has Fréchet derivative $f'$ at $x$ along $L$ and $g$ has Fréchet derivative $g'$ at $x$ along $L$, then the function $y \mapsto f(y) + g(y)$ has Fréchet derivative $f' + g'$ at $x$ along $L$.

HasFDerivWithinAt.add theorem

 (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt g g' s x) :
  HasFDerivWithinAt (fun y => f y + g y) (f' + g') s x

Full source

@[fun_prop]
nonrec theorem HasFDerivWithinAt.add (hf : HasFDerivWithinAt f f' s x)
    (hg : HasFDerivWithinAt g g' s x) : HasFDerivWithinAt (fun y => f y + g y) (f' + g') s x :=
  hf.add hg

Sum Rule for Fréchet Derivatives Within a Set

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$. Let $f, g : E \to F$ be functions, $x \in E$, and $s \subseteq E$. If $f$ has Fréchet derivative $f'$ at $x$ within $s$ and $g$ has Fréchet derivative $g'$ at $x$ within $s$, then the function $y \mapsto f(y) + g(y)$ has Fréchet derivative $f' + g'$ at $x$ within $s$.

HasFDerivAt.add theorem

(hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) : HasFDerivAt (fun x => f x + g x) (f' + g') x

Full source

@[fun_prop]
nonrec theorem HasFDerivAt.add (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) :
    HasFDerivAt (fun x => f x + g x) (f' + g') x :=
  hf.add hg

Sum Rule for Fréchet Derivatives at a Point

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$. Given two functions $f, g : E \to F$ that are Fréchet differentiable at a point $x \in E$ with derivatives $f'$ and $g'$ respectively, the sum function $x \mapsto f(x) + g(x)$ is Fréchet differentiable at $x$ with derivative $f' + g'$.

DifferentiableWithinAt.add theorem

 (hf : DifferentiableWithinAt 𝕜 f s x) (hg : DifferentiableWithinAt 𝕜 g s x) :
  DifferentiableWithinAt 𝕜 (fun y => f y + g y) s x

Full source

@[fun_prop]
theorem DifferentiableWithinAt.add (hf : DifferentiableWithinAt 𝕜 f s x)
    (hg : DifferentiableWithinAt 𝕜 g s x) : DifferentiableWithinAt 𝕜 (fun y => f y + g y) s x :=
  (hf.hasFDerivWithinAt.add hg.hasFDerivWithinAt).differentiableWithinAt

Differentiability of Sum of Functions Within a Set

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, let $f, g : E \to F$ be functions, and let $x \in E$ be a point within a subset $s \subseteq E$. If $f$ is differentiable at $x$ within $s$ and $g$ is differentiable at $x$ within $s$, then the function $y \mapsto f(y) + g(y)$ is differentiable at $x$ within $s$.

DifferentiableAt.add theorem

(hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) : DifferentiableAt 𝕜 (fun y => f y + g y) x

Full source

@[simp, fun_prop]
theorem DifferentiableAt.add (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
    DifferentiableAt 𝕜 (fun y => f y + g y) x :=
  (hf.hasFDerivAt.add hg.hasFDerivAt).differentiableAt

Differentiability of Sum of Functions at a Point

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$. If two functions $f, g : E \to F$ are differentiable at a point $x \in E$, then their sum $y \mapsto f(y) + g(y)$ is also differentiable at $x$.

DifferentiableOn.add theorem

(hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s) : DifferentiableOn 𝕜 (fun y => f y + g y) s

Full source

@[fun_prop]
theorem DifferentiableOn.add (hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s) :
    DifferentiableOn 𝕜 (fun y => f y + g y) s := fun x hx => (hf x hx).add (hg x hx)

Differentiability of Sum of Functions on a Set

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, and let $f, g : E \to F$ be functions. If $f$ and $g$ are differentiable on a subset $s \subseteq E$, then their sum $y \mapsto f(y) + g(y)$ is also differentiable on $s$.

Differentiable.add theorem

(hf : Differentiable 𝕜 f) (hg : Differentiable 𝕜 g) : Differentiable 𝕜 fun y => f y + g y

Full source

@[simp, fun_prop]
theorem Differentiable.add (hf : Differentiable 𝕜 f) (hg : Differentiable 𝕜 g) :
    Differentiable 𝕜 fun y => f y + g y := fun x => (hf x).add (hg x)

Differentiability of Sum of Differentiable Functions

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$. If two functions $f, g : E \to F$ are differentiable, then their sum $y \mapsto f(y) + g(y)$ is also differentiable.

fderivWithin_add theorem

 (hxs : UniqueDiffWithinAt 𝕜 s x) (hf : DifferentiableWithinAt 𝕜 f s x) (hg : DifferentiableWithinAt 𝕜 g s x) :
  fderivWithin 𝕜 (fun y => f y + g y) s x = fderivWithin 𝕜 f s x + fderivWithin 𝕜 g s x

Full source

theorem fderivWithin_add (hxs : UniqueDiffWithinAt 𝕜 s x) (hf : DifferentiableWithinAt 𝕜 f s x)
    (hg : DifferentiableWithinAt 𝕜 g s x) :
    fderivWithin 𝕜 (fun y => f y + g y) s x = fderivWithin 𝕜 f s x + fderivWithin 𝕜 g s x :=
  (hf.hasFDerivWithinAt.add hg.hasFDerivWithinAt).fderivWithin hxs

Sum Rule for Fréchet Derivatives Within a Set: $\text{fderivWithin}_{\mathbb{K}} (f + g) s x = \text{fderivWithin}_{\mathbb{K}} f s x + \text{fderivWithin}_{\mathbb{K}} g s x$

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, and let $f, g : E \to F$ be functions differentiable at a point $x \in E$ within a subset $s \subseteq E$. If $s$ is uniquely differentiable at $x$, then the Fréchet derivative of $f + g$ at $x$ within $s$ is equal to the sum of their derivatives, i.e., $$ \text{fderivWithin}_{\mathbb{K}} (f + g) s x = \text{fderivWithin}_{\mathbb{K}} f s x + \text{fderivWithin}_{\mathbb{K}} g s x. $$

fderivWithin_add' theorem

 (hxs : UniqueDiffWithinAt 𝕜 s x) (hf : DifferentiableWithinAt 𝕜 f s x) (hg : DifferentiableWithinAt 𝕜 g s x) :
  fderivWithin 𝕜 (f + g) s x = fderivWithin 𝕜 f s x + fderivWithin 𝕜 g s x

Full source

/-- Version of `fderivWithin_add` where the function is written as `f + g` instead
of `fun y ↦ f y + g y`. -/
theorem fderivWithin_add' (hxs : UniqueDiffWithinAt 𝕜 s x) (hf : DifferentiableWithinAt 𝕜 f s x)
    (hg : DifferentiableWithinAt 𝕜 g s x) :
    fderivWithin 𝕜 (f + g) s x = fderivWithin 𝕜 f s x + fderivWithin 𝕜 g s x :=
  fderivWithin_add hxs hf hg

Sum Rule for Fréchet Derivatives Within a Set (Pointwise Addition Form)

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, and let $f, g : E \to F$ be functions differentiable at a point $x \in E$ within a subset $s \subseteq E$. If $s$ is uniquely differentiable at $x$, then the Fréchet derivative of $f + g$ at $x$ within $s$ is equal to the sum of their derivatives, i.e., $$ \text{fderivWithin}_{\mathbb{K}} (f + g) s x = \text{fderivWithin}_{\mathbb{K}} f s x + \text{fderivWithin}_{\mathbb{K}} g s x. $$

fderiv_add theorem

 (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
  fderiv 𝕜 (fun y => f y + g y) x = fderiv 𝕜 f x + fderiv 𝕜 g x

Full source

theorem fderiv_add (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
    fderiv 𝕜 (fun y => f y + g y) x = fderiv 𝕜 f x + fderiv 𝕜 g x :=
  (hf.hasFDerivAt.add hg.hasFDerivAt).fderiv

Sum Rule for Fréchet Derivatives: $\text{fderiv}_{\mathbb{K}} (f + g) x = \text{fderiv}_{\mathbb{K}} f x + \text{fderiv}_{\mathbb{K}} g x$

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, and let $f, g : E \to F$ be functions differentiable at a point $x \in E$. Then the Fréchet derivative of the sum function $y \mapsto f(y) + g(y)$ at $x$ is equal to the sum of their derivatives, i.e., $$ \text{fderiv}_{\mathbb{K}} (f + g) x = \text{fderiv}_{\mathbb{K}} f x + \text{fderiv}_{\mathbb{K}} g x. $$

fderiv_add' theorem

 (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) : fderiv 𝕜 (f + g) x = fderiv 𝕜 f x + fderiv 𝕜 g x

Full source

/-- Version of `fderiv_add` where the function is written as `f + g` instead
of `fun y ↦ f y + g y`. -/
theorem fderiv_add' (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
    fderiv 𝕜 (f + g) x = fderiv 𝕜 f x + fderiv 𝕜 g x :=
  fderiv_add hf hg

Sum Rule for Fréchet Derivatives: $\text{fderiv}_{\mathbb{K}} (f + g) x = \text{fderiv}_{\mathbb{K}} f x + \text{fderiv}_{\mathbb{K}} g x$

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, and let $f, g : E \to F$ be functions differentiable at a point $x \in E$. Then the Fréchet derivative of $f + g$ at $x$ equals the sum of their derivatives, i.e., $$ \text{fderiv}_{\mathbb{K}} (f + g) x = \text{fderiv}_{\mathbb{K}} f x + \text{fderiv}_{\mathbb{K}} g x. $$

hasFDerivAtFilter_add_const_iff theorem

(c : F) : HasFDerivAtFilter (f · + c) f' x L ↔ HasFDerivAtFilter f f' x L

Full source

@[simp]
theorem hasFDerivAtFilter_add_const_iff (c : F) :
    HasFDerivAtFilterHasFDerivAtFilter (f · + c) f' x L ↔ HasFDerivAtFilter f f' x L := by
  simp [hasFDerivAtFilter_iff_isLittleOTVS]

Fréchet Derivative of a Function Plus Constant Along a Filter

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ be a function, $f' : E \toL[\mathbb{K}] F$ be a continuous linear map, $x \in E$, and $L$ be a filter on $E$. For any constant $c \in F$, the function $f$ has Fréchet derivative $f'$ at $x$ along the filter $L$ if and only if the function $y \mapsto f(y) + c$ has Fréchet derivative $f'$ at $x$ along $L$.

hasStrictFDerivAt_add_const_iff theorem

(c : F) : HasStrictFDerivAt (f · + c) f' x ↔ HasStrictFDerivAt f f' x

Full source

@[simp]
theorem hasStrictFDerivAt_add_const_iff (c : F) :
    HasStrictFDerivAtHasStrictFDerivAt (f · + c) f' x ↔ HasStrictFDerivAt f f' x := by
  simp [hasStrictFDerivAt_iff_isLittleO]

Strict Fréchet Differentiability of a Function Plus Constant at a Point

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ be a function, $f' : E \toL[\mathbb{K}] F$ be a continuous linear map, and $x \in E$. For any constant $c \in F$, the function $y \mapsto f(y) + c$ has strict Fréchet derivative $f'$ at $x$ if and only if $f$ has strict Fréchet derivative $f'$ at $x$.

hasFDerivWithinAt_add_const_iff theorem

(c : F) : HasFDerivWithinAt (f · + c) f' s x ↔ HasFDerivWithinAt f f' s x

Full source

@[simp]
theorem hasFDerivWithinAt_add_const_iff (c : F) :
    HasFDerivWithinAtHasFDerivWithinAt (f · + c) f' s x ↔ HasFDerivWithinAt f f' s x :=
  hasFDerivAtFilter_add_const_iff c

Fréchet Derivative of a Function Plus Constant Within a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ be a function, $f' : E \toL[\mathbb{K}] F$ be a continuous linear map, $x \in E$, and $s \subseteq E$. For any constant $c \in F$, the function $f$ has Fréchet derivative $f'$ at $x$ within the set $s$ if and only if the function $y \mapsto f(y) + c$ has Fréchet derivative $f'$ at $x$ within $s$.

hasFDerivAt_add_const_iff theorem

(c : F) : HasFDerivAt (f · + c) f' x ↔ HasFDerivAt f f' x

Full source

@[simp]
theorem hasFDerivAt_add_const_iff (c : F) : HasFDerivAtHasFDerivAt (f · + c) f' x ↔ HasFDerivAt f f' x :=
  hasFDerivAtFilter_add_const_iff c

Fréchet Derivative of a Function Plus Constant at a Point

Informal description

For any constant $c \in F$, the function $x \mapsto f(x) + c$ has Fréchet derivative $f'$ at $x$ if and only if $f$ has Fréchet derivative $f'$ at $x$.

differentiableWithinAt_add_const_iff theorem

(c : F) : DifferentiableWithinAt 𝕜 (fun y => f y + c) s x ↔ DifferentiableWithinAt 𝕜 f s x

Full source

@[simp]
theorem differentiableWithinAt_add_const_iff (c : F) :
    DifferentiableWithinAtDifferentiableWithinAt 𝕜 (fun y => f y + c) s x ↔ DifferentiableWithinAt 𝕜 f s x :=
  exists_congr fun _ ↦ hasFDerivWithinAt_add_const_iff c

Differentiability of a Function Plus Constant Within a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ be a function, $x \in E$, and $s \subseteq E$. For any constant $c \in F$, the function $y \mapsto f(y) + c$ is differentiable at $x$ within the set $s$ if and only if $f$ is differentiable at $x$ within $s$.

differentiableAt_add_const_iff theorem

(c : F) : DifferentiableAt 𝕜 (fun y => f y + c) x ↔ DifferentiableAt 𝕜 f x

Full source

@[simp]
theorem differentiableAt_add_const_iff (c : F) :
    DifferentiableAtDifferentiableAt 𝕜 (fun y => f y + c) x ↔ DifferentiableAt 𝕜 f x :=
  exists_congr fun _ ↦ hasFDerivAt_add_const_iff c

Differentiability of a Function Plus Constant at a Point

Informal description

For any constant $c \in F$, the function $y \mapsto f(y) + c$ is differentiable at $x$ if and only if $f$ is differentiable at $x$.

differentiableOn_add_const_iff theorem

(c : F) : DifferentiableOn 𝕜 (fun y => f y + c) s ↔ DifferentiableOn 𝕜 f s

Full source

@[simp]
theorem differentiableOn_add_const_iff (c : F) :
    DifferentiableOnDifferentiableOn 𝕜 (fun y => f y + c) s ↔ DifferentiableOn 𝕜 f s :=
  forall₂_congr fun _ _ ↦ differentiableWithinAt_add_const_iff c

Differentiability of Function Plus Constant on a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ be a function, and $s \subseteq E$ be a subset. For any constant $c \in F$, the function $y \mapsto f(y) + c$ is differentiable on $s$ if and only if $f$ is differentiable on $s$.

differentiable_add_const_iff theorem

(c : F) : (Differentiable 𝕜 fun y => f y + c) ↔ Differentiable 𝕜 f

Full source

@[simp]
theorem differentiable_add_const_iff (c : F) :
    (Differentiable 𝕜 fun y => f y + c) ↔ Differentiable 𝕜 f :=
  forall_congr' fun _ ↦ differentiableAt_add_const_iff c

Differentiability of a Function Plus Constant

Informal description

For any constant $c \in F$, the function $y \mapsto f(y) + c$ is differentiable (on the entire space) if and only if $f$ is differentiable.

fderivWithin_add_const theorem

(c : F) : fderivWithin 𝕜 (fun y => f y + c) s x = fderivWithin 𝕜 f s x

Full source

@[simp]
theorem fderivWithin_add_const (c : F) :
    fderivWithin 𝕜 (fun y => f y + c) s x = fderivWithin 𝕜 f s x := by
  classical simp [fderivWithin]

Fréchet Derivative of Function Plus Constant Within Set

Informal description

For a function $f : E \to F$ between normed spaces $E$ and $F$ over a non-discrete normed field $\mathbb{K}$, a point $x \in E$, a subset $s \subseteq E$, and a constant $c \in F$, the Fréchet derivative of the function $y \mapsto f(y) + c$ at $x$ within $s$ is equal to the Fréchet derivative of $f$ at $x$ within $s$. That is, \[ \text{fderivWithin}_{\mathbb{K}} (\lambda y, f(y) + c) s x = \text{fderivWithin}_{\mathbb{K}} f s x. \]

fderiv_add_const theorem

(c : F) : fderiv 𝕜 (fun y => f y + c) x = fderiv 𝕜 f x

Full source

@[simp]
theorem fderiv_add_const (c : F) : fderiv 𝕜 (fun y => f y + c) x = fderiv 𝕜 f x := by
  simp only [← fderivWithin_univ, fderivWithin_add_const]

Fréchet Derivative of Function Plus Constant

Informal description

For a function $f : E \to F$ between normed spaces $E$ and $F$ over a non-discrete normed field $\mathbb{K}$, a point $x \in E$, and a constant $c \in F$, the Fréchet derivative of the function $y \mapsto f(y) + c$ at $x$ is equal to the Fréchet derivative of $f$ at $x$. That is, \[ \text{fderiv}_{\mathbb{K}} (\lambda y, f(y) + c) x = \text{fderiv}_{\mathbb{K}} f x. \]

hasFDerivAtFilter_const_add_iff theorem

(c : F) : HasFDerivAtFilter (c + f ·) f' x L ↔ HasFDerivAtFilter f f' x L

Full source

@[simp]
theorem hasFDerivAtFilter_const_add_iff (c : F) :
    HasFDerivAtFilterHasFDerivAtFilter (c + f ·) f' x L ↔ HasFDerivAtFilter f f' x L := by
  simpa only [add_comm] using hasFDerivAtFilter_add_const_iff c

Fréchet Derivative of Constant Plus Function Along a Filter

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ be a function, $f' : E \toL[\mathbb{K}] F$ be a continuous linear map, $x \in E$, and $L$ be a filter on $E$. For any constant $c \in F$, the function $f$ has Fréchet derivative $f'$ at $x$ along the filter $L$ if and only if the function $y \mapsto c + f(y)$ has Fréchet derivative $f'$ at $x$ along $L$.

hasStrictFDerivAt_const_add_iff theorem

(c : F) : HasStrictFDerivAt (c + f ·) f' x ↔ HasStrictFDerivAt f f' x

Full source

@[simp]
theorem hasStrictFDerivAt_const_add_iff (c : F) :
    HasStrictFDerivAtHasStrictFDerivAt (c + f ·) f' x ↔ HasStrictFDerivAt f f' x := by
  simpa only [add_comm] using hasStrictFDerivAt_add_const_iff c

Strict Fréchet Differentiability of Constant Plus Function at a Point

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ be a function, $f' : E \toL[\mathbb{K}] F$ be a continuous linear map, and $x \in E$. For any constant $c \in F$, the function $y \mapsto c + f(y)$ has strict Fréchet derivative $f'$ at $x$ if and only if $f$ has strict Fréchet derivative $f'$ at $x$.

hasFDerivWithinAt_const_add_iff theorem

(c : F) : HasFDerivWithinAt (c + f ·) f' s x ↔ HasFDerivWithinAt f f' s x

Full source

@[simp]
theorem hasFDerivWithinAt_const_add_iff (c : F) :
    HasFDerivWithinAtHasFDerivWithinAt (c + f ·) f' s x ↔ HasFDerivWithinAt f f' s x :=
  hasFDerivAtFilter_const_add_iff c

Fréchet Derivative of Constant Plus Function Within a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ be a function, $f' : E \toL[\mathbb{K}] F$ be a continuous linear map, $s \subseteq E$ be a subset, and $x \in E$. For any constant $c \in F$, the function $f$ has Fréchet derivative $f'$ at $x$ within the set $s$ if and only if the function $y \mapsto c + f(y)$ has Fréchet derivative $f'$ at $x$ within $s$.

hasFDerivAt_const_add_iff theorem

(c : F) : HasFDerivAt (c + f ·) f' x ↔ HasFDerivAt f f' x

Full source

@[simp]
theorem hasFDerivAt_const_add_iff (c : F) : HasFDerivAtHasFDerivAt (c + f ·) f' x ↔ HasFDerivAt f f' x :=
  hasFDerivAtFilter_const_add_iff c

Fréchet Derivative of Constant Plus Function at a Point

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ be a function, $f' : E \toL[\mathbb{K}] F$ be a continuous linear map, and $x \in E$. For any constant $c \in F$, the function $y \mapsto c + f(y)$ has Fréchet derivative $f'$ at $x$ if and only if $f$ has Fréchet derivative $f'$ at $x$.

differentiableWithinAt_const_add_iff theorem

(c : F) : DifferentiableWithinAt 𝕜 (fun y => c + f y) s x ↔ DifferentiableWithinAt 𝕜 f s x

Full source

@[simp]
theorem differentiableWithinAt_const_add_iff (c : F) :
    DifferentiableWithinAtDifferentiableWithinAt 𝕜 (fun y => c + f y) s x ↔ DifferentiableWithinAt 𝕜 f s x :=
  exists_congr fun _ ↦ hasFDerivWithinAt_const_add_iff c

Differentiability of Constant Plus Function Within a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ be a function, $s \subseteq E$ be a subset, and $x \in E$. For any constant $c \in F$, the function $y \mapsto c + f(y)$ is differentiable at $x$ within $s$ if and only if $f$ is differentiable at $x$ within $s$.

differentiableAt_const_add_iff theorem

(c : F) : DifferentiableAt 𝕜 (fun y => c + f y) x ↔ DifferentiableAt 𝕜 f x

Full source

@[simp]
theorem differentiableAt_const_add_iff (c : F) :
    DifferentiableAtDifferentiableAt 𝕜 (fun y => c + f y) x ↔ DifferentiableAt 𝕜 f x :=
  exists_congr fun _ ↦ hasFDerivAt_const_add_iff c

Differentiability of Constant Plus Function at a Point

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ be a function, and $x \in E$. For any constant $c \in F$, the function $y \mapsto c + f(y)$ is differentiable at $x$ if and only if $f$ is differentiable at $x$.

differentiableOn_const_add_iff theorem

(c : F) : DifferentiableOn 𝕜 (fun y => c + f y) s ↔ DifferentiableOn 𝕜 f s

Full source

@[simp]
theorem differentiableOn_const_add_iff (c : F) :
    DifferentiableOnDifferentiableOn 𝕜 (fun y => c + f y) s ↔ DifferentiableOn 𝕜 f s :=
  forall₂_congr fun _ _ ↦ differentiableWithinAt_const_add_iff c

Differentiability of Constant Plus Function on a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ be a function, and $s \subseteq E$ be a subset. For any constant $c \in F$, the function $y \mapsto c + f(y)$ is differentiable on $s$ if and only if $f$ is differentiable on $s$.

differentiable_const_add_iff theorem

(c : F) : (Differentiable 𝕜 fun y => c + f y) ↔ Differentiable 𝕜 f

Full source

@[simp]
theorem differentiable_const_add_iff (c : F) :
    (Differentiable 𝕜 fun y => c + f y) ↔ Differentiable 𝕜 f :=
  forall_congr' fun _ ↦ differentiableAt_const_add_iff c

Differentiability of Constant Plus Function: $c + f$ differentiable iff $f$ differentiable

Informal description

For a function $f : E \to F$ between normed spaces $E$ and $F$ over a nontrivially normed field $\mathbb{K}$, and for any constant $c \in F$, the function $y \mapsto c + f(y)$ is differentiable on $E$ if and only if $f$ is differentiable on $E$.

fderivWithin_const_add theorem

(c : F) : fderivWithin 𝕜 (fun y => c + f y) s x = fderivWithin 𝕜 f s x

Full source

@[simp]
theorem fderivWithin_const_add (c : F) :
    fderivWithin 𝕜 (fun y => c + f y) s x = fderivWithin 𝕜 f s x := by
  simpa only [add_comm] using fderivWithin_add_const c

Fréchet Derivative of Constant Plus Function Within Set

Informal description

For a function $f : E \to F$ between normed spaces $E$ and $F$ over a non-discrete normed field $\mathbb{K}$, a point $x \in E$, a subset $s \subseteq E$, and a constant $c \in F$, the Fréchet derivative of the function $y \mapsto c + f(y)$ at $x$ within $s$ is equal to the Fréchet derivative of $f$ at $x$ within $s$. That is, \[ \text{fderivWithin}_{\mathbb{K}} (\lambda y, c + f(y)) s x = \text{fderivWithin}_{\mathbb{K}} f s x. \]

fderiv_const_add theorem

(c : F) : fderiv 𝕜 (fun y => c + f y) x = fderiv 𝕜 f x

Full source

@[simp]
theorem fderiv_const_add (c : F) : fderiv 𝕜 (fun y => c + f y) x = fderiv 𝕜 f x := by
  simp only [add_comm c, fderiv_add_const]

Fréchet Derivative of Constant Plus Function: $\text{fderiv}_{\mathbb{K}} (c + f) x = \text{fderiv}_{\mathbb{K}} f x$

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, and let $f : E \to F$ be a differentiable function at $x \in E$. For any constant $c \in F$, the Fréchet derivative of the function $y \mapsto c + f(y)$ at $x$ is equal to the Fréchet derivative of $f$ at $x$, i.e., \[ \text{fderiv}_{\mathbb{K}} (\lambda y, c + f(y)) x = \text{fderiv}_{\mathbb{K}} f x. \]

HasStrictFDerivAt.sum theorem

 (h : ∀ i ∈ u, HasStrictFDerivAt (A i) (A' i) x) : HasStrictFDerivAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x

Full source

@[fun_prop]
theorem HasStrictFDerivAt.sum (h : ∀ i ∈ u, HasStrictFDerivAt (A i) (A' i) x) :
    HasStrictFDerivAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x := by
  simp only [hasStrictFDerivAt_iff_isLittleO] at *
  convert IsLittleO.sum h
  simp [Finset.sum_sub_distrib, ContinuousLinearMap.sum_apply]

Strict Fréchet Differentiability of Finite Sums

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, and let $x \in E$. For a finite set $u$ and a family of functions $A_i : E \to F$ with strict Fréchet derivatives $A'_i : E \toL[\mathbb{K}] F$ at $x$ for each $i \in u$, the sum function $\sum_{i \in u} A_i$ has strict Fréchet derivative $\sum_{i \in u} A'_i$ at $x$.

HasFDerivAtFilter.sum theorem

 (h : ∀ i ∈ u, HasFDerivAtFilter (A i) (A' i) x L) : HasFDerivAtFilter (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x L

Full source

theorem HasFDerivAtFilter.sum (h : ∀ i ∈ u, HasFDerivAtFilter (A i) (A' i) x L) :
    HasFDerivAtFilter (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x L := by
  simp only [hasFDerivAtFilter_iff_isLittleO] at *
  convert IsLittleO.sum h
  simp [ContinuousLinearMap.sum_apply]

Sum Rule for Fréchet Derivatives Along a Filter: $(\sum_{i \in u} A_i)' = \sum_{i \in u} A'_i$

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, and let $u$ be a finite set. For each $i \in u$, let $A_i : E \to F$ be a function and $A'_i : E \toL[\mathbb{K}] F$ be a continuous linear map. Suppose that for each $i \in u$, the function $A_i$ has Fréchet derivative $A'_i$ at $x \in E$ along the filter $L$ on $E$. Then the sum function $\sum_{i \in u} A_i$ has Fréchet derivative $\sum_{i \in u} A'_i$ at $x$ along $L$.

HasFDerivWithinAt.sum theorem

 (h : ∀ i ∈ u, HasFDerivWithinAt (A i) (A' i) s x) : HasFDerivWithinAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) s x

Full source

@[fun_prop]
theorem HasFDerivWithinAt.sum (h : ∀ i ∈ u, HasFDerivWithinAt (A i) (A' i) s x) :
    HasFDerivWithinAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) s x :=
  HasFDerivAtFilter.sum h

Sum Rule for Fréchet Derivatives Within a Set: $(\sum_{i \in u} A_i)' = \sum_{i \in u} A'_i$ on $s$ at $x$

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, $s \subseteq E$ be a subset, and $x \in E$. For a finite set $u$ and a family of functions $A_i : E \to F$ with Fréchet derivatives $A'_i : E \toL[\mathbb{K}] F$ within $s$ at $x$ for each $i \in u$, the sum function $\sum_{i \in u} A_i$ has Fréchet derivative $\sum_{i \in u} A'_i$ within $s$ at $x$.

HasFDerivAt.sum theorem

(h : ∀ i ∈ u, HasFDerivAt (A i) (A' i) x) : HasFDerivAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x

Full source

@[fun_prop]
theorem HasFDerivAt.sum (h : ∀ i ∈ u, HasFDerivAt (A i) (A' i) x) :
    HasFDerivAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x :=
  HasFDerivAtFilter.sum h

Sum Rule for Fréchet Derivatives: $(\sum_{i \in u} A_i)' = \sum_{i \in u} A'_i$ at a Point

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, and let $u$ be a finite set. For each $i \in u$, let $A_i : E \to F$ be a function and $A'_i : E \toL[\mathbb{K}] F$ be a continuous linear map. If for every $i \in u$, the function $A_i$ has Fréchet derivative $A'_i$ at $x \in E$, then the sum function $\sum_{i \in u} A_i$ has Fréchet derivative $\sum_{i \in u} A'_i$ at $x$.

DifferentiableWithinAt.sum theorem

 (h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x) : DifferentiableWithinAt 𝕜 (fun y => ∑ i ∈ u, A i y) s x

Full source

@[fun_prop]
theorem DifferentiableWithinAt.sum (h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x) :
    DifferentiableWithinAt 𝕜 (fun y => ∑ i ∈ u, A i y) s x :=
  HasFDerivWithinAt.differentiableWithinAt <|
    HasFDerivWithinAt.sum fun i hi => (h i hi).hasFDerivWithinAt

Differentiability of Finite Sums Within a Set at a Point

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, $s \subseteq E$ be a subset, and $x \in E$. For a finite set $u$ and a family of functions $A_i : E \to F$ that are differentiable at $x$ within $s$ for each $i \in u$, the sum function $\sum_{i \in u} A_i$ is differentiable at $x$ within $s$.

DifferentiableAt.sum theorem

(h : ∀ i ∈ u, DifferentiableAt 𝕜 (A i) x) : DifferentiableAt 𝕜 (fun y => ∑ i ∈ u, A i y) x

Full source

@[simp, fun_prop]
theorem DifferentiableAt.sum (h : ∀ i ∈ u, DifferentiableAt 𝕜 (A i) x) :
    DifferentiableAt 𝕜 (fun y => ∑ i ∈ u, A i y) x :=
  HasFDerivAt.differentiableAt <| HasFDerivAt.sum fun i hi => (h i hi).hasFDerivAt

Differentiability of Finite Sums of Functions at a Point

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, and let $u$ be a finite set. For each $i \in u$, let $A_i : E \to F$ be a function. If for every $i \in u$, the function $A_i$ is differentiable at $x \in E$, then the sum function $\sum_{i \in u} A_i$ is differentiable at $x$.

DifferentiableOn.sum theorem

(h : ∀ i ∈ u, DifferentiableOn 𝕜 (A i) s) : DifferentiableOn 𝕜 (fun y => ∑ i ∈ u, A i y) s

Full source

@[fun_prop]
theorem DifferentiableOn.sum (h : ∀ i ∈ u, DifferentiableOn 𝕜 (A i) s) :
    DifferentiableOn 𝕜 (fun y => ∑ i ∈ u, A i y) s := fun x hx =>
  DifferentiableWithinAt.sum fun i hi => h i hi x hx

Differentiability of Finite Sums on a Set

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, $s \subseteq E$ be a subset, and $u$ be a finite set. For a family of functions $A_i : E \to F$ indexed by $i \in u$, if each $A_i$ is differentiable on $s$, then the sum function $\sum_{i \in u} A_i$ is differentiable on $s$.

Differentiable.sum theorem

(h : ∀ i ∈ u, Differentiable 𝕜 (A i)) : Differentiable 𝕜 fun y => ∑ i ∈ u, A i y

Full source

@[simp, fun_prop]
theorem Differentiable.sum (h : ∀ i ∈ u, Differentiable 𝕜 (A i)) :
    Differentiable 𝕜 fun y => ∑ i ∈ u, A i y := fun x => DifferentiableAt.sum fun i hi => h i hi x

Differentiability of Finite Sums of Differentiable Functions

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, and let $u$ be a finite set. For each $i \in u$, let $A_i : E \to F$ be a function. If for every $i \in u$, the function $A_i$ is differentiable on $E$, then the sum function $\sum_{i \in u} A_i$ is differentiable on $E$.

fderivWithin_sum theorem

 (hxs : UniqueDiffWithinAt 𝕜 s x) (h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x) :
  fderivWithin 𝕜 (fun y => ∑ i ∈ u, A i y) s x = ∑ i ∈ u, fderivWithin 𝕜 (A i) s x

Full source

theorem fderivWithin_sum (hxs : UniqueDiffWithinAt 𝕜 s x)
    (h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x) :
    fderivWithin 𝕜 (fun y => ∑ i ∈ u, A i y) s x = ∑ i ∈ u, fderivWithin 𝕜 (A i) s x :=
  (HasFDerivWithinAt.sum fun i hi => (h i hi).hasFDerivWithinAt).fderivWithin hxs

Sum Rule for Fréchet Derivatives Within a Set: $\left(\sum_{i \in u} A_i\right)' = \sum_{i \in u} A_i'$ on $s$ at $x$

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, $s \subseteq E$ be a subset, and $x \in E$ be a point where $s$ is uniquely differentiable. For a finite set $u$ and a family of functions $A_i : E \to F$ indexed by $i \in u$, if each $A_i$ is differentiable at $x$ within $s$, then the Fréchet derivative of the sum function $\sum_{i \in u} A_i$ at $x$ within $s$ is equal to the sum of the Fréchet derivatives of the $A_i$ at $x$ within $s$, i.e., \[ \text{fderivWithin}_{\mathbb{K}} \left( \sum_{i \in u} A_i \right) s x = \sum_{i \in u} \text{fderivWithin}_{\mathbb{K}} (A_i) s x. \]

fderiv_sum theorem

 (h : ∀ i ∈ u, DifferentiableAt 𝕜 (A i) x) : fderiv 𝕜 (fun y => ∑ i ∈ u, A i y) x = ∑ i ∈ u, fderiv 𝕜 (A i) x

Full source

theorem fderiv_sum (h : ∀ i ∈ u, DifferentiableAt 𝕜 (A i) x) :
    fderiv 𝕜 (fun y => ∑ i ∈ u, A i y) x = ∑ i ∈ u, fderiv 𝕜 (A i) x :=
  (HasFDerivAt.sum fun i hi => (h i hi).hasFDerivAt).fderiv

Sum Rule for Fréchet Derivatives: $(\sum_{i \in u} A_i)' = \sum_{i \in u} A_i'$ at a Point

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $u$ be a finite set. For each $i \in u$, let $A_i : E \to F$ be a function differentiable at $x \in E$. Then the Fréchet derivative of the sum function $\sum_{i \in u} A_i$ at $x$ equals the sum of the Fréchet derivatives of the $A_i$ at $x$, i.e., \[ \text{fderiv}_{\mathbb{K}} \left( \sum_{i \in u} A_i \right) x = \sum_{i \in u} \text{fderiv}_{\mathbb{K}} (A_i) x. \]

HasStrictFDerivAt.neg theorem

(h : HasStrictFDerivAt f f' x) : HasStrictFDerivAt (fun x => -f x) (-f') x

Full source

@[fun_prop]
theorem HasStrictFDerivAt.neg (h : HasStrictFDerivAt f f' x) :
    HasStrictFDerivAt (fun x => -f x) (-f') x :=
  (-1 : F →L[𝕜] F).hasStrictFDerivAt.comp x h

Strict Fréchet Derivative of the Negative of a Function

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ has a strict Fréchet derivative $f'$ at a point $x \in E$, then the function $-f$ defined by $x \mapsto -f(x)$ has $-f'$ as its strict Fréchet derivative at $x$.

HasFDerivAtFilter.neg theorem

(h : HasFDerivAtFilter f f' x L) : HasFDerivAtFilter (fun x => -f x) (-f') x L

Full source

theorem HasFDerivAtFilter.neg (h : HasFDerivAtFilter f f' x L) :
    HasFDerivAtFilter (fun x => -f x) (-f') x L :=
  (-1 : F →L[𝕜] F).hasFDerivAtFilter.comp x h tendsto_map

Fréchet derivative of the negative of a function

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function with Fréchet derivative $f'$ at $x \in E$ along the filter $L$ on $E$. Then the function $-f$ has Fréchet derivative $-f'$ at $x$ along $L$.

HasFDerivWithinAt.neg theorem

(h : HasFDerivWithinAt f f' s x) : HasFDerivWithinAt (fun x => -f x) (-f') s x

Full source

@[fun_prop]
nonrec theorem HasFDerivWithinAt.neg (h : HasFDerivWithinAt f f' s x) :
    HasFDerivWithinAt (fun x => -f x) (-f') s x :=
  h.neg

Fréchet Derivative of Negative Function Within a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ has a Fréchet derivative $f'$ at a point $x \in E$ within a set $s \subseteq E$, then the function $-f$ defined by $x \mapsto -f(x)$ has $-f'$ as its Fréchet derivative at $x$ within $s$.

HasFDerivAt.neg theorem

(h : HasFDerivAt f f' x) : HasFDerivAt (fun x => -f x) (-f') x

Full source

@[fun_prop]
nonrec theorem HasFDerivAt.neg (h : HasFDerivAt f f' x) : HasFDerivAt (fun x => -f x) (-f') x :=
  h.neg

Fréchet derivative of the negative of a function at a point

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function that is Fréchet differentiable at $x \in E$ with derivative $f'$. Then the function $-f$ is Fréchet differentiable at $x$ with derivative $-f'$.

DifferentiableWithinAt.neg theorem

(h : DifferentiableWithinAt 𝕜 f s x) : DifferentiableWithinAt 𝕜 (fun y => -f y) s x

Full source

@[fun_prop]
theorem DifferentiableWithinAt.neg (h : DifferentiableWithinAt 𝕜 f s x) :
    DifferentiableWithinAt 𝕜 (fun y => -f y) s x :=
  h.hasFDerivWithinAt.neg.differentiableWithinAt

Differentiability of Negative Function Within a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ is differentiable at a point $x \in E$ within a subset $s \subseteq E$, then the function $-f$ defined by $y \mapsto -f(y)$ is also differentiable at $x$ within $s$.

differentiableWithinAt_neg_iff theorem

: DifferentiableWithinAt 𝕜 (fun y => -f y) s x ↔ DifferentiableWithinAt 𝕜 f s x

Full source

@[simp]
theorem differentiableWithinAt_neg_iff :
    DifferentiableWithinAtDifferentiableWithinAt 𝕜 (fun y => -f y) s x ↔ DifferentiableWithinAt 𝕜 f s x :=
  ⟨fun h => by simpa only [neg_neg] using h.neg, fun h => h.neg⟩

Differentiability of Negative Function Within a Set is Equivalent to Differentiability of Original Function

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any subset $s \subseteq E$ and point $x \in E$, the function $-f$ defined by $y \mapsto -f(y)$ is differentiable at $x$ within $s$ if and only if $f$ is differentiable at $x$ within $s$.

DifferentiableAt.neg theorem

(h : DifferentiableAt 𝕜 f x) : DifferentiableAt 𝕜 (fun y => -f y) x

Full source

@[fun_prop]
theorem DifferentiableAt.neg (h : DifferentiableAt 𝕜 f x) : DifferentiableAt 𝕜 (fun y => -f y) x :=
  h.hasFDerivAt.neg.differentiableAt

Differentiability of the Negative of a Function at a Point

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function differentiable at a point $x \in E$. Then the function $-f$ is differentiable at $x$.

differentiableAt_neg_iff theorem

: DifferentiableAt 𝕜 (fun y => -f y) x ↔ DifferentiableAt 𝕜 f x

Full source

@[simp]
theorem differentiableAt_neg_iff : DifferentiableAtDifferentiableAt 𝕜 (fun y => -f y) x ↔ DifferentiableAt 𝕜 f x :=
  ⟨fun h => by simpa only [neg_neg] using h.neg, fun h => h.neg⟩

Differentiability of Negative Function at a Point is Equivalent to Differentiability of Original Function

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. Then $f$ is differentiable at a point $x \in E$ if and only if the function $-f$ is differentiable at $x$.

DifferentiableOn.neg theorem

(h : DifferentiableOn 𝕜 f s) : DifferentiableOn 𝕜 (fun y => -f y) s

Full source

@[fun_prop]
theorem DifferentiableOn.neg (h : DifferentiableOn 𝕜 f s) : DifferentiableOn 𝕜 (fun y => -f y) s :=
  fun x hx => (h x hx).neg

Differentiability of Negative Function on a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ is differentiable on a set $s \subseteq E$, then the function $-f$ defined by $y \mapsto -f(y)$ is also differentiable on $s$.

differentiableOn_neg_iff theorem

: DifferentiableOn 𝕜 (fun y => -f y) s ↔ DifferentiableOn 𝕜 f s

Full source

@[simp]
theorem differentiableOn_neg_iff : DifferentiableOnDifferentiableOn 𝕜 (fun y => -f y) s ↔ DifferentiableOn 𝕜 f s :=
  ⟨fun h => by simpa only [neg_neg] using h.neg, fun h => h.neg⟩

Differentiability of Negative Function on Set is Equivalent to Differentiability of Original Function

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. Then $f$ is differentiable on a set $s \subseteq E$ if and only if the function $-f$ defined by $y \mapsto -f(y)$ is differentiable on $s$.

Differentiable.neg theorem

(h : Differentiable 𝕜 f) : Differentiable 𝕜 fun y => -f y

Full source

@[fun_prop]
theorem Differentiable.neg (h : Differentiable 𝕜 f) : Differentiable 𝕜 fun y => -f y := fun x =>
  (h x).neg

Differentiability of the Negative of a Differentiable Function

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$. If a function $f : E \to F$ is differentiable, then the function $-f$ defined by $(-f)(y) = -f(y)$ is also differentiable.

differentiable_neg_iff theorem

: (Differentiable 𝕜 fun y => -f y) ↔ Differentiable 𝕜 f

Full source

@[simp]
theorem differentiable_neg_iff : (Differentiable 𝕜 fun y => -f y) ↔ Differentiable 𝕜 f :=
  ⟨fun h => by simpa only [neg_neg] using h.neg, fun h => h.neg⟩

Differentiability of Negative Function Equivalence

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$. A function $f : E \to F$ is differentiable if and only if the function $-f$ defined by $(-f)(y) = -f(y)$ is differentiable.

fderivWithin_neg theorem

(hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 (fun y => -f y) s x = -fderivWithin 𝕜 f s x

Full source

theorem fderivWithin_neg (hxs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 (fun y => -f y) s x = -fderivWithin 𝕜 f s x := by
  classical
  by_cases h : DifferentiableWithinAt 𝕜 f s x
  · exact h.hasFDerivWithinAt.neg.fderivWithin hxs
  · rw [fderivWithin_zero_of_not_differentiableWithinAt h,
      fderivWithin_zero_of_not_differentiableWithinAt, neg_zero]
    simpa

Fréchet Derivative of Negative Function within a Set: $\text{fderivWithin}_{\mathbb{K}} (-f) s x = -\text{fderivWithin}_{\mathbb{K}} f s x$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ be a function, $s \subseteq E$ be a subset, and $x \in E$ be a point where $s$ is uniquely differentiable. Then the Fréchet derivative of $-f$ at $x$ within $s$ equals the negative of the Fréchet derivative of $f$ at $x$ within $s$, i.e., $$ \text{fderivWithin}_{\mathbb{K}} (-f) s x = -\text{fderivWithin}_{\mathbb{K}} f s x. $$

fderivWithin_neg' theorem

(hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 (-f) s x = -fderivWithin 𝕜 f s x

Full source

/-- Version of `fderivWithin_neg` where the function is written `-f` instead of `fun y ↦ - f y`. -/
theorem fderivWithin_neg' (hxs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 (-f) s x = -fderivWithin 𝕜 f s x :=
  fderivWithin_neg hxs

Fréchet Derivative of Negative Function within a Set: $\text{fderivWithin}_{\mathbb{K}} (-f) s x = -\text{fderivWithin}_{\mathbb{K}} f s x$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ be a function, $s \subseteq E$ be a subset, and $x \in E$ be a point where $s$ is uniquely differentiable. Then the Fréchet derivative of $-f$ at $x$ within $s$ equals the negative of the Fréchet derivative of $f$ at $x$ within $s$, i.e., $$ \text{fderivWithin}_{\mathbb{K}} (-f) s x = -\text{fderivWithin}_{\mathbb{K}} f s x. $$

fderiv_neg theorem

: fderiv 𝕜 (fun y => -f y) x = -fderiv 𝕜 f x

Full source

@[simp]
theorem fderiv_neg : fderiv 𝕜 (fun y => -f y) x = -fderiv 𝕜 f x := by
  simp only [← fderivWithin_univ, fderivWithin_neg uniqueDiffWithinAt_univ]

Fréchet Derivative of Negative Function: $\text{fderiv}_{\mathbb{K}} (-f) x = -\text{fderiv}_{\mathbb{K}} f x$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ is Fréchet differentiable at a point $x \in E$, then the Fréchet derivative of the function $-f$ at $x$ is equal to the negative of the Fréchet derivative of $f$ at $x$, i.e., $$ \text{fderiv}_{\mathbb{K}} (-f) x = -\text{fderiv}_{\mathbb{K}} f x. $$

fderiv_neg' theorem

: fderiv 𝕜 (-f) x = -fderiv 𝕜 f x

Full source

/-- Version of `fderiv_neg` where the function is written `-f` instead of `fun y ↦ - f y`. -/
theorem fderiv_neg' : fderiv 𝕜 (-f) x = -fderiv 𝕜 f x :=
  fderiv_neg

Fréchet Derivative of Negative Function: $\text{fderiv}_{\mathbb{K}} (-f) x = -\text{fderiv}_{\mathbb{K}} f x$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ is Fréchet differentiable at a point $x \in E$, then the Fréchet derivative of $-f$ at $x$ is equal to the negative of the Fréchet derivative of $f$ at $x$, i.e., $$ \text{fderiv}_{\mathbb{K}} (-f) x = -\text{fderiv}_{\mathbb{K}} f x. $$

HasStrictFDerivAt.sub theorem

(hf : HasStrictFDerivAt f f' x) (hg : HasStrictFDerivAt g g' x) : HasStrictFDerivAt (fun x => f x - g x) (f' - g') x

Full source

@[fun_prop]
theorem HasStrictFDerivAt.sub (hf : HasStrictFDerivAt f f' x) (hg : HasStrictFDerivAt g g' x) :
    HasStrictFDerivAt (fun x => f x - g x) (f' - g') x := by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

Strict Fréchet Derivative of the Difference of Two Functions

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$. Suppose $f, g : E \to F$ are functions that have strict Fréchet derivatives $f'$ and $g'$ at a point $x \in E$, respectively. Then the difference $f - g$ has a strict Fréchet derivative at $x$ given by $f' - g'$.

HasFDerivAtFilter.sub theorem

 (hf : HasFDerivAtFilter f f' x L) (hg : HasFDerivAtFilter g g' x L) :
  HasFDerivAtFilter (fun x => f x - g x) (f' - g') x L

Full source

theorem HasFDerivAtFilter.sub (hf : HasFDerivAtFilter f f' x L) (hg : HasFDerivAtFilter g g' x L) :
    HasFDerivAtFilter (fun x => f x - g x) (f' - g') x L := by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

Difference Rule for Fréchet Derivatives Along a Filter

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$. Let $f, g : E \to F$ be functions, $x \in E$, and $L$ a filter on $E$. If $f$ has Fréchet derivative $f'$ at $x$ along $L$ and $g$ has Fréchet derivative $g'$ at $x$ along $L$, then the function $x \mapsto f(x) - g(x)$ has Fréchet derivative $f' - g'$ at $x$ along $L$.

HasFDerivWithinAt.sub theorem

 (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt g g' s x) :
  HasFDerivWithinAt (fun x => f x - g x) (f' - g') s x

Full source

@[fun_prop]
nonrec theorem HasFDerivWithinAt.sub (hf : HasFDerivWithinAt f f' s x)
    (hg : HasFDerivWithinAt g g' s x) : HasFDerivWithinAt (fun x => f x - g x) (f' - g') s x :=
  hf.sub hg

Difference Rule for Fréchet Derivatives Within a Set

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$. Let $f, g : E \to F$ be functions, $x \in E$, and $s \subseteq E$. If $f$ has Fréchet derivative $f'$ at $x$ within $s$ and $g$ has Fréchet derivative $g'$ at $x$ within $s$, then the function $x \mapsto f(x) - g(x)$ has Fréchet derivative $f' - g'$ at $x$ within $s$.

HasFDerivAt.sub theorem

(hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) : HasFDerivAt (fun x => f x - g x) (f' - g') x

Full source

@[fun_prop]
nonrec theorem HasFDerivAt.sub (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) :
    HasFDerivAt (fun x => f x - g x) (f' - g') x :=
  hf.sub hg

Difference Rule for Fréchet Derivatives at a Point

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$. If functions $f, g : E \to F$ are Fréchet differentiable at a point $x \in E$ with derivatives $f'$ and $g'$ respectively, then the function $x \mapsto f(x) - g(x)$ is Fréchet differentiable at $x$ with derivative $f' - g'$.

DifferentiableWithinAt.sub theorem

 (hf : DifferentiableWithinAt 𝕜 f s x) (hg : DifferentiableWithinAt 𝕜 g s x) :
  DifferentiableWithinAt 𝕜 (fun y => f y - g y) s x

Full source

@[fun_prop]
theorem DifferentiableWithinAt.sub (hf : DifferentiableWithinAt 𝕜 f s x)
    (hg : DifferentiableWithinAt 𝕜 g s x) : DifferentiableWithinAt 𝕜 (fun y => f y - g y) s x :=
  (hf.hasFDerivWithinAt.sub hg.hasFDerivWithinAt).differentiableWithinAt

Differentiability of Function Difference Within a Set

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$. Given functions $f, g : E \to F$ that are differentiable at a point $x \in E$ within a subset $s \subseteq E$, the function $y \mapsto f(y) - g(y)$ is also differentiable at $x$ within $s$.

DifferentiableAt.sub theorem

(hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) : DifferentiableAt 𝕜 (fun y => f y - g y) x

Full source

@[simp, fun_prop]
theorem DifferentiableAt.sub (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
    DifferentiableAt 𝕜 (fun y => f y - g y) x :=
  (hf.hasFDerivAt.sub hg.hasFDerivAt).differentiableAt

Differentiability of Function Difference at a Point

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$. If functions $f, g : E \to F$ are differentiable at a point $x \in E$, then the function $y \mapsto f(y) - g(y)$ is also differentiable at $x$.

DifferentiableAt.add_iff_left theorem

(hg : DifferentiableAt 𝕜 g x) : DifferentiableAt 𝕜 (fun y => f y + g y) x ↔ DifferentiableAt 𝕜 f x

Full source

@[simp]
lemma DifferentiableAt.add_iff_left (hg : DifferentiableAt 𝕜 g x) :
    DifferentiableAtDifferentiableAt 𝕜 (fun y => f y + g y) x ↔ DifferentiableAt 𝕜 f x := by
  refine ⟨fun h ↦ ?_, fun hf ↦ hf.add hg⟩
  simpa only [add_sub_cancel_right] using h.sub hg

Differentiability of Sum at a Point (Left Condition)

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f, g : E \to F$ be functions. For a point $x \in E$, if $g$ is differentiable at $x$, then the function $y \mapsto f(y) + g(y)$ is differentiable at $x$ if and only if $f$ is differentiable at $x$.

DifferentiableAt.add_iff_right theorem

(hg : DifferentiableAt 𝕜 f x) : DifferentiableAt 𝕜 (fun y => f y + g y) x ↔ DifferentiableAt 𝕜 g x

Full source

@[simp]
lemma DifferentiableAt.add_iff_right (hg : DifferentiableAt 𝕜 f x) :
    DifferentiableAtDifferentiableAt 𝕜 (fun y => f y + g y) x ↔ DifferentiableAt 𝕜 g x := by
  simp only [add_comm (f _), hg.add_iff_left]

Differentiability of Sum at a Point (Right Condition)

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f, g : E \to F$ be functions. For a point $x \in E$, if $f$ is differentiable at $x$, then the function $y \mapsto f(y) + g(y)$ is differentiable at $x$ if and only if $g$ is differentiable at $x$.

DifferentiableAt.sub_iff_left theorem

(hg : DifferentiableAt 𝕜 g x) : DifferentiableAt 𝕜 (fun y => f y - g y) x ↔ DifferentiableAt 𝕜 f x

Full source

@[simp]
lemma DifferentiableAt.sub_iff_left (hg : DifferentiableAt 𝕜 g x) :
    DifferentiableAtDifferentiableAt 𝕜 (fun y => f y - g y) x ↔ DifferentiableAt 𝕜 f x := by
  simp only [sub_eq_add_neg, differentiableAt_neg_iff, hg, add_iff_left]

Differentiability of Function Difference at a Point (Left Condition)

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f, g : E \to F$ be functions. For a point $x \in E$, if $g$ is differentiable at $x$, then the function $f - g$ is differentiable at $x$ if and only if $f$ is differentiable at $x$.

DifferentiableAt.sub_iff_right theorem

(hg : DifferentiableAt 𝕜 f x) : DifferentiableAt 𝕜 (fun y => f y - g y) x ↔ DifferentiableAt 𝕜 g x

Full source

@[simp]
lemma DifferentiableAt.sub_iff_right (hg : DifferentiableAt 𝕜 f x) :
    DifferentiableAtDifferentiableAt 𝕜 (fun y => f y - g y) x ↔ DifferentiableAt 𝕜 g x := by
  simp only [sub_eq_add_neg, hg, add_iff_right, differentiableAt_neg_iff]

Differentiability of difference function at a point iff second function is differentiable

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f, g : E \to F$ be functions differentiable at a point $x \in E$. Then the difference function $y \mapsto f(y) - g(y)$ is differentiable at $x$ if and only if $g$ is differentiable at $x$.

DifferentiableOn.sub theorem

(hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s) : DifferentiableOn 𝕜 (fun y => f y - g y) s

Full source

@[fun_prop]
theorem DifferentiableOn.sub (hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s) :
    DifferentiableOn 𝕜 (fun y => f y - g y) s := fun x hx => (hf x hx).sub (hg x hx)

Differentiability of the difference of two functions on a set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f, g : E \to F$ be functions. If $f$ and $g$ are differentiable on a subset $s \subseteq E$, then the function $y \mapsto f(y) - g(y)$ is also differentiable on $s$.

DifferentiableOn.add_iff_left theorem

(hg : DifferentiableOn 𝕜 g s) : DifferentiableOn 𝕜 (fun y => f y + g y) s ↔ DifferentiableOn 𝕜 f s

Full source

@[simp]
lemma DifferentiableOn.add_iff_left (hg : DifferentiableOn 𝕜 g s) :
    DifferentiableOnDifferentiableOn 𝕜 (fun y => f y + g y) s ↔ DifferentiableOn 𝕜 f s := by
  refine ⟨fun h ↦ ?_, fun hf ↦ hf.add hg⟩
  simpa only [add_sub_cancel_right] using h.sub hg

Differentiability of Sum Function iff Differentiability of First Component

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a set. For functions $f, g : E \to F$, if $g$ is differentiable on $s$, then the sum function $y \mapsto f(y) + g(y)$ is differentiable on $s$ if and only if $f$ is differentiable on $s$.

DifferentiableOn.add_iff_right theorem

(hg : DifferentiableOn 𝕜 f s) : DifferentiableOn 𝕜 (fun y => f y + g y) s ↔ DifferentiableOn 𝕜 g s

Full source

@[simp]
lemma DifferentiableOn.add_iff_right (hg : DifferentiableOn 𝕜 f s) :
    DifferentiableOnDifferentiableOn 𝕜 (fun y => f y + g y) s ↔ DifferentiableOn 𝕜 g s := by
  simp only [add_comm (f _), hg.add_iff_left]

Differentiability of Sum Function iff Differentiability of Second Component

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a set. For functions $f, g : E \to F$, if $f$ is differentiable on $s$, then the sum function $y \mapsto f(y) + g(y)$ is differentiable on $s$ if and only if $g$ is differentiable on $s$.

DifferentiableOn.sub_iff_left theorem

(hg : DifferentiableOn 𝕜 g s) : DifferentiableOn 𝕜 (fun y => f y - g y) s ↔ DifferentiableOn 𝕜 f s

Full source

@[simp]
lemma DifferentiableOn.sub_iff_left (hg : DifferentiableOn 𝕜 g s) :
    DifferentiableOnDifferentiableOn 𝕜 (fun y => f y - g y) s ↔ DifferentiableOn 𝕜 f s := by
  simp only [sub_eq_add_neg, differentiableOn_neg_iff, hg, add_iff_left]

Differentiability of difference function implies differentiability of first component

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a set. For functions $f, g : E \to F$, if $g$ is differentiable on $s$, then the function $y \mapsto f(y) - g(y)$ is differentiable on $s$ if and only if $f$ is differentiable on $s$.

DifferentiableOn.sub_iff_right theorem

(hg : DifferentiableOn 𝕜 f s) : DifferentiableOn 𝕜 (fun y => f y - g y) s ↔ DifferentiableOn 𝕜 g s

Full source

@[simp]
lemma DifferentiableOn.sub_iff_right (hg : DifferentiableOn 𝕜 f s) :
    DifferentiableOnDifferentiableOn 𝕜 (fun y => f y - g y) s ↔ DifferentiableOn 𝕜 g s := by
  simp only [sub_eq_add_neg, differentiableOn_neg_iff, hg, add_iff_right]

Differentiability of Difference Function on a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $s$ be a subset of $E$. Given a function $f : E \to F$ that is differentiable on $s$, the function $y \mapsto f(y) - g(y)$ is differentiable on $s$ if and only if $g$ is differentiable on $s$.

Differentiable.sub theorem

(hf : Differentiable 𝕜 f) (hg : Differentiable 𝕜 g) : Differentiable 𝕜 fun y => f y - g y

Full source

@[simp, fun_prop]
theorem Differentiable.sub (hf : Differentiable 𝕜 f) (hg : Differentiable 𝕜 g) :
    Differentiable 𝕜 fun y => f y - g y := fun x => (hf x).sub (hg x)

Differentiability of the Difference of Differentiable Functions

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$. If $f, g : E \to F$ are differentiable functions, then the function $y \mapsto f(y) - g(y)$ is also differentiable.

Differentiable.add_iff_left theorem

(hg : Differentiable 𝕜 g) : Differentiable 𝕜 (fun y => f y + g y) ↔ Differentiable 𝕜 f

Full source

@[simp]
lemma Differentiable.add_iff_left (hg : Differentiable 𝕜 g) :
    DifferentiableDifferentiable 𝕜 (fun y => f y + g y) ↔ Differentiable 𝕜 f := by
  refine ⟨fun h ↦ ?_, fun hf ↦ hf.add hg⟩
  simpa only [add_sub_cancel_right] using h.sub hg

Differentiability of Sum Function (Left Version)

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$. Given a differentiable function $g : E \to F$, the function $y \mapsto f(y) + g(y)$ is differentiable if and only if $f$ is differentiable.

Differentiable.add_iff_right theorem

(hg : Differentiable 𝕜 f) : Differentiable 𝕜 (fun y => f y + g y) ↔ Differentiable 𝕜 g

Full source

@[simp]
lemma Differentiable.add_iff_right (hg : Differentiable 𝕜 f) :
    DifferentiableDifferentiable 𝕜 (fun y => f y + g y) ↔ Differentiable 𝕜 g := by
  simp only [add_comm (f _), hg.add_iff_left]

Differentiability of Sum Function (Right Version)

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$. Given a differentiable function $f : E \to F$, the function $y \mapsto f(y) + g(y)$ is differentiable if and only if $g$ is differentiable.

Differentiable.sub_iff_left theorem

(hg : Differentiable 𝕜 g) : Differentiable 𝕜 (fun y => f y - g y) ↔ Differentiable 𝕜 f

Full source

@[simp]
lemma Differentiable.sub_iff_left (hg : Differentiable 𝕜 g) :
    DifferentiableDifferentiable 𝕜 (fun y => f y - g y) ↔ Differentiable 𝕜 f := by
  simp only [sub_eq_add_neg, differentiable_neg_iff, hg, add_iff_left]

Differentiability of difference function (left version)

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f, g : E \to F$ be differentiable functions. If $g$ is differentiable, then the function $y \mapsto f(y) - g(y)$ is differentiable if and only if $f$ is differentiable.

Differentiable.sub_iff_right theorem

(hg : Differentiable 𝕜 f) : Differentiable 𝕜 (fun y => f y - g y) ↔ Differentiable 𝕜 g

Full source

@[simp]
lemma Differentiable.sub_iff_right (hg : Differentiable 𝕜 f) :
    DifferentiableDifferentiable 𝕜 (fun y => f y - g y) ↔ Differentiable 𝕜 g := by
  simp only [sub_eq_add_neg, differentiable_neg_iff, hg, add_iff_right]

Differentiability of Difference Function if and only if Second Function is Differentiable

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f, g : E \to F$ be functions. If $f$ is differentiable on $E$, then the function $y \mapsto f(y) - g(y)$ is differentiable on $E$ if and only if $g$ is differentiable on $E$.

fderivWithin_sub theorem

 (hxs : UniqueDiffWithinAt 𝕜 s x) (hf : DifferentiableWithinAt 𝕜 f s x) (hg : DifferentiableWithinAt 𝕜 g s x) :
  fderivWithin 𝕜 (fun y => f y - g y) s x = fderivWithin 𝕜 f s x - fderivWithin 𝕜 g s x

Full source

theorem fderivWithin_sub (hxs : UniqueDiffWithinAt 𝕜 s x) (hf : DifferentiableWithinAt 𝕜 f s x)
    (hg : DifferentiableWithinAt 𝕜 g s x) :
    fderivWithin 𝕜 (fun y => f y - g y) s x = fderivWithin 𝕜 f s x - fderivWithin 𝕜 g s x :=
  (hf.hasFDerivWithinAt.sub hg.hasFDerivWithinAt).fderivWithin hxs

Fréchet Derivative of Difference Within a Set: $\text{fderivWithin}_{\mathbb{K}} (f - g) s x = \text{fderivWithin}_{\mathbb{K}} f s x - \text{fderivWithin}_{\mathbb{K}} g s x$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f, g : E \to F$ be functions differentiable at a point $x \in E$ within a subset $s \subseteq E$. If $s$ is uniquely differentiable at $x$, then the Fréchet derivative of the function $y \mapsto f(y) - g(y)$ at $x$ within $s$ is equal to the difference of the Fréchet derivatives of $f$ and $g$ at $x$ within $s$, i.e., $$ \text{fderivWithin}_{\mathbb{K}} (f - g) s x = \text{fderivWithin}_{\mathbb{K}} f s x - \text{fderivWithin}_{\mathbb{K}} g s x. $$

fderivWithin_sub' theorem

 (hxs : UniqueDiffWithinAt 𝕜 s x) (hf : DifferentiableWithinAt 𝕜 f s x) (hg : DifferentiableWithinAt 𝕜 g s x) :
  fderivWithin 𝕜 (f - g) s x = fderivWithin 𝕜 f s x - fderivWithin 𝕜 g s x

Full source

/-- Version of `fderivWithin_sub` where the function is written as `f - g` instead
of `fun y ↦ f y - g y`. -/
theorem fderivWithin_sub' (hxs : UniqueDiffWithinAt 𝕜 s x) (hf : DifferentiableWithinAt 𝕜 f s x)
    (hg : DifferentiableWithinAt 𝕜 g s x) :
    fderivWithin 𝕜 (f - g) s x = fderivWithin 𝕜 f s x - fderivWithin 𝕜 g s x :=
  fderivWithin_sub hxs hf hg

Fréchet Derivative of Function Difference Within a Set: $\text{fderivWithin}_{\mathbb{K}} (f - g) s x = \text{fderivWithin}_{\mathbb{K}} f s x - \text{fderivWithin}_{\mathbb{K}} g s x$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f, g : E \to F$ be functions differentiable at a point $x \in E$ within a subset $s \subseteq E$. If $s$ is uniquely differentiable at $x$, then the Fréchet derivative of $f - g$ at $x$ within $s$ is equal to the difference of the Fréchet derivatives of $f$ and $g$ at $x$ within $s$, i.e., $$ \text{fderivWithin}_{\mathbb{K}} (f - g) s x = \text{fderivWithin}_{\mathbb{K}} f s x - \text{fderivWithin}_{\mathbb{K}} g s x. $$

fderiv_sub theorem

 (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
  fderiv 𝕜 (fun y => f y - g y) x = fderiv 𝕜 f x - fderiv 𝕜 g x

Full source

theorem fderiv_sub (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
    fderiv 𝕜 (fun y => f y - g y) x = fderiv 𝕜 f x - fderiv 𝕜 g x :=
  (hf.hasFDerivAt.sub hg.hasFDerivAt).fderiv

Fréchet Derivative of Difference: $\text{fderiv}_{\mathbb{K}} (f - g) x = \text{fderiv}_{\mathbb{K}} f x - \text{fderiv}_{\mathbb{K}} g x$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$. If functions $f, g : E \to F$ are differentiable at a point $x \in E$, then the Fréchet derivative of the function $y \mapsto f(y) - g(y)$ at $x$ is equal to the difference of the Fréchet derivatives of $f$ and $g$ at $x$, i.e., $$ \text{fderiv}_{\mathbb{K}} (f - g) x = \text{fderiv}_{\mathbb{K}} f x - \text{fderiv}_{\mathbb{K}} g x. $$

fderiv_sub' theorem

 (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) : fderiv 𝕜 (f - g) x = fderiv 𝕜 f x - fderiv 𝕜 g x

Full source

/-- Version of `fderiv_sub` where the function is written as `f - g` instead
of `fun y ↦ f y - g y`. -/
theorem fderiv_sub' (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
    fderiv 𝕜 (f - g) x = fderiv 𝕜 f x - fderiv 𝕜 g x :=
  fderiv_sub hf hg

Fréchet Derivative of Function Difference: $\text{fderiv}_{\mathbb{K}} (f - g) x = \text{fderiv}_{\mathbb{K}} f x - \text{fderiv}_{\mathbb{K}} g x$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$. If functions $f, g : E \to F$ are differentiable at a point $x \in E$, then the Fréchet derivative of $f - g$ at $x$ is equal to the difference of the Fréchet derivatives of $f$ and $g$ at $x$, i.e., $$ \text{fderiv}_{\mathbb{K}} (f - g) x = \text{fderiv}_{\mathbb{K}} f x - \text{fderiv}_{\mathbb{K}} g x. $$

hasFDerivAtFilter_sub_const_iff theorem

(c : F) : HasFDerivAtFilter (f · - c) f' x L ↔ HasFDerivAtFilter f f' x L

Full source

@[simp]
theorem hasFDerivAtFilter_sub_const_iff (c : F) :
    HasFDerivAtFilterHasFDerivAtFilter (f · - c) f' x L ↔ HasFDerivAtFilter f f' x L := by
  simp only [sub_eq_add_neg, hasFDerivAtFilter_add_const_iff]

Fréchet Derivative Invariance under Subtraction of a Constant

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any constant $c \in F$, the function $f(\cdot - c)$ has Fréchet derivative $f'$ at $x$ along filter $L$ if and only if $f$ has Fréchet derivative $f'$ at $x$ along $L$.

hasStrictFDerivAt_sub_const_iff theorem

(c : F) : HasStrictFDerivAt (f · - c) f' x ↔ HasStrictFDerivAt f f' x

Full source

@[simp]
theorem hasStrictFDerivAt_sub_const_iff (c : F) :
    HasStrictFDerivAtHasStrictFDerivAt (f · - c) f' x ↔ HasStrictFDerivAt f f' x := by
  simp only [sub_eq_add_neg, hasStrictFDerivAt_add_const_iff]

Strict Fréchet Differentiability is Preserved Under Subtraction of a Constant

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any constant $c \in F$ and point $x \in E$, the function $f(\cdot - c)$ has strict Fréchet derivative $f'$ at $x$ if and only if $f$ has strict Fréchet derivative $f'$ at $x$.

hasFDerivWithinAt_sub_const_iff theorem

(c : F) : HasFDerivWithinAt (f · - c) f' s x ↔ HasFDerivWithinAt f f' s x

Full source

@[simp]
theorem hasFDerivWithinAt_sub_const_iff (c : F) :
    HasFDerivWithinAtHasFDerivWithinAt (f · - c) f' s x ↔ HasFDerivWithinAt f f' s x :=
  hasFDerivAtFilter_sub_const_iff c

Fréchet Derivative Invariance under Subtraction of a Constant within a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any constant $c \in F$, the function $f(\cdot - c)$ has Fréchet derivative $f'$ at $x$ within the set $s \subseteq E$ if and only if $f$ has Fréchet derivative $f'$ at $x$ within $s$.

hasFDerivAt_sub_const_iff theorem

(c : F) : HasFDerivAt (f · - c) f' x ↔ HasFDerivAt f f' x

Full source

@[simp]
theorem hasFDerivAt_sub_const_iff (c : F) : HasFDerivAtHasFDerivAt (f · - c) f' x ↔ HasFDerivAt f f' x :=
  hasFDerivAtFilter_sub_const_iff c

Fréchet Derivative Invariance under Subtraction of a Constant at a Point

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any constant $c \in F$ and point $x \in E$, the function $f(\cdot - c)$ has Fréchet derivative $f'$ at $x$ if and only if $f$ has Fréchet derivative $f'$ at $x$.

hasStrictFDerivAt_sub_const theorem

{x : F} (c : F) : HasStrictFDerivAt (· - c) (id 𝕜 F) x

Full source

@[fun_prop]
theorem hasStrictFDerivAt_sub_const {x : F} (c : F) : HasStrictFDerivAt (· - c) (id 𝕜 F) x :=
  (hasStrictFDerivAt_id x).sub_const c

Strict Fréchet Differentiability of Translation by a Constant

Informal description

Let $F$ be a normed space over a nontrivially normed field $\mathbb{K}$. For any constant $c \in F$ and any point $x \in F$, the function $y \mapsto y - c$ has the identity map $\mathrm{id}_{\mathbb{K}} F$ as its strict Fréchet derivative at $x$.

hasFDerivAt_sub_const theorem

{x : F} (c : F) : HasFDerivAt (· - c) (id 𝕜 F) x

Full source

@[fun_prop]
theorem hasFDerivAt_sub_const {x : F} (c : F) : HasFDerivAt (· - c) (id 𝕜 F) x :=
  (hasFDerivAt_id x).sub_const c

Fréchet Derivative of Translation by a Constant is the Identity Map

Informal description

Let $F$ be a normed space over a nontrivially normed field $\mathbb{K}$. For any point $x \in F$ and any constant $c \in F$, the function $f(y) = y - c$ has the identity map $\mathrm{id} : F \to F$ as its Fréchet derivative at $x$.

DifferentiableWithinAt.sub_const theorem

(hf : DifferentiableWithinAt 𝕜 f s x) (c : F) : DifferentiableWithinAt 𝕜 (fun y => f y - c) s x

Full source

@[fun_prop]
theorem DifferentiableWithinAt.sub_const (hf : DifferentiableWithinAt 𝕜 f s x) (c : F) :
    DifferentiableWithinAt 𝕜 (fun y => f y - c) s x :=
  (hf.hasFDerivWithinAt.sub_const c).differentiableWithinAt

Differentiability of Shifted Function Within a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, let $f : E \to F$ be a function differentiable at a point $x \in E$ within a subset $s \subseteq E$, and let $c \in F$ be a constant. Then the function $y \mapsto f(y) - c$ is differentiable at $x$ within $s$.

differentiableWithinAt_sub_const_iff theorem

(c : F) : DifferentiableWithinAt 𝕜 (fun y => f y - c) s x ↔ DifferentiableWithinAt 𝕜 f s x

Full source

@[simp]
theorem differentiableWithinAt_sub_const_iff (c : F) :
    DifferentiableWithinAtDifferentiableWithinAt 𝕜 (fun y => f y - c) s x ↔ DifferentiableWithinAt 𝕜 f s x := by
  simp only [sub_eq_add_neg, differentiableWithinAt_add_const_iff]

Differentiability of Shifted Function Within a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, let $f : E \to F$ be a function, and let $s \subseteq E$ be a subset. For any point $x \in E$ and any constant $c \in F$, the function $y \mapsto f(y) - c$ is differentiable at $x$ within $s$ if and only if $f$ is differentiable at $x$ within $s$.

DifferentiableAt.sub_const theorem

(hf : DifferentiableAt 𝕜 f x) (c : F) : DifferentiableAt 𝕜 (fun y => f y - c) x

Full source

@[fun_prop]
theorem DifferentiableAt.sub_const (hf : DifferentiableAt 𝕜 f x) (c : F) :
    DifferentiableAt 𝕜 (fun y => f y - c) x :=
  (hf.hasFDerivAt.sub_const c).differentiableAt

Differentiability of Shifted Function at a Point

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function differentiable at a point $x \in E$. Then for any constant $c \in F$, the function $y \mapsto f(y) - c$ is differentiable at $x$.

DifferentiableOn.sub_const theorem

(hf : DifferentiableOn 𝕜 f s) (c : F) : DifferentiableOn 𝕜 (fun y => f y - c) s

Full source

@[fun_prop]
theorem DifferentiableOn.sub_const (hf : DifferentiableOn 𝕜 f s) (c : F) :
    DifferentiableOn 𝕜 (fun y => f y - c) s := fun x hx => (hf x hx).sub_const c

Differentiability of Shifted Function on a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function differentiable on a subset $s \subseteq E$. Then for any constant $c \in F$, the function $y \mapsto f(y) - c$ is differentiable on $s$.

Differentiable.sub_const theorem

(hf : Differentiable 𝕜 f) (c : F) : Differentiable 𝕜 fun y => f y - c

Full source

@[fun_prop]
theorem Differentiable.sub_const (hf : Differentiable 𝕜 f) (c : F) :
    Differentiable 𝕜 fun y => f y - c := fun x => (hf x).sub_const c

Differentiability of Shifted Function

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, and let $E$ and $F$ be normed spaces over $\mathbb{K}$. If a function $f : E \to F$ is differentiable, then for any constant $c \in F$, the function $y \mapsto f(y) - c$ is also differentiable.

fderivWithin_sub_const theorem

(c : F) : fderivWithin 𝕜 (fun y => f y - c) s x = fderivWithin 𝕜 f s x

Full source

theorem fderivWithin_sub_const (c : F) :
    fderivWithin 𝕜 (fun y => f y - c) s x = fderivWithin 𝕜 f s x := by
  simp only [sub_eq_add_neg, fderivWithin_add_const]

Fréchet Derivative of Function Minus Constant Within Set Equals Derivative of Function

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, $f : E \to F$ be a function, $s \subseteq E$ be a subset, $x \in E$, and $c \in F$. Then the Fréchet derivative of the function $y \mapsto f(y) - c$ at $x$ within $s$ is equal to the Fréchet derivative of $f$ at $x$ within $s$, i.e., \[ \text{fderivWithin}_{\mathbb{K}} (\lambda y, f(y) - c) s x = \text{fderivWithin}_{\mathbb{K}} f s x. \]

fderiv_sub_const theorem

(c : F) : fderiv 𝕜 (fun y => f y - c) x = fderiv 𝕜 f x

Full source

theorem fderiv_sub_const (c : F) : fderiv 𝕜 (fun y => f y - c) x = fderiv 𝕜 f x := by
  simp only [sub_eq_add_neg, fderiv_add_const]

Fréchet Derivative of Function Minus Constant Equals Derivative of Function

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, $f : E \to F$ be a function, $x \in E$, and $c \in F$. Then the Fréchet derivative of the function $y \mapsto f(y) - c$ at $x$ is equal to the Fréchet derivative of $f$ at $x$, i.e., \[ \text{fderiv}_{\mathbb{K}} (\lambda y, f(y) - c) x = \text{fderiv}_{\mathbb{K}} f x. \]

HasFDerivAtFilter.const_sub theorem

(hf : HasFDerivAtFilter f f' x L) (c : F) : HasFDerivAtFilter (fun x => c - f x) (-f') x L

Full source

theorem HasFDerivAtFilter.const_sub (hf : HasFDerivAtFilter f f' x L) (c : F) :
    HasFDerivAtFilter (fun x => c - f x) (-f') x L := by
  simpa only [sub_eq_add_neg] using hf.neg.const_add c

Fréchet Derivative of Constant Minus Function is Negative Derivative

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $f : E \to F$ be a function with Fréchet derivative $f'$ at $x \in E$ along the filter $L$ on $E$. Then for any constant $c \in F$, the function $x \mapsto c - f(x)$ has Fréchet derivative $-f'$ at $x$ along $L$.

HasStrictFDerivAt.const_sub theorem

(hf : HasStrictFDerivAt f f' x) (c : F) : HasStrictFDerivAt (fun x => c - f x) (-f') x

Full source

@[fun_prop]
nonrec theorem HasStrictFDerivAt.const_sub (hf : HasStrictFDerivAt f f' x) (c : F) :
    HasStrictFDerivAt (fun x => c - f x) (-f') x := by
  simpa only [sub_eq_add_neg] using hf.neg.const_add c

Strict Fréchet Derivative of Constant Minus Function: $(c - f)' = -f'$ at $x$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ has a strict Fréchet derivative $f'$ at a point $x \in E$, then for any constant $c \in F$, the function $x \mapsto c - f(x)$ has $-f'$ as its strict Fréchet derivative at $x$.

HasFDerivWithinAt.const_sub theorem

(hf : HasFDerivWithinAt f f' s x) (c : F) : HasFDerivWithinAt (fun x => c - f x) (-f') s x

Full source

@[fun_prop]
nonrec theorem HasFDerivWithinAt.const_sub (hf : HasFDerivWithinAt f f' s x) (c : F) :
    HasFDerivWithinAt (fun x => c - f x) (-f') s x :=
  hf.const_sub c

Fréchet Derivative of Constant Minus Function within a Set: $(c - f)' = -f'$ at $x$ within $s$

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $f : E \to F$ be a function. If $f$ has a Fréchet derivative $f'$ at a point $x \in E$ within a set $s \subseteq E$, then for any constant $c \in F$, the function $x \mapsto c - f(x)$ has Fréchet derivative $-f'$ at $x$ within $s$.

HasFDerivAt.const_sub theorem

(hf : HasFDerivAt f f' x) (c : F) : HasFDerivAt (fun x => c - f x) (-f') x

Full source

@[fun_prop]
nonrec theorem HasFDerivAt.const_sub (hf : HasFDerivAt f f' x) (c : F) :
    HasFDerivAt (fun x => c - f x) (-f') x :=
  hf.const_sub c

Fréchet Derivative of Constant Minus Function: $(c - f)' = -f'$ at $x$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ has a Fréchet derivative $f'$ at a point $x \in E$, then for any constant $c \in F$, the function $x \mapsto c - f(x)$ has $-f'$ as its Fréchet derivative at $x$.

DifferentiableWithinAt.const_sub theorem

(hf : DifferentiableWithinAt 𝕜 f s x) (c : F) : DifferentiableWithinAt 𝕜 (fun y => c - f y) s x

Full source

@[fun_prop]
theorem DifferentiableWithinAt.const_sub (hf : DifferentiableWithinAt 𝕜 f s x) (c : F) :
    DifferentiableWithinAt 𝕜 (fun y => c - f y) s x :=
  (hf.hasFDerivWithinAt.const_sub c).differentiableWithinAt

Differentiability of Constant Minus Function within a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function differentiable at a point $x \in E$ within a subset $s \subseteq E$. Then for any constant $c \in F$, the function $y \mapsto c - f(y)$ is differentiable at $x$ within $s$.

differentiableWithinAt_const_sub_iff theorem

(c : F) : DifferentiableWithinAt 𝕜 (fun y => c - f y) s x ↔ DifferentiableWithinAt 𝕜 f s x

Full source

@[simp]
theorem differentiableWithinAt_const_sub_iff (c : F) :
    DifferentiableWithinAtDifferentiableWithinAt 𝕜 (fun y => c - f y) s x ↔ DifferentiableWithinAt 𝕜 f s x := by
  simp [sub_eq_add_neg]

Differentiability of Constant Minus Function ↔ Differentiability of Original Function

Informal description

For a function $f : E \to F$ between normed spaces $E$ and $F$ over a nontrivially normed field $\mathbb{K}$, a point $x \in E$, a subset $s \subseteq E$, and a constant $c \in F$, the function $y \mapsto c - f(y)$ is differentiable at $x$ within $s$ if and only if $f$ is differentiable at $x$ within $s$.

DifferentiableAt.const_sub theorem

(hf : DifferentiableAt 𝕜 f x) (c : F) : DifferentiableAt 𝕜 (fun y => c - f y) x

Full source

@[fun_prop]
theorem DifferentiableAt.const_sub (hf : DifferentiableAt 𝕜 f x) (c : F) :
    DifferentiableAt 𝕜 (fun y => c - f y) x :=
  (hf.hasFDerivAt.const_sub c).differentiableAt

Differentiability of Constant Minus Function at a Point

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function differentiable at a point $x \in E$. Then for any constant $c \in F$, the function $y \mapsto c - f(y)$ is differentiable at $x$.

DifferentiableOn.const_sub theorem

(hf : DifferentiableOn 𝕜 f s) (c : F) : DifferentiableOn 𝕜 (fun y => c - f y) s

Full source

@[fun_prop]
theorem DifferentiableOn.const_sub (hf : DifferentiableOn 𝕜 f s) (c : F) :
    DifferentiableOn 𝕜 (fun y => c - f y) s := fun x hx => (hf x hx).const_sub c

Differentiability of Constant Minus Function on a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function differentiable on a subset $s \subseteq E$. Then for any constant $c \in F$, the function $y \mapsto c - f(y)$ is differentiable on $s$.

Differentiable.const_sub theorem

(hf : Differentiable 𝕜 f) (c : F) : Differentiable 𝕜 fun y => c - f y

Full source

@[fun_prop]
theorem Differentiable.const_sub (hf : Differentiable 𝕜 f) (c : F) :
    Differentiable 𝕜 fun y => c - f y := fun x => (hf x).const_sub c

Differentiability of Constant Minus Differentiable Function

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a differentiable function. Then for any constant $c \in F$, the function $y \mapsto c - f(y)$ is differentiable on $E$.

fderivWithin_const_sub theorem

(hxs : UniqueDiffWithinAt 𝕜 s x) (c : F) : fderivWithin 𝕜 (fun y => c - f y) s x = -fderivWithin 𝕜 f s x

Full source

theorem fderivWithin_const_sub (hxs : UniqueDiffWithinAt 𝕜 s x) (c : F) :
    fderivWithin 𝕜 (fun y => c - f y) s x = -fderivWithin 𝕜 f s x := by
  simp only [sub_eq_add_neg, fderivWithin_const_add, fderivWithin_neg, hxs]

Fréchet Derivative of Constant Minus Function within a Set: $\text{fderivWithin}_{\mathbb{K}} (c - f) s x = -\text{fderivWithin}_{\mathbb{K}} f s x$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ be a function, $s \subseteq E$ be a subset, and $x \in E$ be a point where $s$ is uniquely differentiable. Then for any constant $c \in F$, the Fréchet derivative of the function $y \mapsto c - f(y)$ at $x$ within $s$ equals the negative of the Fréchet derivative of $f$ at $x$ within $s$, i.e., \[ \text{fderivWithin}_{\mathbb{K}} (\lambda y, c - f(y)) s x = -\text{fderivWithin}_{\mathbb{K}} f s x. \]

fderiv_const_sub theorem

(c : F) : fderiv 𝕜 (fun y => c - f y) x = -fderiv 𝕜 f x

Full source

theorem fderiv_const_sub (c : F) : fderiv 𝕜 (fun y => c - f y) x = -fderiv 𝕜 f x := by
  simp only [← fderivWithin_univ, fderivWithin_const_sub uniqueDiffWithinAt_univ]

Fréchet Derivative of Constant Minus Function: $\text{fderiv}_{\mathbb{K}} (c - f) x = -\text{fderiv}_{\mathbb{K}} f x$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function differentiable at $x \in E$. Then for any constant $c \in F$, the Fréchet derivative of the function $y \mapsto c - f(y)$ at $x$ equals the negative of the Fréchet derivative of $f$ at $x$, i.e., \[ \text{fderiv}_{\mathbb{K}} (\lambda y, c - f(y)) x = -\text{fderiv}_{\mathbb{K}} f x. \]

hasFDerivWithinAt_comp_add_left theorem

(a : E) : HasFDerivWithinAt (fun x ↦ f (a + x)) f' s x ↔ HasFDerivWithinAt f f' (a +ᵥ s) (a + x)

Full source

theorem hasFDerivWithinAt_comp_add_left (a : E) :
    HasFDerivWithinAtHasFDerivWithinAt (fun x ↦ f (a + x)) f' s x ↔ HasFDerivWithinAt f f' (a +ᵥ s) (a + x) := by
  have : map (a + ·) (𝓝[s] x) = 𝓝[a +ᵥ s] (a + x) := by
    simp only [add_comm x a, nhdsWithin, Filter.map_inf (add_right_injective a)]
    simp [← Set.image_vadd]
  simp [HasFDerivWithinAt, hasFDerivAtFilter_iff_isLittleOTVS, ← this, Function.comp_def]

Fréchet Derivative of Left-Translated Function within a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any point $a \in E$, the function $x \mapsto f(a + x)$ has Fréchet derivative $f'$ at a point $x$ within a set $s \subseteq E$ if and only if $f$ has Fréchet derivative $f'$ at the point $a + x$ within the translated set $a + s$.

differentiableWithinAt_comp_add_left theorem

(a : E) : DifferentiableWithinAt 𝕜 (fun x ↦ f (a + x)) s x ↔ DifferentiableWithinAt 𝕜 f (a +ᵥ s) (a + x)

Full source

theorem differentiableWithinAt_comp_add_left (a : E) :
    DifferentiableWithinAtDifferentiableWithinAt 𝕜 (fun x ↦ f (a + x)) s x ↔
      DifferentiableWithinAt 𝕜 f (a +ᵥ s) (a + x) := by
  simp [DifferentiableWithinAt, hasFDerivWithinAt_comp_add_left]

Differentiability of Left-Translated Function within a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any point $a \in E$, the function $x \mapsto f(a + x)$ is differentiable within a set $s \subseteq E$ at a point $x \in E$ if and only if $f$ is differentiable within the translated set $a + s$ at the point $a + x$.

fderivWithin_comp_add_left theorem

(a : E) : fderivWithin 𝕜 (fun x ↦ f (a + x)) s x = fderivWithin 𝕜 f (a +ᵥ s) (a + x)

Full source

theorem fderivWithin_comp_add_left (a : E) :
    fderivWithin 𝕜 (fun x ↦ f (a + x)) s x = fderivWithin 𝕜 f (a +ᵥ s) (a + x) := by
  classical
  simp only [fderivWithin, hasFDerivWithinAt_comp_add_left, differentiableWithinAt_comp_add_left]

Fréchet Derivative of Left-Translated Function within a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any point $a \in E$, the Fréchet derivative of the function $x \mapsto f(a + x)$ at a point $x$ within a set $s \subseteq E$ is equal to the Fréchet derivative of $f$ at the point $a + x$ within the translated set $a + s$.

hasFDerivWithinAt_comp_add_right theorem

(a : E) : HasFDerivWithinAt (fun x ↦ f (x + a)) f' s x ↔ HasFDerivWithinAt f f' (a +ᵥ s) (x + a)

Full source

theorem hasFDerivWithinAt_comp_add_right (a : E) :
    HasFDerivWithinAtHasFDerivWithinAt (fun x ↦ f (x + a)) f' s x ↔ HasFDerivWithinAt f f' (a +ᵥ s) (x + a) := by
  simpa only [add_comm a] using hasFDerivWithinAt_comp_add_left a

Fréchet Derivative of Right-Translated Function within a Set is Equivalent to Derivative at Translated Point

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any vector $a \in E$, the function $x \mapsto f(x + a)$ has Fréchet derivative $f'$ at a point $x$ within a set $s \subseteq E$ if and only if $f$ has Fréchet derivative $f'$ at the point $x + a$ within the translated set $a + s$.

differentiableWithinAt_comp_add_right theorem

(a : E) : DifferentiableWithinAt 𝕜 (fun x ↦ f (x + a)) s x ↔ DifferentiableWithinAt 𝕜 f (a +ᵥ s) (x + a)

Full source

theorem differentiableWithinAt_comp_add_right (a : E) :
    DifferentiableWithinAtDifferentiableWithinAt 𝕜 (fun x ↦ f (x + a)) s x ↔
      DifferentiableWithinAt 𝕜 f (a +ᵥ s) (x + a) := by
  simp [DifferentiableWithinAt, hasFDerivWithinAt_comp_add_right]

Differentiability of Function Composition with Right Translation within a Set

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any point $x \in E$, any vector $a \in E$, and any subset $s \subseteq E$, the function $x \mapsto f(x + a)$ is differentiable at $x$ within $s$ if and only if $f$ is differentiable at $x + a$ within the translated set $a + s$.

fderivWithin_comp_add_right theorem

(a : E) : fderivWithin 𝕜 (fun x ↦ f (x + a)) s x = fderivWithin 𝕜 f (a +ᵥ s) (x + a)

Full source

theorem fderivWithin_comp_add_right (a : E) :
    fderivWithin 𝕜 (fun x ↦ f (x + a)) s x = fderivWithin 𝕜 f (a +ᵥ s) (x + a) := by
  simp only [add_comm _ a, fderivWithin_comp_add_left]

Fréchet Derivative of Right-Translated Function within a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any vector $a \in E$, the Fréchet derivative of the function $x \mapsto f(x + a)$ at a point $x$ within a set $s \subseteq E$ is equal to the Fréchet derivative of $f$ at the point $x + a$ within the translated set $a + s$.

hasFDerivAt_comp_add_right theorem

(a : E) : HasFDerivAt (fun x ↦ f (x + a)) f' x ↔ HasFDerivAt f f' (x + a)

Full source

theorem hasFDerivAt_comp_add_right (a : E) :
    HasFDerivAtHasFDerivAt (fun x ↦ f (x + a)) f' x ↔ HasFDerivAt f f' (x + a) := by
  simp [← hasFDerivWithinAt_univ, hasFDerivWithinAt_comp_add_right]

Fréchet Derivative of Function Composition with Right Translation

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any point $x \in E$ and any vector $a \in E$, the function $x \mapsto f(x + a)$ has Fréchet derivative $f'$ at $x$ if and only if $f$ has Fréchet derivative $f'$ at $x + a$.

differentiableAt_comp_add_right theorem

(a : E) : DifferentiableAt 𝕜 (fun x ↦ f (x + a)) x ↔ DifferentiableAt 𝕜 f (x + a)

Full source

theorem differentiableAt_comp_add_right (a : E) :
    DifferentiableAtDifferentiableAt 𝕜 (fun x ↦ f (x + a)) x ↔ DifferentiableAt 𝕜 f (x + a) := by
  simp [DifferentiableAt, hasFDerivAt_comp_add_right]

Differentiability of Function Composition with Right Translation

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any point $x \in E$ and any vector $a \in E$, the function $x \mapsto f(x + a)$ is differentiable at $x$ if and only if $f$ is differentiable at $x + a$.

fderiv_comp_add_right theorem

(a : E) : fderiv 𝕜 (fun x ↦ f (x + a)) x = fderiv 𝕜 f (x + a)

Full source

theorem fderiv_comp_add_right (a : E) :
    fderiv 𝕜 (fun x ↦ f (x + a)) x = fderiv 𝕜 f (x + a) := by
  simp [← fderivWithin_univ, fderivWithin_comp_add_right]

Fréchet Derivative of Right-Translated Function: $\text{fderiv}_{\mathbb{K}} (f \circ (+a)) x = \text{fderiv}_{\mathbb{K}} f (x + a)$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any point $x \in E$ and any vector $a \in E$, the Fréchet derivative of the function $x \mapsto f(x + a)$ at $x$ is equal to the Fréchet derivative of $f$ at $x + a$.

hasFDerivAt_comp_add_left theorem

(a : E) : HasFDerivAt (fun x ↦ f (a + x)) f' x ↔ HasFDerivAt f f' (a + x)

Full source

theorem hasFDerivAt_comp_add_left (a : E) :
    HasFDerivAtHasFDerivAt (fun x ↦ f (a + x)) f' x ↔ HasFDerivAt f f' (a + x) := by
  simpa [add_comm a] using hasFDerivAt_comp_add_right a

Fréchet Derivative of Function Composition with Left Translation

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any point $x \in E$ and any vector $a \in E$, the function $x \mapsto f(a + x)$ has Fréchet derivative $f'$ at $x$ if and only if $f$ has Fréchet derivative $f'$ at $a + x$.

differentiableAt_comp_add_left theorem

(a : E) : DifferentiableAt 𝕜 (fun x ↦ f (a + x)) x ↔ DifferentiableAt 𝕜 f (a + x)

Full source

theorem differentiableAt_comp_add_left (a : E) :
    DifferentiableAtDifferentiableAt 𝕜 (fun x ↦ f (a + x)) x ↔ DifferentiableAt 𝕜 f (a + x) := by
  simp [DifferentiableAt, hasFDerivAt_comp_add_left]

Differentiability of Left Translation of a Function

Informal description

Let $E$ be a normed space over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function to another normed space $F$. For any point $x \in E$ and any vector $a \in E$, the function $x \mapsto f(a + x)$ is differentiable at $x$ if and only if $f$ is differentiable at $a + x$.

fderiv_comp_add_left theorem

(a : E) : fderiv 𝕜 (fun x ↦ f (a + x)) x = fderiv 𝕜 f (a + x)

Full source

theorem fderiv_comp_add_left (a : E) :
    fderiv 𝕜 (fun x ↦ f (a + x)) x = fderiv 𝕜 f (a + x) := by
  simpa [add_comm a] using fderiv_comp_add_right a

Fréchet Derivative of Left-Translated Function: $\text{fderiv}_{\mathbb{K}} (f \circ (a + \cdot)) x = \text{fderiv}_{\mathbb{K}} f (a + x)$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any point $x \in E$ and any vector $a \in E$, the Fréchet derivative of the function $x \mapsto f(a + x)$ at $x$ is equal to the Fréchet derivative of $f$ at $a + x$.

hasFDerivWithinAt_comp_sub theorem

(a : E) : HasFDerivWithinAt (fun x ↦ f (x - a)) f' s x ↔ HasFDerivWithinAt f f' (-a +ᵥ s) (x - a)

Full source

theorem hasFDerivWithinAt_comp_sub (a : E) :
    HasFDerivWithinAtHasFDerivWithinAt (fun x ↦ f (x - a)) f' s x ↔ HasFDerivWithinAt f f' (-a +ᵥ s) (x - a) := by
  simpa [sub_eq_add_neg] using hasFDerivWithinAt_comp_add_right (-a)

Fréchet Derivative of Translated Function: $f(x-a)$ has derivative $f'$ at $x$ within $s$ iff $f$ has derivative $f'$ at $x-a$ within $-a + s$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any vector $a \in E$, the function $x \mapsto f(x - a)$ has Fréchet derivative $f'$ at a point $x$ within a set $s \subseteq E$ if and only if $f$ has Fréchet derivative $f'$ at the point $x - a$ within the translated set $-a + s$.

differentiableWithinAt_comp_sub theorem

(a : E) : DifferentiableWithinAt 𝕜 (fun x ↦ f (x - a)) s x ↔ DifferentiableWithinAt 𝕜 f (-a +ᵥ s) (x - a)

Full source

theorem differentiableWithinAt_comp_sub (a : E) :
    DifferentiableWithinAtDifferentiableWithinAt 𝕜 (fun x ↦ f (x - a)) s x ↔
      DifferentiableWithinAt 𝕜 f (-a +ᵥ s) (x - a) := by
  simp [DifferentiableWithinAt, hasFDerivWithinAt_comp_sub]

Differentiability of Translated Function within a Set: $f(x-a)$ differentiable at $x$ within $s$ iff $f$ differentiable at $x-a$ within $-a + s$

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any $a \in E$, the function $x \mapsto f(x - a)$ is differentiable at $x$ within the set $s$ if and only if $f$ is differentiable at $x - a$ within the translated set $-a + s$.

fderivWithin_comp_sub theorem

(a : E) : fderivWithin 𝕜 (fun x ↦ f (x - a)) s x = fderivWithin 𝕜 f (-a +ᵥ s) (x - a)

Full source

theorem fderivWithin_comp_sub (a : E) :
    fderivWithin 𝕜 (fun x ↦ f (x - a)) s x = fderivWithin 𝕜 f (-a +ᵥ s) (x - a) := by
  simpa [sub_eq_add_neg] using fderivWithin_comp_add_right (-a)

Fréchet Derivative of Left-Translated Function within a Set: $\text{fderivWithin}_{\mathbb{K}} (x \mapsto f(x-a)) s x = \text{fderivWithin}_{\mathbb{K}} f (-a + s) (x-a)$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any vector $a \in E$, the Fréchet derivative of the function $x \mapsto f(x - a)$ at a point $x$ within a set $s \subseteq E$ is equal to the Fréchet derivative of $f$ at the point $x - a$ within the translated set $-a + s$.

hasFDerivAt_comp_sub theorem

(a : E) : HasFDerivAt (fun x ↦ f (x - a)) f' x ↔ HasFDerivAt f f' (x - a)

Full source

theorem hasFDerivAt_comp_sub (a : E) :
    HasFDerivAtHasFDerivAt (fun x ↦ f (x - a)) f' x ↔ HasFDerivAt f f' (x - a) := by
  simp [← hasFDerivWithinAt_univ, hasFDerivWithinAt_comp_sub]

Fréchet Derivative of Translated Function: $f(x-a)$ has derivative $f'$ at $x$ iff $f$ has derivative $f'$ at $x-a$

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any $a \in E$, the function $x \mapsto f(x - a)$ has Fréchet derivative $f'$ at $x$ if and only if $f$ has Fréchet derivative $f'$ at $x - a$.

differentiableAt_comp_sub theorem

(a : E) : DifferentiableAt 𝕜 (fun x ↦ f (x - a)) x ↔ DifferentiableAt 𝕜 f (x - a)

Full source

theorem differentiableAt_comp_sub (a : E) :
    DifferentiableAtDifferentiableAt 𝕜 (fun x ↦ f (x - a)) x ↔ DifferentiableAt 𝕜 f (x - a) := by
  simp [DifferentiableAt, hasFDerivAt_comp_sub]

Differentiability of Translated Function: $f(x-a)$ at $x$ iff $f$ at $x-a$

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any $a \in E$, the translated function $x \mapsto f(x - a)$ is differentiable at $x$ if and only if $f$ is differentiable at $x - a$.

fderiv_comp_sub theorem

(a : E) : fderiv 𝕜 (fun x ↦ f (x - a)) x = fderiv 𝕜 f (x - a)

Full source

theorem fderiv_comp_sub (a : E) :
    fderiv 𝕜 (fun x ↦ f (x - a)) x = fderiv 𝕜 f (x - a) := by
  simp [← fderivWithin_univ, fderivWithin_comp_sub]

Fréchet Derivative of Translated Function: $\text{fderiv}_{\mathbb{K}} (x \mapsto f(x - a)) (x) = \text{fderiv}_{\mathbb{K}} f (x - a)$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any vector $a \in E$, the Fréchet derivative of the translated function $x \mapsto f(x - a)$ at a point $x \in E$ is equal to the Fréchet derivative of $f$ at the point $x - a$. In other words, $$ \text{fderiv}_{\mathbb{K}} (x \mapsto f(x - a)) (x) = \text{fderiv}_{\mathbb{K}} f (x - a). $$