Mathlib.Analysis.Calculus.FDeriv.Mul

HasStrictFDerivAt.clm_comp theorem

 (hc : HasStrictFDerivAt c c' x) (hd : HasStrictFDerivAt d d' x) :
  HasStrictFDerivAt (fun y => (c y).comp (d y)) ((compL 𝕜 F G H (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c') x

Full source

@[fun_prop]
theorem HasStrictFDerivAt.clm_comp (hc : HasStrictFDerivAt c c' x) (hd : HasStrictFDerivAt d d' x) :
    HasStrictFDerivAt (fun y => (c y).comp (d y))
      ((compL 𝕜 F G H (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c') x := by
  have := isBoundedBilinearMap_comp.hasStrictFDerivAt (c x, d x)
  have := this.comp x (hc.prodMk hd)
  exact this

Strict Fréchet Differentiability of Composition of Continuous Linear Maps

Informal description

Let $E$, $F$, $G$, and $H$ be normed spaces over a field $\mathbb{K}$, and let $c : E \to F \to_{\mathcal{L}} G$ and $d : E \to F \to_{\mathcal{L}} H$ be functions. Suppose $c$ has strict Fréchet derivative $c'$ at $x \in E$ and $d$ has strict Fréchet derivative $d'$ at $x$. Then the function $y \mapsto c(y) \circ d(y)$ has strict Fréchet derivative at $x$ given by: $$(\text{compL}_{\mathbb{K}}(F,G,H)(c(x))) \circ d' + (\text{compL}_{\mathbb{K}}(F,G,H).\text{flip}(d(x))) \circ c'$$ where $\text{compL}_{\mathbb{K}}(F,G,H)$ is the bounded bilinear map of composition of continuous linear maps.

HasFDerivWithinAt.clm_comp theorem

 (hc : HasFDerivWithinAt c c' s x) (hd : HasFDerivWithinAt d d' s x) :
  HasFDerivWithinAt (fun y => (c y).comp (d y)) ((compL 𝕜 F G H (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c') s
    x

Full source

@[fun_prop]
theorem HasFDerivWithinAt.clm_comp (hc : HasFDerivWithinAt c c' s x)
    (hd : HasFDerivWithinAt d d' s x) :
    HasFDerivWithinAt (fun y => (c y).comp (d y))
      ((compL 𝕜 F G H (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c') s x := by
  exact (isBoundedBilinearMap_comp.hasFDerivAt (c x, d x) :).comp_hasFDerivWithinAt x (hc.prodMk hd)

Differentiability of Composition of Differentiable Continuous Linear Maps Within a Set

Informal description

Let $E$, $F$, $G$, and $H$ be normed spaces over a field $\mathbb{K}$, and let $s$ be a subset of $E$. Suppose: 1. $c : E \to (F \to_{\mathcal{L}} G)$ is differentiable within $s$ at $x \in E$ with derivative $c'$ 2. $d : E \to (E \to_{\mathcal{L}} F)$ is differentiable within $s$ at $x$ with derivative $d'$ Then the function $y \mapsto c(y) \circ d(y)$ is differentiable within $s$ at $x$, and its derivative is the continuous linear map: \[ (\text{compL}_{\mathbb{K}}(F,G,H)(c(x))) \circ d' + (\text{compL}_{\mathbb{K}}(F,G,H)^{\text{flip}}(d(x))) \circ c' \] where $\text{compL}_{\mathbb{K}}(F,G,H)$ is the bounded bilinear map of composition of continuous linear maps, and $\text{flip}$ denotes the reversed argument order.

HasFDerivAt.clm_comp theorem

 (hc : HasFDerivAt c c' x) (hd : HasFDerivAt d d' x) :
  HasFDerivAt (fun y => (c y).comp (d y)) ((compL 𝕜 F G H (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c') x

Full source

@[fun_prop]
theorem HasFDerivAt.clm_comp (hc : HasFDerivAt c c' x) (hd : HasFDerivAt d d' x) :
    HasFDerivAt (fun y => (c y).comp (d y))
      ((compL 𝕜 F G H (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c') x := by
  exact (isBoundedBilinearMap_comp.hasFDerivAt (c x, d x) :).comp x <| hc.prodMk hd

Derivative of Composition of Differentiable Continuous Linear Maps

Informal description

Let $E$, $F$, $G$, and $H$ be normed spaces over a field $\mathbb{K}$. Suppose $c : E \to (F \to_{\mathcal{L}} G)$ and $d : E \to (G \to_{\mathcal{L}} H)$ are differentiable at $x \in E$ with Fréchet derivatives $c'$ and $d'$ respectively. Then the function $y \mapsto c(y) \circ d(y)$ is differentiable at $x$ with derivative given by the composition of the derivative of $c$ with $d(x)$ plus the composition of the derivative of $d$ with $c(x)$, i.e., \[ (f \circ g)'(x) = (f'(x) \circ g(x)) + (g'(x) \circ f(x)). \]

DifferentiableWithinAt.clm_comp theorem

 (hc : DifferentiableWithinAt 𝕜 c s x) (hd : DifferentiableWithinAt 𝕜 d s x) :
  DifferentiableWithinAt 𝕜 (fun y => (c y).comp (d y)) s x

Full source

@[fun_prop]
theorem DifferentiableWithinAt.clm_comp (hc : DifferentiableWithinAt 𝕜 c s x)
    (hd : DifferentiableWithinAt 𝕜 d s x) :
    DifferentiableWithinAt 𝕜 (fun y => (c y).comp (d y)) s x :=
  (hc.hasFDerivWithinAt.clm_comp hd.hasFDerivWithinAt).differentiableWithinAt

Differentiability of composition of differentiable continuous linear maps within a set

Informal description

Let $E$, $F$, and $G$ be normed spaces over a field $\mathbb{K}$, and let $s \subseteq E$ be a subset. If two functions $c : E \to (F \to_{\mathcal{L}} G)$ and $d : E \to (E \to_{\mathcal{L}} F)$ are differentiable at a point $x \in E$ within $s$, then the function $y \mapsto c(y) \circ d(y)$ is also differentiable at $x$ within $s$.

DifferentiableAt.clm_comp theorem

(hc : DifferentiableAt 𝕜 c x) (hd : DifferentiableAt 𝕜 d x) : DifferentiableAt 𝕜 (fun y => (c y).comp (d y)) x

Full source

@[fun_prop]
theorem DifferentiableAt.clm_comp (hc : DifferentiableAt 𝕜 c x) (hd : DifferentiableAt 𝕜 d x) :
    DifferentiableAt 𝕜 (fun y => (c y).comp (d y)) x :=
  (hc.hasFDerivAt.clm_comp hd.hasFDerivAt).differentiableAt

Differentiability of Composition of Differentiable Continuous Linear Maps at a Point

Informal description

Let $E$, $F$, $G$, and $H$ be normed spaces over a field $\mathbb{K}$. If $c : E \to (F \to_{\mathcal{L}} G)$ and $d : E \to (G \to_{\mathcal{L}} H)$ are differentiable at $x \in E$, then the function $y \mapsto c(y) \circ d(y)$ is differentiable at $x$.

DifferentiableOn.clm_comp theorem

(hc : DifferentiableOn 𝕜 c s) (hd : DifferentiableOn 𝕜 d s) : DifferentiableOn 𝕜 (fun y => (c y).comp (d y)) s

Full source

@[fun_prop]
theorem DifferentiableOn.clm_comp (hc : DifferentiableOn 𝕜 c s) (hd : DifferentiableOn 𝕜 d s) :
    DifferentiableOn 𝕜 (fun y => (c y).comp (d y)) s := fun x hx => (hc x hx).clm_comp (hd x hx)

Differentiability of Composition of Continuous Linear Maps on a Set

Informal description

Let $E$, $F$, and $G$ be normed spaces over a field $\mathbb{K}$, and let $s \subseteq E$ be a subset. If two functions $c : E \to (F \to_{\mathcal{L}} G)$ and $d : E \to (E \to_{\mathcal{L}} F)$ are differentiable on $s$, then the function $y \mapsto c(y) \circ d(y)$ is also differentiable on $s$.

Differentiable.clm_comp theorem

(hc : Differentiable 𝕜 c) (hd : Differentiable 𝕜 d) : Differentiable 𝕜 fun y => (c y).comp (d y)

Full source

@[fun_prop]
theorem Differentiable.clm_comp (hc : Differentiable 𝕜 c) (hd : Differentiable 𝕜 d) :
    Differentiable 𝕜 fun y => (c y).comp (d y) := fun x => (hc x).clm_comp (hd x)

Differentiability of Composition of Differentiable Continuous Linear Maps

Informal description

Let $E$, $F$, $G$, and $H$ be normed spaces over a field $\mathbb{K}$. If $c : E \to (F \to_{\mathcal{L}} G)$ and $d : E \to (G \to_{\mathcal{L}} H)$ are differentiable functions, then the function $y \mapsto c(y) \circ d(y)$ is differentiable.

fderivWithin_clm_comp theorem

 (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x) (hd : DifferentiableWithinAt 𝕜 d s x) :
  fderivWithin 𝕜 (fun y => (c y).comp (d y)) s x =
    (compL 𝕜 F G H (c x)).comp (fderivWithin 𝕜 d s x) + ((compL 𝕜 F G H).flip (d x)).comp (fderivWithin 𝕜 c s x)

Full source

theorem fderivWithin_clm_comp (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x)
    (hd : DifferentiableWithinAt 𝕜 d s x) :
    fderivWithin 𝕜 (fun y => (c y).comp (d y)) s x =
      (compL 𝕜 F G H (c x)).comp (fderivWithin 𝕜 d s x) +
        ((compL 𝕜 F G H).flip (d x)).comp (fderivWithin 𝕜 c s x) :=
  (hc.hasFDerivWithinAt.clm_comp hd.hasFDerivWithinAt).fderivWithin hxs

Derivative of Composition of Differentiable Continuous Linear Maps Within a Set

Informal description

Let $E$, $F$, $G$, and $H$ be normed spaces over a field $\mathbb{K}$, and let $s \subseteq E$ be a subset that is uniquely differentiable at a point $x \in s$. Suppose: 1. $c : E \to (F \to_{\mathcal{L}} G)$ is differentiable at $x$ within $s$ 2. $d : E \to (E \to_{\mathcal{L}} F)$ is differentiable at $x$ within $s$ Then the Fréchet derivative of the function $y \mapsto c(y) \circ d(y)$ at $x$ within $s$ is given by: \[ (\text{compL}_{\mathbb{K}}(F,G,H)(c(x))) \circ f'(x) + (\text{compL}_{\mathbb{K}}(F,G,H)^{\text{flip}}(d(x))) \circ g'(x) \] where $f'(x)$ and $g'(x)$ are the Fréchet derivatives of $d$ and $c$ at $x$ within $s$ respectively, and $\text{compL}_{\mathbb{K}}(F,G,H)$ is the bounded bilinear map of composition of continuous linear maps.

fderiv_clm_comp theorem

 (hc : DifferentiableAt 𝕜 c x) (hd : DifferentiableAt 𝕜 d x) :
  fderiv 𝕜 (fun y => (c y).comp (d y)) x =
    (compL 𝕜 F G H (c x)).comp (fderiv 𝕜 d x) + ((compL 𝕜 F G H).flip (d x)).comp (fderiv 𝕜 c x)

Full source

theorem fderiv_clm_comp (hc : DifferentiableAt 𝕜 c x) (hd : DifferentiableAt 𝕜 d x) :
    fderiv 𝕜 (fun y => (c y).comp (d y)) x =
      (compL 𝕜 F G H (c x)).comp (fderiv 𝕜 d x) +
        ((compL 𝕜 F G H).flip (d x)).comp (fderiv 𝕜 c x) :=
  (hc.hasFDerivAt.clm_comp hd.hasFDerivAt).fderiv

Derivative of Composition of Differentiable Continuous Linear Maps: $fderiv_{\mathbb{K}}(c \circ d)(x) = (compL_{\mathbb{K}}(c(x)) \circ fderiv_{\mathbb{K}} d(x)) + (flip(compL_{\mathbb{K}})(d(x)) \circ fderiv_{\mathbb{K}} c(x))$

Informal description

Let $E$, $F$, $G$, and $H$ be normed spaces over a field $\mathbb{K}$. Suppose $c : E \to (F \to_{\mathcal{L}} G)$ and $d : E \to (G \to_{\mathcal{L}} H)$ are differentiable at a point $x \in E$. Then the Fréchet derivative of the function $y \mapsto c(y) \circ d(y)$ at $x$ is given by: \[ (\text{compL}_{\mathbb{K}}(F,G,H)(c(x))) \circ f'(x) + (\text{compL}_{\mathbb{K}}(F,G,H)^{\text{flip}}(d(x))) \circ g'(x) \] where $f'(x)$ and $g'(x)$ are the Fréchet derivatives of $d$ and $c$ at $x$ respectively, and $\text{compL}_{\mathbb{K}}(F,G,H)$ is the bounded bilinear map of composition of continuous linear maps.

HasStrictFDerivAt.clm_apply theorem

 (hc : HasStrictFDerivAt c c' x) (hu : HasStrictFDerivAt u u' x) :
  HasStrictFDerivAt (fun y => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) x

Full source

@[fun_prop]
theorem HasStrictFDerivAt.clm_apply (hc : HasStrictFDerivAt c c' x)
    (hu : HasStrictFDerivAt u u' x) :
    HasStrictFDerivAt (fun y => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) x :=
  (isBoundedBilinearMap_apply.hasStrictFDerivAt (c x, u x)).comp x (hc.prodMk hu)

Strict Fréchet Differentiability of the Application of a Differentiable Operator to a Differentiable Function

Informal description

Let $E$, $F$, and $G$ be normed spaces over a field $\mathbb{K}$. Suppose $c \colon E \to F \to_{\mathcal{L}} G$ and $u \colon E \to F$ are functions that are strictly Fréchet differentiable at a point $x \in E$, with derivatives $c' \colon E \to_{\mathcal{L}} (F \to_{\mathcal{L}} G)$ and $u' \colon E \to_{\mathcal{L}} F$, respectively. Then the function $y \mapsto c(y)(u(y))$ is strictly Fréchet differentiable at $x$, and its derivative is given by $(c(x)) \circ u' + c'^{\text{flip}}(u(x))$.

HasFDerivWithinAt.clm_apply theorem

 (hc : HasFDerivWithinAt c c' s x) (hu : HasFDerivWithinAt u u' s x) :
  HasFDerivWithinAt (fun y => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) s x

Full source

@[fun_prop]
theorem HasFDerivWithinAt.clm_apply (hc : HasFDerivWithinAt c c' s x)
    (hu : HasFDerivWithinAt u u' s x) :
    HasFDerivWithinAt (fun y => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) s x := by
  exact (isBoundedBilinearMap_apply.hasFDerivAt (c x, u x) :).comp_hasFDerivWithinAt x
    (hc.prodMk hu)

Differentiability of Continuous Linear Map Application Within a Set

Informal description

Let $E$, $F$, and $G$ be normed spaces over a field $\mathbb{K}$. Suppose $c : E \to (F \to_{\mathcal{L}} G)$ and $u : E \to F$ are functions differentiable within a set $s \subseteq E$ at a point $x \in s$, with derivatives $c'$ and $u'$ respectively. Then the function $y \mapsto c(y)(u(y))$ is differentiable within $s$ at $x$, and its derivative is given by the continuous linear map: \[ (c(x)) \circ u' + c'^{\text{flip}}(u(x)) \] where $\circ$ denotes composition of continuous linear maps and $c'^{\text{flip}}$ is the flipped version of $c'$.

HasFDerivAt.clm_apply theorem

 (hc : HasFDerivAt c c' x) (hu : HasFDerivAt u u' x) :
  HasFDerivAt (fun y => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) x

Full source

@[fun_prop]
theorem HasFDerivAt.clm_apply (hc : HasFDerivAt c c' x) (hu : HasFDerivAt u u' x) :
    HasFDerivAt (fun y => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) x := by
  exact (isBoundedBilinearMap_apply.hasFDerivAt (c x, u x) :).comp x (hc.prodMk hu)

Differentiability of the Application of Differentiable Operator-Valued Functions

Informal description

Let $E$, $F$, and $G$ be normed spaces over a field $\mathbb{K}$, and let $x \in E$. Suppose $c : E \to F \toL[\mathbb{K}] G$ and $u : E \to F$ are functions that are Fréchet differentiable at $x$, with derivatives $c' : E \toL[\mathbb{K}] (F \toL[\mathbb{K}] G)$ and $u' : E \toL[\mathbb{K}] F$ respectively. Then the function $y \mapsto c(y)(u(y))$ is Fréchet differentiable at $x$, and its derivative is given by the continuous linear map \[ (c(x)) \circ u' + c'^{\text{flip}}(u(x)), \] where $c'^{\text{flip}}$ denotes the flipped version of $c'$ (i.e., $c'^{\text{flip}}(v)(w) = c'(w)(v)$ for $v \in F$ and $w \in E$).

DifferentiableWithinAt.clm_apply theorem

 (hc : DifferentiableWithinAt 𝕜 c s x) (hu : DifferentiableWithinAt 𝕜 u s x) :
  DifferentiableWithinAt 𝕜 (fun y => (c y) (u y)) s x

Full source

@[fun_prop]
theorem DifferentiableWithinAt.clm_apply (hc : DifferentiableWithinAt 𝕜 c s x)
    (hu : DifferentiableWithinAt 𝕜 u s x) : DifferentiableWithinAt 𝕜 (fun y => (c y) (u y)) s x :=
  (hc.hasFDerivWithinAt.clm_apply hu.hasFDerivWithinAt).differentiableWithinAt

Differentiability of Operator Application Within a Set

Informal description

Let $E$, $F$, and $G$ be normed spaces over a field $\mathbb{K}$, and let $s \subseteq E$ be a subset. If $c : E \to (F \to_{\mathcal{L}} G)$ and $u : E \to F$ are functions that are differentiable at a point $x \in s$ within $s$, then the function $y \mapsto c(y)(u(y))$ is differentiable at $x$ within $s$.

DifferentiableAt.clm_apply theorem

(hc : DifferentiableAt 𝕜 c x) (hu : DifferentiableAt 𝕜 u x) : DifferentiableAt 𝕜 (fun y => (c y) (u y)) x

Full source

@[fun_prop]
theorem DifferentiableAt.clm_apply (hc : DifferentiableAt 𝕜 c x) (hu : DifferentiableAt 𝕜 u x) :
    DifferentiableAt 𝕜 (fun y => (c y) (u y)) x :=
  (hc.hasFDerivAt.clm_apply hu.hasFDerivAt).differentiableAt

Differentiability of operator application at a point

Informal description

Let $E$, $F$, and $G$ be normed spaces over a field $\mathbb{K}$, and let $x \in E$. If $c : E \to F \toL[\mathbb{K}] G$ and $u : E \to F$ are differentiable at $x$, then the function $y \mapsto c(y)(u(y))$ is differentiable at $x$.

DifferentiableOn.clm_apply theorem

(hc : DifferentiableOn 𝕜 c s) (hu : DifferentiableOn 𝕜 u s) : DifferentiableOn 𝕜 (fun y => (c y) (u y)) s

Full source

@[fun_prop]
theorem DifferentiableOn.clm_apply (hc : DifferentiableOn 𝕜 c s) (hu : DifferentiableOn 𝕜 u s) :
    DifferentiableOn 𝕜 (fun y => (c y) (u y)) s := fun x hx => (hc x hx).clm_apply (hu x hx)

Differentiability of Operator Application on a Set

Informal description

Let $E$, $F$, and $G$ be normed spaces over a field $\mathbb{K}$, and let $s \subseteq E$ be a subset. If $c : E \to (F \to_{\mathcal{L}} G)$ and $u : E \to F$ are differentiable on $s$, then the function $y \mapsto c(y)(u(y))$ is differentiable on $s$.

Differentiable.clm_apply theorem

(hc : Differentiable 𝕜 c) (hu : Differentiable 𝕜 u) : Differentiable 𝕜 fun y => (c y) (u y)

Full source

@[fun_prop]
theorem Differentiable.clm_apply (hc : Differentiable 𝕜 c) (hu : Differentiable 𝕜 u) :
    Differentiable 𝕜 fun y => (c y) (u y) := fun x => (hc x).clm_apply (hu x)

Differentiability of Operator Application

Informal description

Let $E$, $F$, and $G$ be normed spaces over a field $\mathbb{K}$. If $c : E \to F \toL[\mathbb{K}] G$ and $u : E \to F$ are differentiable functions, then the function $y \mapsto c(y)(u(y))$ is differentiable on $E$.

fderivWithin_clm_apply theorem

 (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x) (hu : DifferentiableWithinAt 𝕜 u s x) :
  fderivWithin 𝕜 (fun y => (c y) (u y)) s x = (c x).comp (fderivWithin 𝕜 u s x) + (fderivWithin 𝕜 c s x).flip (u x)

Full source

theorem fderivWithin_clm_apply (hxs : UniqueDiffWithinAt 𝕜 s x)
    (hc : DifferentiableWithinAt 𝕜 c s x) (hu : DifferentiableWithinAt 𝕜 u s x) :
    fderivWithin 𝕜 (fun y => (c y) (u y)) s x =
      (c x).comp (fderivWithin 𝕜 u s x) + (fderivWithin 𝕜 c s x).flip (u x) :=
  (hc.hasFDerivWithinAt.clm_apply hu.hasFDerivWithinAt).fderivWithin hxs

Fréchet Derivative of Operator Application Within a Set

Informal description

Let $E$, $F$, and $G$ be normed spaces over a field $\mathbb{K}$, and let $s \subseteq E$ be a subset that is uniquely differentiable at $x \in s$. If $c : E \to (F \to_{\mathcal{L}} G)$ and $u : E \to F$ are differentiable at $x$ within $s$, then the Fréchet derivative of the function $y \mapsto c(y)(u(y))$ at $x$ within $s$ is given by: \[ (c(x)) \circ \text{fderivWithin}_{\mathbb{K}} u s x + (\text{fderivWithin}_{\mathbb{K}} c s x)^{\text{flip}}(u(x)) \] where $\circ$ denotes composition of continuous linear maps and $(\cdot)^{\text{flip}}$ denotes the flipped derivative.

fderiv_clm_apply theorem

 (hc : DifferentiableAt 𝕜 c x) (hu : DifferentiableAt 𝕜 u x) :
  fderiv 𝕜 (fun y => (c y) (u y)) x = (c x).comp (fderiv 𝕜 u x) + (fderiv 𝕜 c x).flip (u x)

Full source

theorem fderiv_clm_apply (hc : DifferentiableAt 𝕜 c x) (hu : DifferentiableAt 𝕜 u x) :
    fderiv 𝕜 (fun y => (c y) (u y)) x = (c x).comp (fderiv 𝕜 u x) + (fderiv 𝕜 c x).flip (u x) :=
  (hc.hasFDerivAt.clm_apply hu.hasFDerivAt).fderiv

Fréchet Derivative of Operator Application: $\text{fderiv}(c(u))(x) = c(x) \circ \text{fderiv} u x + (\text{fderiv} c x)^{\text{flip}}(u(x))$

Informal description

Let $E$, $F$, and $G$ be normed spaces over a field $\mathbb{K}$. Given functions $c : E \to F \to_{\mathcal{L}} G$ and $u : E \to F$ that are differentiable at a point $x \in E$, the Fréchet derivative of the function $y \mapsto c(y)(u(y))$ at $x$ is given by: \[ \text{fderiv}_{\mathbb{K}} (y \mapsto c(y)(u(y))) x = (c(x)) \circ \text{fderiv}_{\mathbb{K}} u x + (\text{fderiv}_{\mathbb{K}} c x)^{\text{flip}}(u(x)) \] where $\circ$ denotes composition of continuous linear maps and $(\cdot)^{\text{flip}}$ denotes the flipped derivative.

HasStrictFDerivAt.continuousMultilinear_apply_const theorem

(hc : HasStrictFDerivAt c c' x) (u : ∀ i, M i) : HasStrictFDerivAt (fun y ↦ (c y) u) (c'.flipMultilinear u) x

Full source

@[fun_prop]
theorem HasStrictFDerivAt.continuousMultilinear_apply_const (hc : HasStrictFDerivAt c c' x)
    (u : ∀ i, M i) : HasStrictFDerivAt (fun y ↦ (c y) u) (c'.flipMultilinear u) x :=
  (ContinuousMultilinearMap.apply 𝕜 M H u).hasStrictFDerivAt.comp x hc

Strict Differentiability of Multilinear Map Application at a Fixed Point

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $M$ be a family of normed spaces indexed by $\iota$. Suppose $c : E \to \text{ContinuousMultilinearMap}_{\mathbb{K}}(M, F)$ is a function that has strict Fréchet derivative $c' : E \toL[\mathbb{K}] \text{ContinuousMultilinearMap}_{\mathbb{K}}(M, F)$ at a point $x \in E$. Then for any fixed tuple $u = (u_i)_{i \in \iota}$ where each $u_i \in M_i$, the function $y \mapsto c(y)(u)$ has strict Fréchet derivative at $x$ given by $c'(x).\text{flipMultilinear}(u)$.

HasFDerivWithinAt.continuousMultilinear_apply_const theorem

(hc : HasFDerivWithinAt c c' s x) (u : ∀ i, M i) : HasFDerivWithinAt (fun y ↦ (c y) u) (c'.flipMultilinear u) s x

Full source

@[fun_prop]
theorem HasFDerivWithinAt.continuousMultilinear_apply_const (hc : HasFDerivWithinAt c c' s x)
    (u : ∀ i, M i) :
    HasFDerivWithinAt (fun y ↦ (c y) u) (c'.flipMultilinear u) s x :=
  (ContinuousMultilinearMap.apply 𝕜 M H u).hasFDerivAt.comp_hasFDerivWithinAt x hc

Differentiability of Continuous Multilinear Map Application to Constant Vectors

Informal description

Let $E$ be a normed space over a field $\mathbb{K}$, $M$ be a family of normed spaces indexed by $\iota$, and $F$ be another normed space. Let $c : E \to \text{ContinuousMultilinearMap}_{\mathbb{K}} M F$ be a function that is differentiable at a point $x \in E$ within a set $s \subseteq E$, with derivative $c' : E \toL[\mathbb{K}] \text{ContinuousMultilinearMap}_{\mathbb{K}} M F$. Then for any fixed tuple of vectors $u = (u_i)_{i \in \iota}$ in $\prod_{i} M_i$, the function $y \mapsto c(y)(u)$ is differentiable at $x$ within $s$, with derivative equal to the evaluation of the flipped multilinear map $c'.flipMultilinear(u)$.

HasFDerivAt.continuousMultilinear_apply_const theorem

(hc : HasFDerivAt c c' x) (u : ∀ i, M i) : HasFDerivAt (fun y ↦ (c y) u) (c'.flipMultilinear u) x

Full source

@[fun_prop]
theorem HasFDerivAt.continuousMultilinear_apply_const (hc : HasFDerivAt c c' x) (u : ∀ i, M i) :
    HasFDerivAt (fun y ↦ (c y) u) (c'.flipMultilinear u) x :=
  (ContinuousMultilinearMap.apply 𝕜 M H u).hasFDerivAt.comp x hc

Differentiability of the evaluation of a differentiable continuous multilinear map at a fixed point

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $M_i$ be a family of normed spaces indexed by $i$. Suppose $c : E \to \text{ContinuousMultilinearMap}_{\mathbb{K}} M F$ is a function that is Fréchet differentiable at a point $x \in E$ with derivative $c' : E \toL[\mathbb{K}] \text{ContinuousMultilinearMap}_{\mathbb{K}} M F$. Then for any fixed tuple $u = (u_i)_{i}$ in $\prod_i M_i$, the function $y \mapsto c(y)(u)$ is Fréchet differentiable at $x$ with derivative $c'(x)(u, \cdot) : E \to F$.

DifferentiableWithinAt.continuousMultilinear_apply_const theorem

(hc : DifferentiableWithinAt 𝕜 c s x) (u : ∀ i, M i) : DifferentiableWithinAt 𝕜 (fun y ↦ (c y) u) s x

Full source

@[fun_prop]
theorem DifferentiableWithinAt.continuousMultilinear_apply_const
    (hc : DifferentiableWithinAt 𝕜 c s x) (u : ∀ i, M i) :
    DifferentiableWithinAt 𝕜 (fun y ↦ (c y) u) s x :=
  (hc.hasFDerivWithinAt.continuousMultilinear_apply_const u).differentiableWithinAt

Differentiability of Continuous Multilinear Map Evaluation Within a Set

Informal description

Let $E$ be a normed space over a field $\mathbb{K}$, $M$ be a family of normed spaces indexed by $\iota$, and $F$ be another normed space. Let $c : E \to \text{ContinuousMultilinearMap}_{\mathbb{K}} M F$ be a function that is differentiable at a point $x \in E$ within a set $s \subseteq E$. Then for any fixed tuple of vectors $u = (u_i)_{i \in \iota}$ in $\prod_{i} M_i$, the function $y \mapsto c(y)(u)$ is differentiable at $x$ within $s$.

DifferentiableAt.continuousMultilinear_apply_const theorem

(hc : DifferentiableAt 𝕜 c x) (u : ∀ i, M i) : DifferentiableAt 𝕜 (fun y ↦ (c y) u) x

Full source

@[fun_prop]
theorem DifferentiableAt.continuousMultilinear_apply_const (hc : DifferentiableAt 𝕜 c x)
    (u : ∀ i, M i) :
    DifferentiableAt 𝕜 (fun y ↦ (c y) u) x :=
  (hc.hasFDerivAt.continuousMultilinear_apply_const u).differentiableAt

Differentiability of evaluation of differentiable continuous multilinear maps at fixed points

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $(M_i)_{i}$ be a family of normed spaces. If a function $c : E \to \text{ContinuousMultilinearMap}_{\mathbb{K}} (M_i)_i F$ is differentiable at a point $x \in E$, then for any fixed tuple $u = (u_i)_i \in \prod_i M_i$, the function $y \mapsto c(y)(u)$ is differentiable at $x$.

DifferentiableOn.continuousMultilinear_apply_const theorem

(hc : DifferentiableOn 𝕜 c s) (u : ∀ i, M i) : DifferentiableOn 𝕜 (fun y ↦ (c y) u) s

Full source

@[fun_prop]
theorem DifferentiableOn.continuousMultilinear_apply_const (hc : DifferentiableOn 𝕜 c s)
    (u : ∀ i, M i) : DifferentiableOn 𝕜 (fun y ↦ (c y) u) s :=
  fun x hx ↦ (hc x hx).continuousMultilinear_apply_const u

Differentiability of Continuous Multilinear Map Evaluation on a Set

Informal description

Let $E$ be a normed space over a field $\mathbb{K}$, $M$ be a family of normed spaces indexed by $\iota$, and $F$ be another normed space. If a function $c : E \to \text{ContinuousMultilinearMap}_{\mathbb{K}} M F$ is differentiable on a set $s \subseteq E$, then for any fixed tuple of vectors $u = (u_i)_{i \in \iota}$ in $\prod_{i} M_i$, the function $y \mapsto c(y)(u)$ is differentiable on $s$.

Differentiable.continuousMultilinear_apply_const theorem

(hc : Differentiable 𝕜 c) (u : ∀ i, M i) : Differentiable 𝕜 fun y ↦ (c y) u

Full source

@[fun_prop]
theorem Differentiable.continuousMultilinear_apply_const (hc : Differentiable 𝕜 c) (u : ∀ i, M i) :
    Differentiable 𝕜 fun y ↦ (c y) u := fun x ↦ (hc x).continuousMultilinear_apply_const u

Differentiability of evaluation of differentiable continuous multilinear maps at fixed points (global version)

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $(M_i)_{i}$ be a family of normed spaces. If a function $c : E \to \text{ContinuousMultilinearMap}_{\mathbb{K}} (M_i)_i F$ is differentiable on $E$, then for any fixed tuple $u = (u_i)_i \in \prod_i M_i$, the function $y \mapsto c(y)(u)$ is differentiable on $E$.

fderivWithin_continuousMultilinear_apply_const theorem

 (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x) (u : ∀ i, M i) :
  fderivWithin 𝕜 (fun y ↦ (c y) u) s x = ((fderivWithin 𝕜 c s x).flipMultilinear u)

Full source

theorem fderivWithin_continuousMultilinear_apply_const (hxs : UniqueDiffWithinAt 𝕜 s x)
    (hc : DifferentiableWithinAt 𝕜 c s x) (u : ∀ i, M i) :
    fderivWithin 𝕜 (fun y ↦ (c y) u) s x = ((fderivWithin 𝕜 c s x).flipMultilinear u) :=
  (hc.hasFDerivWithinAt.continuousMultilinear_apply_const u).fderivWithin hxs

Derivative of Continuous Multilinear Map Evaluation Within a Set

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $(M_i)_i$ be a family of normed spaces. For a function $c : E \to \text{ContinuousMultilinearMap}_{\mathbb{K}} (M_i)_i F$ that is differentiable at a point $x \in E$ within a set $s \subseteq E$, where $s$ is uniquely differentiable at $x$, and for any fixed tuple of vectors $u = (u_i)_i \in \prod_i M_i$, the Fréchet derivative of the function $y \mapsto c(y)(u)$ at $x$ within $s$ is equal to the evaluation of the flipped multilinear map of the derivative of $c$ at $x$ within $s$ applied to $u$. In symbols: $$ \text{fderivWithin}_{\mathbb{K}} (\lambda y, c(y)(u)) s x = (\text{fderivWithin}_{\mathbb{K}} c s x).\text{flipMultilinear}(u) $$

fderiv_continuousMultilinear_apply_const theorem

 (hc : DifferentiableAt 𝕜 c x) (u : ∀ i, M i) : (fderiv 𝕜 (fun y ↦ (c y) u) x) = (fderiv 𝕜 c x).flipMultilinear u

Full source

theorem fderiv_continuousMultilinear_apply_const (hc : DifferentiableAt 𝕜 c x) (u : ∀ i, M i) :
    (fderiv 𝕜 (fun y ↦ (c y) u) x) = (fderiv 𝕜 c x).flipMultilinear u :=
  (hc.hasFDerivAt.continuousMultilinear_apply_const u).fderiv

Derivative of Continuous Multilinear Map Evaluation at a Point

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $(M_i)_{i}$ be a family of normed spaces. If a function $c : E \to \text{ContinuousMultilinearMap}_{\mathbb{K}} (M_i)_i F$ is differentiable at a point $x \in E$, then for any fixed tuple $u = (u_i)_i \in \prod_i M_i$, the Fréchet derivative of the function $y \mapsto c(y)(u)$ at $x$ is equal to the evaluation of the flipped multilinear map of the derivative of $c$ at $x$ applied to $u$. In symbols: $$ \text{fderiv}_{\mathbb{K}} (\lambda y, c(y)(u)) x = (\text{fderiv}_{\mathbb{K}} c x).\text{flipMultilinear}(u) $$

fderivWithin_continuousMultilinear_apply_const_apply theorem

 (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x) (u : ∀ i, M i) (m : E) :
  (fderivWithin 𝕜 (fun y ↦ (c y) u) s x) m = (fderivWithin 𝕜 c s x) m u

Full source

/-- Application of a `ContinuousMultilinearMap` to a constant commutes with `fderivWithin`. -/
theorem fderivWithin_continuousMultilinear_apply_const_apply (hxs : UniqueDiffWithinAt 𝕜 s x)
    (hc : DifferentiableWithinAt 𝕜 c s x) (u : ∀ i, M i) (m : E) :
    (fderivWithin 𝕜 (fun y ↦ (c y) u) s x) m = (fderivWithin 𝕜 c s x) m u := by
  simp [fderivWithin_continuousMultilinear_apply_const hxs hc]

Evaluation of Derivative of Continuous Multilinear Map Application Within a Set

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $(M_i)_i$ be a family of normed spaces. For a function $c : E \to \text{ContinuousMultilinearMap}_{\mathbb{K}} (M_i)_i F$ that is differentiable at a point $x \in E$ within a set $s \subseteq E$, where $s$ is uniquely differentiable at $x$, and for any fixed tuple of vectors $u = (u_i)_i \in \prod_i M_i$ and any vector $m \in E$, the evaluation of the Fréchet derivative of the function $y \mapsto c(y)(u)$ at $x$ within $s$ applied to $m$ is equal to the evaluation of the derivative of $c$ at $x$ within $s$ applied to $m$ and $u$. In symbols: $$ \text{fderivWithin}_{\mathbb{K}} (\lambda y, c(y)(u)) s x (m) = \text{fderivWithin}_{\mathbb{K}} c s x (m)(u) $$

fderiv_continuousMultilinear_apply_const_apply theorem

 (hc : DifferentiableAt 𝕜 c x) (u : ∀ i, M i) (m : E) : (fderiv 𝕜 (fun y ↦ (c y) u) x) m = (fderiv 𝕜 c x) m u

Full source

/-- Application of a `ContinuousMultilinearMap` to a constant commutes with `fderiv`. -/
theorem fderiv_continuousMultilinear_apply_const_apply (hc : DifferentiableAt 𝕜 c x)
    (u : ∀ i, M i) (m : E) :
    (fderiv 𝕜 (fun y ↦ (c y) u) x) m = (fderiv 𝕜 c x) m u := by
  simp [fderiv_continuousMultilinear_apply_const hc]

Evaluation of Derivative of Continuous Multilinear Map Application at a Point

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $(M_i)_i$ be a family of normed spaces. If a function $c : E \to \text{ContinuousMultilinearMap}_{\mathbb{K}} (M_i)_i F$ is differentiable at a point $x \in E$, then for any fixed tuple of vectors $u = (u_i)_i \in \prod_i M_i$ and any vector $m \in E$, the evaluation of the Fréchet derivative of the function $y \mapsto c(y)(u)$ at $x$ applied to $m$ is equal to the evaluation of the derivative of $c$ at $x$ applied to $m$ and $u$. In symbols: $$ \text{fderiv}_{\mathbb{K}} (\lambda y, c(y)(u)) x (m) = \text{fderiv}_{\mathbb{K}} c x (m)(u) $$

HasStrictFDerivAt.smul theorem

 (hc : HasStrictFDerivAt c c' x) (hf : HasStrictFDerivAt f f' x) :
  HasStrictFDerivAt (fun y => c y • f y) (c x • f' + c'.smulRight (f x)) x

Full source

@[fun_prop]
theorem HasStrictFDerivAt.smul (hc : HasStrictFDerivAt c c' x) (hf : HasStrictFDerivAt f f' x) :
    HasStrictFDerivAt (fun y => c y • f y) (c x • f' + c'.smulRight (f x)) x :=
  (isBoundedBilinearMap_smul.hasStrictFDerivAt (c x, f x)).comp x <| hc.prodMk hf

Strict Fréchet Derivative of Scalar Multiplication of Functions

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$. Suppose $c : E \to \mathbb{K}$ and $f : E \to F$ are functions that are strictly Fréchet differentiable at a point $x \in E$, with derivatives $c' : E \to \mathbb{K}$ and $f' : E \to F$ respectively. Then the function $y \mapsto c(y) \cdot f(y)$ is strictly Fréchet differentiable at $x$, and its derivative is given by the continuous linear map $h \mapsto c(x) \cdot f'(h) + c'(h) \cdot f(x)$.

HasFDerivWithinAt.smul theorem

 (hc : HasFDerivWithinAt c c' s x) (hf : HasFDerivWithinAt f f' s x) :
  HasFDerivWithinAt (fun y => c y • f y) (c x • f' + c'.smulRight (f x)) s x

Full source

@[fun_prop]
theorem HasFDerivWithinAt.smul (hc : HasFDerivWithinAt c c' s x) (hf : HasFDerivWithinAt f f' s x) :
    HasFDerivWithinAt (fun y => c y • f y) (c x • f' + c'.smulRight (f x)) s x := by
  exact (isBoundedBilinearMap_smul.hasFDerivAt (𝕜 := 𝕜) (c x, f x) :).comp_hasFDerivWithinAt x <|
    hc.prodMk hf

Product rule for Fréchet derivatives of scalar-vector multiplication within a set

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $s \subseteq E$ be a subset. Suppose $c : E \to \mathbb{K}$ and $f : E \to F$ are functions differentiable at $x \in s$ within $s$, with Fréchet derivatives $c'$ and $f'$ at $x$ within $s$ respectively. Then the function $y \mapsto c(y) \cdot f(y)$ is differentiable at $x$ within $s$, and its Fréchet derivative is given by $c(x) \cdot f' + c'(\cdot) \cdot f(x)$.

HasFDerivAt.smul theorem

 (hc : HasFDerivAt c c' x) (hf : HasFDerivAt f f' x) :
  HasFDerivAt (fun y => c y • f y) (c x • f' + c'.smulRight (f x)) x

Full source

@[fun_prop]
theorem HasFDerivAt.smul (hc : HasFDerivAt c c' x) (hf : HasFDerivAt f f' x) :
    HasFDerivAt (fun y => c y • f y) (c x • f' + c'.smulRight (f x)) x := by
  exact (isBoundedBilinearMap_smul.hasFDerivAt (𝕜 := 𝕜) (c x, f x) :).comp x <| hc.prodMk hf

Product Rule for Scalar Multiplication of Differentiable Functions

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, and let $E$ and $F$ be normed spaces over $\mathbb{K}$. Suppose $c : E \to \mathbb{K}$ and $f : E \to F$ are differentiable at $x \in E$ with Fréchet derivatives $c' : E \to \mathbb{K}$ and $f' : E \to F$ respectively. Then the function $y \mapsto c(y) \cdot f(y)$ is differentiable at $x$ with Fréchet derivative given by $c(x) \cdot f' + c' \cdot f(x)$, where $c' \cdot f(x)$ denotes the linear map $v \mapsto c'(v) \cdot f(x)$.

DifferentiableWithinAt.smul theorem

 (hc : DifferentiableWithinAt 𝕜 c s x) (hf : DifferentiableWithinAt 𝕜 f s x) :
  DifferentiableWithinAt 𝕜 (fun y => c y • f y) s x

Full source

@[fun_prop]
theorem DifferentiableWithinAt.smul (hc : DifferentiableWithinAt 𝕜 c s x)
    (hf : DifferentiableWithinAt 𝕜 f s x) : DifferentiableWithinAt 𝕜 (fun y => c y • f y) s x :=
  (hc.hasFDerivWithinAt.smul hf.hasFDerivWithinAt).differentiableWithinAt

Differentiability of Scalar-Vector Product Within a Set

Informal description

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

DifferentiableAt.smul theorem

(hc : DifferentiableAt 𝕜 c x) (hf : DifferentiableAt 𝕜 f x) : DifferentiableAt 𝕜 (fun y => c y • f y) x

Full source

@[simp, fun_prop]
theorem DifferentiableAt.smul (hc : DifferentiableAt 𝕜 c x) (hf : DifferentiableAt 𝕜 f x) :
    DifferentiableAt 𝕜 (fun y => c y • f y) x :=
  (hc.hasFDerivAt.smul hf.hasFDerivAt).differentiableAt

Differentiability of Scalar Multiplication of Differentiable Functions at a Point

Informal description

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

DifferentiableOn.smul theorem

(hc : DifferentiableOn 𝕜 c s) (hf : DifferentiableOn 𝕜 f s) : DifferentiableOn 𝕜 (fun y => c y • f y) s

Full source

@[fun_prop]
theorem DifferentiableOn.smul (hc : DifferentiableOn 𝕜 c s) (hf : DifferentiableOn 𝕜 f s) :
    DifferentiableOn 𝕜 (fun y => c y • f y) s := fun x hx => (hc x hx).smul (hf x hx)

Differentiability of Scalar-Vector Product on a Set

Informal description

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

Differentiable.smul theorem

(hc : Differentiable 𝕜 c) (hf : Differentiable 𝕜 f) : Differentiable 𝕜 fun y => c y • f y

Full source

@[simp, fun_prop]
theorem Differentiable.smul (hc : Differentiable 𝕜 c) (hf : Differentiable 𝕜 f) :
    Differentiable 𝕜 fun y => c y • f y := fun x => (hc x).smul (hf x)

Differentiability of Scalar Multiplication of Differentiable Functions

Informal description

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

fderivWithin_smul theorem

 (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x) (hf : DifferentiableWithinAt 𝕜 f s x) :
  fderivWithin 𝕜 (fun y => c y • f y) s x = c x • fderivWithin 𝕜 f s x + (fderivWithin 𝕜 c s x).smulRight (f x)

Full source

theorem fderivWithin_smul (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x)
    (hf : DifferentiableWithinAt 𝕜 f s x) :
    fderivWithin 𝕜 (fun y => c y • f y) s x =
      c x • fderivWithin 𝕜 f s x + (fderivWithin 𝕜 c s x).smulRight (f x) :=
  (hc.hasFDerivWithinAt.smul hf.hasFDerivWithinAt).fderivWithin hxs

Product Rule for Fréchet Derivatives of Scalar-Vector Multiplication within a Set

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ normed spaces over $\mathbb{K}$, and $s \subseteq E$ a subset. Suppose $x \in s$ is a point where $s$ is uniquely differentiable (i.e., the tangent cone at $x$ spans a dense subspace of $E$). If $c : E \to \mathbb{K}$ and $f : E \to F$ are differentiable at $x$ within $s$, then the Fréchet derivative of the function $y \mapsto c(y) \cdot f(y)$ at $x$ within $s$ is given by: \[ c(x) \cdot f'(x) + c'(x)(\cdot) \cdot f(x) \] where $f'(x)$ is the Fréchet derivative of $f$ at $x$ within $s$, and $c'(x)(\cdot) \cdot f(x)$ denotes the continuous linear map obtained by scalar multiplying $f(x)$ with the derivative $c'(x)$.

fderiv_smul theorem

 (hc : DifferentiableAt 𝕜 c x) (hf : DifferentiableAt 𝕜 f x) :
  fderiv 𝕜 (fun y => c y • f y) x = c x • fderiv 𝕜 f x + (fderiv 𝕜 c x).smulRight (f x)

Full source

theorem fderiv_smul (hc : DifferentiableAt 𝕜 c x) (hf : DifferentiableAt 𝕜 f x) :
    fderiv 𝕜 (fun y => c y • f y) x = c x • fderiv 𝕜 f x + (fderiv 𝕜 c x).smulRight (f x) :=
  (hc.hasFDerivAt.smul hf.hasFDerivAt).fderiv

Product Rule for Fréchet Derivatives of Scalar-Vector Multiplication

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, and let $E$ and $F$ be normed spaces over $\mathbb{K}$. Suppose $c : E \to \mathbb{K}$ and $f : E \to F$ are differentiable at a point $x \in E$. Then the Fréchet derivative of the function $y \mapsto c(y) \cdot f(y)$ at $x$ is given by: \[ c(x) \cdot f'(x) + c'(x)(\cdot) \cdot f(x) \] where $f'(x)$ is the Fréchet derivative of $f$ at $x$, and $c'(x)(\cdot) \cdot f(x)$ denotes the continuous linear map obtained by scalar multiplying $f(x)$ with the derivative $c'(x)$.

HasStrictFDerivAt.smul_const theorem

(hc : HasStrictFDerivAt c c' x) (f : F) : HasStrictFDerivAt (fun y => c y • f) (c'.smulRight f) x

Full source

@[fun_prop]
theorem HasStrictFDerivAt.smul_const (hc : HasStrictFDerivAt c c' x) (f : F) :
    HasStrictFDerivAt (fun y => c y • f) (c'.smulRight f) x := by
  simpa only [smul_zero, zero_add] using hc.smul (hasStrictFDerivAt_const f x)

Strict Fréchet derivative of scalar multiplication by a constant vector

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$. Suppose $c : E \to \mathbb{K}$ is a function that is strictly Fréchet differentiable at a point $x \in E$ with derivative $c' : E \to \mathbb{K}$, and let $f \in F$ be a fixed vector. Then the function $y \mapsto c(y) \cdot f$ is strictly Fréchet differentiable at $x$, and its derivative is the continuous linear map $h \mapsto c'(h) \cdot f$.

HasFDerivWithinAt.smul_const theorem

(hc : HasFDerivWithinAt c c' s x) (f : F) : HasFDerivWithinAt (fun y => c y • f) (c'.smulRight f) s x

Full source

@[fun_prop]
theorem HasFDerivWithinAt.smul_const (hc : HasFDerivWithinAt c c' s x) (f : F) :
    HasFDerivWithinAt (fun y => c y • f) (c'.smulRight f) s x := by
  simpa only [smul_zero, zero_add] using hc.smul (hasFDerivWithinAt_const f x s)

Differentiability of scalar multiplication with a constant vector within a set

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $s \subseteq E$ be a subset. Suppose $c : E \to \mathbb{K}$ is differentiable at $x \in s$ within $s$ with Fréchet derivative $c'$ at $x$ within $s$, and let $f \in F$ be a constant vector. Then the function $y \mapsto c(y) \cdot f$ is differentiable at $x$ within $s$, and its Fréchet derivative is given by $c'(\cdot) \cdot f$.

HasFDerivAt.smul_const theorem

(hc : HasFDerivAt c c' x) (f : F) : HasFDerivAt (fun y => c y • f) (c'.smulRight f) x

Full source

@[fun_prop]
theorem HasFDerivAt.smul_const (hc : HasFDerivAt c c' x) (f : F) :
    HasFDerivAt (fun y => c y • f) (c'.smulRight f) x := by
  simpa only [smul_zero, zero_add] using hc.smul (hasFDerivAt_const f x)

Differentiability of scalar multiplication with a constant vector

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$. If a function $c : E \to \mathbb{K}$ is Fréchet differentiable at $x \in E$ with derivative $c' : E \to \mathbb{K}$, then for any fixed vector $f \in F$, the function $y \mapsto c(y) \cdot f$ is Fréchet differentiable at $x$ with derivative $h \mapsto c'(h) \cdot f$.

DifferentiableWithinAt.smul_const theorem

(hc : DifferentiableWithinAt 𝕜 c s x) (f : F) : DifferentiableWithinAt 𝕜 (fun y => c y • f) s x

Full source

@[fun_prop]
theorem DifferentiableWithinAt.smul_const (hc : DifferentiableWithinAt 𝕜 c s x) (f : F) :
    DifferentiableWithinAt 𝕜 (fun y => c y • f) s x :=
  (hc.hasFDerivWithinAt.smul_const f).differentiableWithinAt

Differentiability of scalar multiplication with a constant vector within a set

Informal description

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

DifferentiableAt.smul_const theorem

(hc : DifferentiableAt 𝕜 c x) (f : F) : DifferentiableAt 𝕜 (fun y => c y • f) x

Full source

@[fun_prop]
theorem DifferentiableAt.smul_const (hc : DifferentiableAt 𝕜 c x) (f : F) :
    DifferentiableAt 𝕜 (fun y => c y • f) x :=
  (hc.hasFDerivAt.smul_const f).differentiableAt

Differentiability of scalar multiplication with a constant vector at a point

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$. If a function $c : E \to \mathbb{K}$ is differentiable at a point $x \in E$, then for any fixed vector $f \in F$, the function $y \mapsto c(y) \cdot f$ is differentiable at $x$.

DifferentiableOn.smul_const theorem

(hc : DifferentiableOn 𝕜 c s) (f : F) : DifferentiableOn 𝕜 (fun y => c y • f) s

Full source

@[fun_prop]
theorem DifferentiableOn.smul_const (hc : DifferentiableOn 𝕜 c s) (f : F) :
    DifferentiableOn 𝕜 (fun y => c y • f) s := fun x hx => (hc x hx).smul_const f

Differentiability of Scalar Multiplication with a Constant Vector on a Set

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset. If a function $c : E \to \mathbb{K}$ is differentiable on $s$, then for any fixed vector $f \in F$, the function $y \mapsto c(y) \cdot f$ is differentiable on $s$.

Differentiable.smul_const theorem

(hc : Differentiable 𝕜 c) (f : F) : Differentiable 𝕜 fun y => c y • f

Full source

@[fun_prop]
theorem Differentiable.smul_const (hc : Differentiable 𝕜 c) (f : F) :
    Differentiable 𝕜 fun y => c y • f := fun x => (hc x).smul_const f

Differentiability of scalar multiplication with a constant vector

Informal description

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

fderivWithin_smul_const theorem

 (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x) (f : F) :
  fderivWithin 𝕜 (fun y => c y • f) s x = (fderivWithin 𝕜 c s x).smulRight f

Full source

theorem fderivWithin_smul_const (hxs : UniqueDiffWithinAt 𝕜 s x)
    (hc : DifferentiableWithinAt 𝕜 c s x) (f : F) :
    fderivWithin 𝕜 (fun y => c y • f) s x = (fderivWithin 𝕜 c s x).smulRight f :=
  (hc.hasFDerivWithinAt.smul_const f).fderivWithin hxs

Fréchet derivative of scalar multiplication with a constant vector within a set

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset that is uniquely differentiable at a point $x \in s$. If a function $c : E \to \mathbb{K}$ is differentiable at $x$ within $s$, then for any fixed vector $f \in F$, the Fréchet derivative of the function $y \mapsto c(y) \cdot f$ at $x$ within $s$ is given by the continuous linear map $(\text{fderivWithin}_{\mathbb{K}} c s x)(\cdot) \cdot f$.

fderiv_smul_const theorem

(hc : DifferentiableAt 𝕜 c x) (f : F) : fderiv 𝕜 (fun y => c y • f) x = (fderiv 𝕜 c x).smulRight f

Full source

theorem fderiv_smul_const (hc : DifferentiableAt 𝕜 c x) (f : F) :
    fderiv 𝕜 (fun y => c y • f) x = (fderiv 𝕜 c x).smulRight f :=
  (hc.hasFDerivAt.smul_const f).fderiv

Fréchet Derivative of Scalar Multiplication with a Constant Vector

Informal description

Let $E$ and $F$ be normed spaces over a non-discrete normed field $\mathbb{K}$, and let $c : E \to \mathbb{K}$ be a function differentiable at a point $x \in E$. For any fixed vector $f \in F$, the Fréchet derivative of the function $y \mapsto c(y) \cdot f$ at $x$ is given by the continuous linear map $(\text{fderiv}_{\mathbb{K}} c x)(\cdot) \cdot f$.

HasStrictFDerivAt.mul' theorem

 {x : E} (ha : HasStrictFDerivAt a a' x) (hb : HasStrictFDerivAt b b' x) :
  HasStrictFDerivAt (fun y => a y * b y) (a x • b' + a'.smulRight (b x)) x

Full source

@[fun_prop]
theorem HasStrictFDerivAt.mul' {x : E} (ha : HasStrictFDerivAt a a' x)
    (hb : HasStrictFDerivAt b b' x) :
    HasStrictFDerivAt (fun y => a y * b y) (a x • b' + a'.smulRight (b x)) x :=
  ((ContinuousLinearMap.mul 𝕜 𝔸).isBoundedBilinearMap.hasStrictFDerivAt (a x, b x)).comp x
    (ha.prodMk hb)

Strict Differentiability of Product of Functions at a Point

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $a, b : E \to F$ be functions differentiable at a point $x \in E$ with strict Fréchet derivatives $a'$ and $b'$ respectively. Then the product function $y \mapsto a(y) \cdot b(y)$ is strictly differentiable at $x$, and its strict Fréchet derivative is given by $a(x) \cdot b' + a' \cdot b(x)$, where $a' \cdot b(x)$ denotes the linear map obtained by applying $a'$ to $b(x)$.

HasStrictFDerivAt.mul theorem

 (hc : HasStrictFDerivAt c c' x) (hd : HasStrictFDerivAt d d' x) :
  HasStrictFDerivAt (fun y => c y * d y) (c x • d' + d x • c') x

Full source

@[fun_prop]
theorem HasStrictFDerivAt.mul (hc : HasStrictFDerivAt c c' x) (hd : HasStrictFDerivAt d d' x) :
    HasStrictFDerivAt (fun y => c y * d y) (c x • d' + d x • c') x := by
  convert hc.mul' hd
  ext z
  apply mul_comm

Strict Differentiability of Product of Functions (Commutative Case) at a Point

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $c, d : E \to F$ be functions strictly differentiable at a point $x \in E$ with strict Fréchet derivatives $c'$ and $d'$ respectively. Then the product function $y \mapsto c(y) \cdot d(y)$ is strictly differentiable at $x$, and its strict Fréchet derivative is given by $c(x) \cdot d' + d(x) \cdot c'$.

HasFDerivWithinAt.mul' theorem

 (ha : HasFDerivWithinAt a a' s x) (hb : HasFDerivWithinAt b b' s x) :
  HasFDerivWithinAt (fun y => a y * b y) (a x • b' + a'.smulRight (b x)) s x

Full source

@[fun_prop]
theorem HasFDerivWithinAt.mul' (ha : HasFDerivWithinAt a a' s x) (hb : HasFDerivWithinAt b b' s x) :
    HasFDerivWithinAt (fun y => a y * b y) (a x • b' + a'.smulRight (b x)) s x := by
  exact ((ContinuousLinearMap.mul 𝕜 𝔸).isBoundedBilinearMap.hasFDerivAt
    (a x, b x)).comp_hasFDerivWithinAt x (ha.prodMk hb)

Product Rule for Fréchet Derivatives within a Set (Noncommutative Case)

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $a, b : E \to F$ be functions differentiable at a point $x \in E$ within a set $s \subseteq E$, with Fréchet derivatives $a'$ and $b'$ respectively. Then the product function $y \mapsto a(y) \cdot b(y)$ is differentiable at $x$ within $s$, and its Fréchet derivative is given by $a(x) \cdot b' + a'(\cdot) \cdot b(x)$.

HasFDerivWithinAt.mul theorem

 (hc : HasFDerivWithinAt c c' s x) (hd : HasFDerivWithinAt d d' s x) :
  HasFDerivWithinAt (fun y => c y * d y) (c x • d' + d x • c') s x

Full source

@[fun_prop]
theorem HasFDerivWithinAt.mul (hc : HasFDerivWithinAt c c' s x) (hd : HasFDerivWithinAt d d' s x) :
    HasFDerivWithinAt (fun y => c y * d y) (c x • d' + d x • c') s x := by
  convert hc.mul' hd
  ext z
  apply mul_comm

Product Rule for Fréchet Derivatives within a Set (Commutative Case)

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $c, d : E \to F$ be functions differentiable at a point $x \in E$ within a set $s \subseteq E$, with Fréchet derivatives $c'$ and $d'$ respectively. Then the product function $y \mapsto c(y) \cdot d(y)$ is differentiable at $x$ within $s$, and its Fréchet derivative is given by $c(x) \cdot d' + d(x) \cdot c'$.

HasFDerivAt.mul' theorem

 (ha : HasFDerivAt a a' x) (hb : HasFDerivAt b b' x) :
  HasFDerivAt (fun y => a y * b y) (a x • b' + a'.smulRight (b x)) x

Full source

@[fun_prop]
theorem HasFDerivAt.mul' (ha : HasFDerivAt a a' x) (hb : HasFDerivAt b b' x) :
    HasFDerivAt (fun y => a y * b y) (a x • b' + a'.smulRight (b x)) x := by
  exact ((ContinuousLinearMap.mul 𝕜 𝔸).isBoundedBilinearMap.hasFDerivAt
    (a x, b x)).comp x (ha.prodMk hb)

Product Rule for Fréchet Derivatives of Noncommutative Multiplication

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $a, b : E \to F$ be functions differentiable at a point $x \in E$ with Fréchet derivatives $a'$ and $b'$ respectively. Then the product function $y \mapsto a(y) * b(y)$ is differentiable at $x$, and its Fréchet derivative is given by $a(x) \cdot b' + a'(\cdot) * b(x)$.

HasFDerivAt.mul theorem

(hc : HasFDerivAt c c' x) (hd : HasFDerivAt d d' x) : HasFDerivAt (fun y => c y * d y) (c x • d' + d x • c') x

Full source

@[fun_prop]
theorem HasFDerivAt.mul (hc : HasFDerivAt c c' x) (hd : HasFDerivAt d d' x) :
    HasFDerivAt (fun y => c y * d y) (c x • d' + d x • c') x := by
  convert hc.mul' hd
  ext z
  apply mul_comm

Product Rule for Fréchet Derivatives of Commutative Multiplication

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $c, d : E \to F$ be functions differentiable at a point $x \in E$ with Fréchet derivatives $c'$ and $d'$ respectively. Then the product function $y \mapsto c(y) \cdot d(y)$ is differentiable at $x$, and its Fréchet derivative is given by $c(x) \cdot d' + d(x) \cdot c'$.

DifferentiableWithinAt.mul theorem

 (ha : DifferentiableWithinAt 𝕜 a s x) (hb : DifferentiableWithinAt 𝕜 b s x) :
  DifferentiableWithinAt 𝕜 (fun y => a y * b y) s x

Full source

@[fun_prop]
theorem DifferentiableWithinAt.mul (ha : DifferentiableWithinAt 𝕜 a s x)
    (hb : DifferentiableWithinAt 𝕜 b s x) : DifferentiableWithinAt 𝕜 (fun y => a y * b y) s x :=
  (ha.hasFDerivWithinAt.mul' hb.hasFDerivWithinAt).differentiableWithinAt

Differentiability of Product Function Within a Set

Informal description

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

DifferentiableAt.mul theorem

(ha : DifferentiableAt 𝕜 a x) (hb : DifferentiableAt 𝕜 b x) : DifferentiableAt 𝕜 (fun y => a y * b y) x

Full source

@[simp, fun_prop]
theorem DifferentiableAt.mul (ha : DifferentiableAt 𝕜 a x) (hb : DifferentiableAt 𝕜 b x) :
    DifferentiableAt 𝕜 (fun y => a y * b y) x :=
  (ha.hasFDerivAt.mul' hb.hasFDerivAt).differentiableAt

Differentiability of Product of Differentiable Functions at a Point

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $a, b : E \to F$ be functions differentiable at a point $x \in E$. Then the product function $y \mapsto a(y) \cdot b(y)$ is differentiable at $x$.

DifferentiableOn.mul theorem

(ha : DifferentiableOn 𝕜 a s) (hb : DifferentiableOn 𝕜 b s) : DifferentiableOn 𝕜 (fun y => a y * b y) s

Full source

@[fun_prop]
theorem DifferentiableOn.mul (ha : DifferentiableOn 𝕜 a s) (hb : DifferentiableOn 𝕜 b s) :
    DifferentiableOn 𝕜 (fun y => a y * b y) s := fun x hx => (ha x hx).mul (hb x hx)

Differentiability of Product Function on a Set

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $a, b : E \to F$ be functions differentiable on a subset $s \subseteq E$. Then the product function $y \mapsto a(y) \cdot b(y)$ is differentiable on $s$.

Differentiable.mul theorem

(ha : Differentiable 𝕜 a) (hb : Differentiable 𝕜 b) : Differentiable 𝕜 fun y => a y * b y

Full source

@[simp, fun_prop]
theorem Differentiable.mul (ha : Differentiable 𝕜 a) (hb : Differentiable 𝕜 b) :
    Differentiable 𝕜 fun y => a y * b y := fun x => (ha x).mul (hb x)

Differentiability of Product of Differentiable Functions

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $a, b : E \to F$ be differentiable functions. Then the product function $y \mapsto a(y) \cdot b(y)$ is differentiable.

DifferentiableWithinAt.pow theorem

(ha : DifferentiableWithinAt 𝕜 a s x) : ∀ n : ℕ, DifferentiableWithinAt 𝕜 (fun x => a x ^ n) s x

Full source

@[fun_prop]
theorem DifferentiableWithinAt.pow (ha : DifferentiableWithinAt 𝕜 a s x) :
    ∀ n : ℕ, DifferentiableWithinAt 𝕜 (fun x => a x ^ n) s x
  | 0 => by simp only [pow_zero, differentiableWithinAt_const]
  | n + 1 => by simp only [pow_succ', DifferentiableWithinAt.pow ha n, ha.mul]

Differentiability of Power Function Within a Set

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $a : E \to F$ be a function differentiable at a point $x \in E$ within a subset $s \subseteq E$. Then for any natural number $n$, the power function $x \mapsto a(x)^n$ is differentiable at $x$ within $s$.

DifferentiableAt.pow theorem

(ha : DifferentiableAt 𝕜 a x) (n : ℕ) : DifferentiableAt 𝕜 (fun x => a x ^ n) x

Full source

@[simp, fun_prop]
theorem DifferentiableAt.pow (ha : DifferentiableAt 𝕜 a x) (n : ℕ) :
    DifferentiableAt 𝕜 (fun x => a x ^ n) x :=
  differentiableWithinAt_univ.mp <| ha.differentiableWithinAt.pow n

Differentiability of Power Function at a Point

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $a : E \to F$ be a function differentiable at a point $x \in E$. Then for any natural number $n$, the power function $x \mapsto a(x)^n$ is differentiable at $x$.

DifferentiableOn.pow theorem

(ha : DifferentiableOn 𝕜 a s) (n : ℕ) : DifferentiableOn 𝕜 (fun x => a x ^ n) s

Full source

@[fun_prop]
theorem DifferentiableOn.pow (ha : DifferentiableOn 𝕜 a s) (n : ℕ) :
    DifferentiableOn 𝕜 (fun x => a x ^ n) s := fun x h => (ha x h).pow n

Differentiability of Power Functions on a Set

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $a : E \to F$ be a function differentiable on a subset $s \subseteq E$. Then for any natural number $n$, the power function $x \mapsto a(x)^n$ is differentiable on $s$.

Differentiable.pow theorem

(ha : Differentiable 𝕜 a) (n : ℕ) : Differentiable 𝕜 fun x => a x ^ n

Full source

@[simp, fun_prop]
theorem Differentiable.pow (ha : Differentiable 𝕜 a) (n : ℕ) : Differentiable 𝕜 fun x => a x ^ n :=
  fun x => (ha x).pow n

Differentiability of Power Functions for Differentiable Maps

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $a : E \to F$ be a differentiable function. Then for any natural number $n$, the power function $x \mapsto a(x)^n$ is differentiable.

fderivWithin_mul' theorem

 (hxs : UniqueDiffWithinAt 𝕜 s x) (ha : DifferentiableWithinAt 𝕜 a s x) (hb : DifferentiableWithinAt 𝕜 b s x) :
  fderivWithin 𝕜 (fun y => a y * b y) s x = a x • fderivWithin 𝕜 b s x + (fderivWithin 𝕜 a s x).smulRight (b x)

Full source

theorem fderivWithin_mul' (hxs : UniqueDiffWithinAt 𝕜 s x) (ha : DifferentiableWithinAt 𝕜 a s x)
    (hb : DifferentiableWithinAt 𝕜 b s x) :
    fderivWithin 𝕜 (fun y => a y * b y) s x =
      a x • fderivWithin 𝕜 b s x + (fderivWithin 𝕜 a s x).smulRight (b x) :=
  (ha.hasFDerivWithinAt.mul' hb.hasFDerivWithinAt).fderivWithin hxs

Product Rule for Fréchet Derivatives within a Uniquely Differentiable Set (Noncommutative Case)

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $a, b : 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 product function $y \mapsto a(y) \cdot b(y)$ at $x$ within $s$ is given by: \[ \text{fderivWithin}_{\mathbb{K}} (a \cdot b) s x = a(x) \cdot \text{fderivWithin}_{\mathbb{K}} b s x + (\text{fderivWithin}_{\mathbb{K}} a s x)(\cdot) \cdot b(x) \]

fderivWithin_mul theorem

 (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x) (hd : DifferentiableWithinAt 𝕜 d s x) :
  fderivWithin 𝕜 (fun y => c y * d y) s x = c x • fderivWithin 𝕜 d s x + d x • fderivWithin 𝕜 c s x

Full source

theorem fderivWithin_mul (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x)
    (hd : DifferentiableWithinAt 𝕜 d s x) :
    fderivWithin 𝕜 (fun y => c y * d y) s x =
      c x • fderivWithin 𝕜 d s x + d x • fderivWithin 𝕜 c s x :=
  (hc.hasFDerivWithinAt.mul hd.hasFDerivWithinAt).fderivWithin hxs

Product Rule for Fréchet Derivatives within a Uniquely Differentiable Set

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $s \subseteq E$ be a subset. Suppose $c, d : E \to F$ are functions differentiable at a point $x \in E$ within $s$, and $s$ is uniquely differentiable at $x$. Then the Fréchet derivative of the product function $y \mapsto c(y) \cdot d(y)$ at $x$ within $s$ is given by: \[ \text{fderivWithin}_{\mathbb{K}} (c \cdot d) s x = c(x) \cdot \text{fderivWithin}_{\mathbb{K}} d s x + d(x) \cdot \text{fderivWithin}_{\mathbb{K}} c s x. \]

fderiv_mul' theorem

 (ha : DifferentiableAt 𝕜 a x) (hb : DifferentiableAt 𝕜 b x) :
  fderiv 𝕜 (fun y => a y * b y) x = a x • fderiv 𝕜 b x + (fderiv 𝕜 a x).smulRight (b x)

Full source

theorem fderiv_mul' (ha : DifferentiableAt 𝕜 a x) (hb : DifferentiableAt 𝕜 b x) :
    fderiv 𝕜 (fun y => a y * b y) x = a x • fderiv 𝕜 b x + (fderiv 𝕜 a x).smulRight (b x) :=
  (ha.hasFDerivAt.mul' hb.hasFDerivAt).fderiv

Product Rule for Fréchet Derivatives (Noncommutative Case)

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, and let $E$ and $F$ be normed spaces over $\mathbb{K}$. Suppose $a, b : E \to F$ are functions differentiable at a point $x \in E$. Then the Fréchet derivative of the product function $y \mapsto a(y) \cdot b(y)$ at $x$ is given by: \[ \text{fderiv}_{\mathbb{K}} (a \cdot b) x = a(x) \cdot \text{fderiv}_{\mathbb{K}} b x + (\text{fderiv}_{\mathbb{K}} a x)(\cdot) \cdot b(x). \]

fderiv_mul theorem

 (hc : DifferentiableAt 𝕜 c x) (hd : DifferentiableAt 𝕜 d x) :
  fderiv 𝕜 (fun y => c y * d y) x = c x • fderiv 𝕜 d x + d x • fderiv 𝕜 c x

Full source

theorem fderiv_mul (hc : DifferentiableAt 𝕜 c x) (hd : DifferentiableAt 𝕜 d x) :
    fderiv 𝕜 (fun y => c y * d y) x = c x • fderiv 𝕜 d x + d x • fderiv 𝕜 c x :=
  (hc.hasFDerivAt.mul hd.hasFDerivAt).fderiv

Product Rule for Fréchet Derivatives of Differentiable Functions

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, and let $E$ and $F$ be normed spaces over $\mathbb{K}$. If functions $c, d : E \to F$ are differentiable at a point $x \in E$, then the Fréchet derivative of their product function $y \mapsto c(y) \cdot d(y)$ at $x$ is given by: \[ \text{fderiv}_{\mathbb{K}} (c \cdot d) x = c(x) \cdot \text{fderiv}_{\mathbb{K}} d x + d(x) \cdot \text{fderiv}_{\mathbb{K}} c x. \]

HasStrictFDerivAt.mul_const' theorem

(ha : HasStrictFDerivAt a a' x) (b : 𝔸) : HasStrictFDerivAt (fun y => a y * b) (a'.smulRight b) x

Full source

@[fun_prop]
theorem HasStrictFDerivAt.mul_const' (ha : HasStrictFDerivAt a a' x) (b : 𝔸) :
    HasStrictFDerivAt (fun y => a y * b) (a'.smulRight b) x :=
  ((ContinuousLinearMap.mul 𝕜 𝔸).flip b).hasStrictFDerivAt.comp x ha

Strict Fréchet Differentiability of Right Multiplication by a Constant

Informal description

Let $E$ and $\mathbb{A}$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $a : E \to \mathbb{A}$ be a function that has a strict Fréchet derivative $a' : E \toL[\mathbb{K}] \mathbb{A}$ at a point $x \in E$. Then for any fixed element $b \in \mathbb{A}$, the function $y \mapsto a(y) \cdot b$ has a strict Fréchet derivative at $x$ given by the continuous linear map $a' \cdot b$, where $\cdot$ denotes the right scalar multiplication of $a'$ by $b$.

HasStrictFDerivAt.mul_const theorem

(hc : HasStrictFDerivAt c c' x) (d : 𝔸') : HasStrictFDerivAt (fun y => c y * d) (d • c') x

Full source

@[fun_prop]
theorem HasStrictFDerivAt.mul_const (hc : HasStrictFDerivAt c c' x) (d : 𝔸') :
    HasStrictFDerivAt (fun y => c y * d) (d • c') x := by
  convert hc.mul_const' d
  ext z
  apply mul_comm

Strict Fréchet Differentiability of Right Multiplication by a Constant in a Normed Algebra

Informal description

Let $E$ and $\mathbb{A}'$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $c : E \to \mathbb{A}'$ be a function that has a strict Fréchet derivative $c' : E \toL[\mathbb{K}] \mathbb{A}'$ at a point $x \in E$. Then for any fixed element $d \in \mathbb{A}'$, the function $y \mapsto c(y) \cdot d$ has a strict Fréchet derivative at $x$ given by the continuous linear map $d \cdot c'$, where $\cdot$ denotes the scalar multiplication of $d$ with $c'$.

HasFDerivWithinAt.mul_const' theorem

(ha : HasFDerivWithinAt a a' s x) (b : 𝔸) : HasFDerivWithinAt (fun y => a y * b) (a'.smulRight b) s x

Full source

@[fun_prop]
theorem HasFDerivWithinAt.mul_const' (ha : HasFDerivWithinAt a a' s x) (b : 𝔸) :
    HasFDerivWithinAt (fun y => a y * b) (a'.smulRight b) s x :=
  ((ContinuousLinearMap.mul 𝕜 𝔸).flip b).hasFDerivAt.comp_hasFDerivWithinAt x ha

Differentiability of Right Multiplication by a Constant within a Set

Informal description

Let $E$ be a normed space over a field $\mathbb{K}$, and let $a : E \to \mathbb{A}$ be a function that is differentiable within a set $s \subseteq E$ at a point $x \in s$, with derivative $a' : E \toL[\mathbb{K}] \mathbb{A}$. Then, for any fixed element $b \in \mathbb{A}$, the function $y \mapsto a(y) \cdot b$ is differentiable within $s$ at $x$, with derivative $a' \cdot b$, where $a' \cdot b$ denotes the continuous linear map obtained by right scalar multiplication of $a'$ by $b$.

HasFDerivWithinAt.mul_const theorem

(hc : HasFDerivWithinAt c c' s x) (d : 𝔸') : HasFDerivWithinAt (fun y => c y * d) (d • c') s x

Full source

@[fun_prop]
theorem HasFDerivWithinAt.mul_const (hc : HasFDerivWithinAt c c' s x) (d : 𝔸') :
    HasFDerivWithinAt (fun y => c y * d) (d • c') s x := by
  convert hc.mul_const' d
  ext z
  apply mul_comm

Differentiability of Right Multiplication by a Constant within a Set in Normed Algebras

Informal description

Let $E$ be a normed space over a nontrivially normed field $\mathbb{K}$, and let $c : E \to \mathbb{A}'$ be a function that is Fréchet differentiable within a set $s \subseteq E$ at a point $x \in s$, with derivative $c' : E \toL[\mathbb{K}] \mathbb{A}'$. Then for any fixed element $d \in \mathbb{A}'$, the function $y \mapsto c(y) \cdot d$ is Fréchet differentiable within $s$ at $x$, with derivative $d \cdot c'$, where $(d \cdot c')(v) = d \cdot c'(v)$ for all $v \in E$.

HasFDerivAt.mul_const' theorem

(ha : HasFDerivAt a a' x) (b : 𝔸) : HasFDerivAt (fun y => a y * b) (a'.smulRight b) x

Full source

@[fun_prop]
theorem HasFDerivAt.mul_const' (ha : HasFDerivAt a a' x) (b : 𝔸) :
    HasFDerivAt (fun y => a y * b) (a'.smulRight b) x :=
  ((ContinuousLinearMap.mul 𝕜 𝔸).flip b).hasFDerivAt.comp x ha

Differentiability of Right Multiplication by a Fixed Element in Normed Algebras

Informal description

Let $E$ and $\mathbb{A}$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $a : E \to \mathbb{A}$ be a function that is Fréchet differentiable at a point $x \in E$ with derivative $a' : E \toL[\mathbb{K}] \mathbb{A}$. Then for any fixed element $b \in \mathbb{A}$, the function $y \mapsto a(y) \cdot b$ is Fréchet differentiable at $x$ with derivative given by the continuous linear map $a' \cdot b$, where $(a' \cdot b)(v) = a'(v) \cdot b$ for all $v \in E$.

HasFDerivAt.mul_const theorem

(hc : HasFDerivAt c c' x) (d : 𝔸') : HasFDerivAt (fun y => c y * d) (d • c') x

Full source

@[fun_prop]
theorem HasFDerivAt.mul_const (hc : HasFDerivAt c c' x) (d : 𝔸') :
    HasFDerivAt (fun y => c y * d) (d • c') x := by
  convert hc.mul_const' d
  ext z
  apply mul_comm

Differentiability of Right Multiplication by a Fixed Element in Normed Algebras (Scalar Multiplication Variant)

Informal description

Let $E$ and $\mathbb{A}'$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $c : E \to \mathbb{A}'$ be a function that is Fréchet differentiable at a point $x \in E$ with derivative $c' : E \toL[\mathbb{K}] \mathbb{A}'$. Then for any fixed element $d \in \mathbb{A}'$, the function $y \mapsto c(y) \cdot d$ is Fréchet differentiable at $x$ with derivative given by the continuous linear map $d \cdot c'$, where $(d \cdot c')(v) = d \cdot c'(v)$ for all $v \in E$.

DifferentiableWithinAt.mul_const theorem

(ha : DifferentiableWithinAt 𝕜 a s x) (b : 𝔸) : DifferentiableWithinAt 𝕜 (fun y => a y * b) s x

Full source

@[fun_prop]
theorem DifferentiableWithinAt.mul_const (ha : DifferentiableWithinAt 𝕜 a s x) (b : 𝔸) :
    DifferentiableWithinAt 𝕜 (fun y => a y * b) s x :=
  (ha.hasFDerivWithinAt.mul_const' b).differentiableWithinAt

Differentiability of right multiplication by a constant within a set

Informal description

Let $E$ and $\mathbb{A}$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $a : E \to \mathbb{A}$ be a function that is differentiable at a point $x \in E$ within a subset $s \subseteq E$. Then for any fixed element $b \in \mathbb{A}$, the function $y \mapsto a(y) \cdot b$ is differentiable at $x$ within $s$.

DifferentiableAt.mul_const theorem

(ha : DifferentiableAt 𝕜 a x) (b : 𝔸) : DifferentiableAt 𝕜 (fun y => a y * b) x

Full source

@[fun_prop]
theorem DifferentiableAt.mul_const (ha : DifferentiableAt 𝕜 a x) (b : 𝔸) :
    DifferentiableAt 𝕜 (fun y => a y * b) x :=
  (ha.hasFDerivAt.mul_const' b).differentiableAt

Differentiability of Right Multiplication by a Fixed Element

Informal description

Let $E$ and $\mathbb{A}$ be normed spaces over a nontrivially normed field $\mathbb{K}$. If a function $a : E \to \mathbb{A}$ is differentiable at a point $x \in E$, then for any fixed element $b \in \mathbb{A}$, the function $y \mapsto a(y) \cdot b$ is differentiable at $x$.

DifferentiableOn.mul_const theorem

(ha : DifferentiableOn 𝕜 a s) (b : 𝔸) : DifferentiableOn 𝕜 (fun y => a y * b) s

Full source

@[fun_prop]
theorem DifferentiableOn.mul_const (ha : DifferentiableOn 𝕜 a s) (b : 𝔸) :
    DifferentiableOn 𝕜 (fun y => a y * b) s := fun x hx => (ha x hx).mul_const b

Differentiability of Right Multiplication by a Constant on a Set

Informal description

Let $E$ and $\mathbb{A}$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $a : E \to \mathbb{A}$ be a function that is differentiable on a subset $s \subseteq E$. Then for any fixed element $b \in \mathbb{A}$, the function $y \mapsto a(y) \cdot b$ is differentiable on $s$.

Differentiable.mul_const theorem

(ha : Differentiable 𝕜 a) (b : 𝔸) : Differentiable 𝕜 fun y => a y * b

Full source

@[fun_prop]
theorem Differentiable.mul_const (ha : Differentiable 𝕜 a) (b : 𝔸) :
    Differentiable 𝕜 fun y => a y * b := fun x => (ha x).mul_const b

Differentiability of Right Multiplication by a Fixed Element

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ a normed space over $\mathbb{K}$, and $\mathbb{A}$ a normed algebra over $\mathbb{K}$. If a function $a : E \to \mathbb{A}$ is differentiable, then for any fixed element $b \in \mathbb{A}$, the function $y \mapsto a(y) \cdot b$ is differentiable.

fderivWithin_mul_const' theorem

 (hxs : UniqueDiffWithinAt 𝕜 s x) (ha : DifferentiableWithinAt 𝕜 a s x) (b : 𝔸) :
  fderivWithin 𝕜 (fun y => a y * b) s x = (fderivWithin 𝕜 a s x).smulRight b

Full source

theorem fderivWithin_mul_const' (hxs : UniqueDiffWithinAt 𝕜 s x)
    (ha : DifferentiableWithinAt 𝕜 a s x) (b : 𝔸) :
    fderivWithin 𝕜 (fun y => a y * b) s x = (fderivWithin 𝕜 a s x).smulRight b :=
  (ha.hasFDerivWithinAt.mul_const' b).fderivWithin hxs

Fréchet derivative of right multiplication by a constant within a set

Informal description

Let $E$ and $\mathbb{A}$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $a : E \to \mathbb{A}$ be a function differentiable at a point $x$ within a subset $s \subseteq E$. If $s$ is uniquely differentiable at $x$, then for any fixed element $b \in \mathbb{A}$, the Fréchet derivative of the function $y \mapsto a(y) \cdot b$ at $x$ within $s$ is equal to the continuous linear map obtained by right scalar multiplication of the Fréchet derivative of $a$ at $x$ within $s$ by $b$.

fderivWithin_mul_const theorem

 (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x) (d : 𝔸') :
  fderivWithin 𝕜 (fun y => c y * d) s x = d • fderivWithin 𝕜 c s x

Full source

theorem fderivWithin_mul_const (hxs : UniqueDiffWithinAt 𝕜 s x)
    (hc : DifferentiableWithinAt 𝕜 c s x) (d : 𝔸') :
    fderivWithin 𝕜 (fun y => c y * d) s x = d • fderivWithin 𝕜 c s x :=
  (hc.hasFDerivWithinAt.mul_const d).fderivWithin hxs

Fréchet Derivative of Right Multiplication by a Constant within a Uniquely Differentiable Set

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ a normed space over $\mathbb{K}$, and $\mathbb{A}'$ a normed algebra over $\mathbb{K}$. Given a subset $s \subseteq E$ that is uniquely differentiable at $x \in s$, if a function $c : E \to \mathbb{A}'$ is differentiable within $s$ at $x$, then for any fixed element $d \in \mathbb{A}'$, the Fréchet derivative within $s$ at $x$ of the function $y \mapsto c(y) \cdot d$ is equal to $d$ multiplied by the Fréchet derivative of $c$ within $s$ at $x$, i.e., \[ \text{fderivWithin}_{\mathbb{K}} (\lambda y, c(y) \cdot d) s x = d \cdot \text{fderivWithin}_{\mathbb{K}} c s x. \]

fderiv_mul_const' theorem

(ha : DifferentiableAt 𝕜 a x) (b : 𝔸) : fderiv 𝕜 (fun y => a y * b) x = (fderiv 𝕜 a x).smulRight b

Full source

theorem fderiv_mul_const' (ha : DifferentiableAt 𝕜 a x) (b : 𝔸) :
    fderiv 𝕜 (fun y => a y * b) x = (fderiv 𝕜 a x).smulRight b :=
  (ha.hasFDerivAt.mul_const' b).fderiv

Fréchet Derivative of Right Multiplication by a Constant

Informal description

Let $E$ and $\mathbb{A}$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $a : E \to \mathbb{A}$ be a function differentiable at a point $x \in E$. Then for any fixed element $b \in \mathbb{A}$, the Fréchet derivative of the function $y \mapsto a(y) \cdot b$ at $x$ is equal to the continuous linear map obtained by right scalar multiplication of the Fréchet derivative of $a$ at $x$ by $b$, i.e., \[ \text{fderiv}_{\mathbb{K}} (\lambda y, a(y) \cdot b) x = (\text{fderiv}_{\mathbb{K}} a x) \cdot b. \]

fderiv_mul_const theorem

(hc : DifferentiableAt 𝕜 c x) (d : 𝔸') : fderiv 𝕜 (fun y => c y * d) x = d • fderiv 𝕜 c x

Full source

theorem fderiv_mul_const (hc : DifferentiableAt 𝕜 c x) (d : 𝔸') :
    fderiv 𝕜 (fun y => c y * d) x = d • fderiv 𝕜 c x :=
  (hc.hasFDerivAt.mul_const d).fderiv

Fréchet Derivative of Right Multiplication by a Constant in Normed Algebras

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ a normed space over $\mathbb{K}$, and $\mathbb{A}'$ a normed algebra over $\mathbb{K}$. If a function $c : E \to \mathbb{A}'$ is differentiable at a point $x \in E$, then for any fixed element $d \in \mathbb{A}'$, the Fréchet derivative at $x$ of the function $y \mapsto c(y) \cdot d$ is equal to $d$ multiplied by the Fréchet derivative of $c$ at $x$, i.e., \[ \text{fderiv}_{\mathbb{K}} (\lambda y, c(y) \cdot d) x = d \cdot \text{fderiv}_{\mathbb{K}} c x. \]

HasStrictFDerivAt.const_mul theorem

(ha : HasStrictFDerivAt a a' x) (b : 𝔸) : HasStrictFDerivAt (fun y => b * a y) (b • a') x

Full source

@[fun_prop]
theorem HasStrictFDerivAt.const_mul (ha : HasStrictFDerivAt a a' x) (b : 𝔸) :
    HasStrictFDerivAt (fun y => b * a y) (b • a') x :=
  ((ContinuousLinearMap.mul 𝕜 𝔸) b).hasStrictFDerivAt.comp x ha

Strict Fréchet Derivative of Constant Multiple of Function

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $\mathfrak{A}$ be a normed algebra over $\mathbb{K}$. Suppose a function $a : E \to \mathfrak{A}$ has a strict Fréchet derivative $a'$ at a point $x \in E$. Then for any constant $b \in \mathfrak{A}$, the function $y \mapsto b \cdot a(y)$ has a strict Fréchet derivative at $x$ given by $b \cdot a'$.

HasFDerivWithinAt.const_mul theorem

(ha : HasFDerivWithinAt a a' s x) (b : 𝔸) : HasFDerivWithinAt (fun y => b * a y) (b • a') s x

Full source

@[fun_prop]
theorem HasFDerivWithinAt.const_mul (ha : HasFDerivWithinAt a a' s x) (b : 𝔸) :
    HasFDerivWithinAt (fun y => b * a y) (b • a') s x :=
  ((ContinuousLinearMap.mul 𝕜 𝔸) b).hasFDerivAt.comp_hasFDerivWithinAt x ha

Differentiation of constant-multiple functions within a set

Informal description

Let $E$ and $\mathbb{A}$ be normed spaces over a nontrivially normed field $\mathbb{K}$, with $\mathbb{A}$ being a normed algebra. Let $a : E \to \mathbb{A}$ be a function that is differentiable within a set $s \subseteq E$ at a point $x \in s$, with Fréchet derivative $a'$ at $x$ within $s$. Then for any constant $b \in \mathbb{A}$, the function $y \mapsto b \cdot a(y)$ is differentiable within $s$ at $x$, and its Fréchet derivative at $x$ within $s$ is the continuous linear map $b \cdot a'$.

HasFDerivAt.const_mul theorem

(ha : HasFDerivAt a a' x) (b : 𝔸) : HasFDerivAt (fun y => b * a y) (b • a') x

Full source

@[fun_prop]
theorem HasFDerivAt.const_mul (ha : HasFDerivAt a a' x) (b : 𝔸) :
    HasFDerivAt (fun y => b * a y) (b • a') x :=
  ((ContinuousLinearMap.mul 𝕜 𝔸) b).hasFDerivAt.comp x ha

Differentiability of Constant Multiple of Differentiable Function

Informal description

Let $E$ and $\mathbb{A}$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $a : E \to \mathbb{A}$ be a function that is Fréchet differentiable at a point $x \in E$ with derivative $a' : E \toL[\mathbb{K}] \mathbb{A}$. Then for any constant $b \in \mathbb{A}$, the function $y \mapsto b \cdot a(y)$ is Fréchet differentiable at $x$ with derivative $b \cdot a'$, where $\cdot$ denotes the scalar multiplication in $\mathbb{A}$.

DifferentiableWithinAt.const_mul theorem

(ha : DifferentiableWithinAt 𝕜 a s x) (b : 𝔸) : DifferentiableWithinAt 𝕜 (fun y => b * a y) s x

Full source

@[fun_prop]
theorem DifferentiableWithinAt.const_mul (ha : DifferentiableWithinAt 𝕜 a s x) (b : 𝔸) :
    DifferentiableWithinAt 𝕜 (fun y => b * a y) s x :=
  (ha.hasFDerivWithinAt.const_mul b).differentiableWithinAt

Differentiability of constant multiple within a set

Informal description

Let $E$ and $\mathbb{A}$ be normed spaces over a nontrivially normed field $\mathbb{K}$, with $\mathbb{A}$ being a normed algebra. If a function $a : E \to \mathbb{A}$ is differentiable at a point $x \in E$ within a subset $s \subseteq E$, then for any constant $b \in \mathbb{A}$, the function $y \mapsto b \cdot a(y)$ is also differentiable at $x$ within $s$.

DifferentiableAt.const_mul theorem

(ha : DifferentiableAt 𝕜 a x) (b : 𝔸) : DifferentiableAt 𝕜 (fun y => b * a y) x

Full source

@[fun_prop]
theorem DifferentiableAt.const_mul (ha : DifferentiableAt 𝕜 a x) (b : 𝔸) :
    DifferentiableAt 𝕜 (fun y => b * a y) x :=
  (ha.hasFDerivAt.const_mul b).differentiableAt

Differentiability of Constant Multiple of Differentiable Function at a Point

Informal description

Let $E$ be a normed space over a nontrivially normed field $\mathbb{K}$, and let $\mathbb{A}$ be a normed algebra over $\mathbb{K}$. If a function $a : E \to \mathbb{A}$ is differentiable at a point $x \in E$, then for any constant $b \in \mathbb{A}$, the function $y \mapsto b \cdot a(y)$ is differentiable at $x$.

DifferentiableOn.const_mul theorem

(ha : DifferentiableOn 𝕜 a s) (b : 𝔸) : DifferentiableOn 𝕜 (fun y => b * a y) s

Full source

@[fun_prop]
theorem DifferentiableOn.const_mul (ha : DifferentiableOn 𝕜 a s) (b : 𝔸) :
    DifferentiableOn 𝕜 (fun y => b * a y) s := fun x hx => (ha x hx).const_mul b

Differentiability of constant multiple on a set

Informal description

Let $E$ be a normed space over a nontrivially normed field $\mathbb{K}$, and let $\mathbb{A}$ be a normed algebra over $\mathbb{K}$. If a function $a : E \to \mathbb{A}$ is differentiable on a subset $s \subseteq E$, then for any constant $b \in \mathbb{A}$, the function $y \mapsto b \cdot a(y)$ is differentiable on $s$.

Differentiable.const_mul theorem

(ha : Differentiable 𝕜 a) (b : 𝔸) : Differentiable 𝕜 fun y => b * a y

Full source

@[fun_prop]
theorem Differentiable.const_mul (ha : Differentiable 𝕜 a) (b : 𝔸) :
    Differentiable 𝕜 fun y => b * a y := fun x => (ha x).const_mul b

Differentiability of Constant Multiple of Differentiable Function

Informal description

Let $E$ be a normed space over a nontrivially normed field $\mathbb{K}$, and let $\mathbb{A}$ be a normed algebra over $\mathbb{K}$. If a function $a : E \to \mathbb{A}$ is differentiable, then for any constant $b \in \mathbb{A}$, the function $y \mapsto b \cdot a(y)$ is differentiable.

fderivWithin_const_mul theorem

 (hxs : UniqueDiffWithinAt 𝕜 s x) (ha : DifferentiableWithinAt 𝕜 a s x) (b : 𝔸) :
  fderivWithin 𝕜 (fun y => b * a y) s x = b • fderivWithin 𝕜 a s x

Full source

theorem fderivWithin_const_mul (hxs : UniqueDiffWithinAt 𝕜 s x)
    (ha : DifferentiableWithinAt 𝕜 a s x) (b : 𝔸) :
    fderivWithin 𝕜 (fun y => b * a y) s x = b • fderivWithin 𝕜 a s x :=
  (ha.hasFDerivWithinAt.const_mul b).fderivWithin hxs

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

Informal description

Let $E$ be a normed space over a nontrivially normed field $\mathbb{K}$, and let $\mathbb{A}$ be a normed algebra over $\mathbb{K}$. Suppose $a : E \to \mathbb{A}$ is differentiable at a point $x \in E$ within a subset $s \subseteq E$, and $s$ is uniquely differentiable at $x$. Then for any constant $b \in \mathbb{A}$, the Fréchet derivative of the function $y \mapsto b \cdot a(y)$ at $x$ within $s$ is given by $b \cdot \text{fderivWithin}_{\mathbb{K}} a s x$.

fderiv_const_mul theorem

(ha : DifferentiableAt 𝕜 a x) (b : 𝔸) : fderiv 𝕜 (fun y => b * a y) x = b • fderiv 𝕜 a x

Full source

theorem fderiv_const_mul (ha : DifferentiableAt 𝕜 a x) (b : 𝔸) :
    fderiv 𝕜 (fun y => b * a y) x = b • fderiv 𝕜 a x :=
  (ha.hasFDerivAt.const_mul b).fderiv

Fréchet Derivative of Constant Multiple: $\text{fderiv}_{\mathbb{K}} (b \cdot a) x = b \cdot \text{fderiv}_{\mathbb{K}} a x$

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ a normed space over $\mathbb{K}$, and $\mathbb{A}$ a normed algebra over $\mathbb{K}$. If a function $a : E \to \mathbb{A}$ is differentiable at a point $x \in E$, then for any constant $b \in \mathbb{A}$, the Fréchet derivative of the function $y \mapsto b \cdot a(y)$ at $x$ is given by $b \cdot \text{fderiv}_{\mathbb{K}} a x$.

hasStrictFDerivAt_list_prod' theorem

 [Fintype ι] {l : List ι} {x : ι → 𝔸} :
  HasStrictFDerivAt (𝕜 := 𝕜) (fun x ↦ (l.map x).prod)
    (∑ i : Fin l.length, ((l.take i).map x).prod • smulRight (proj l[i]) ((l.drop (.succ i)).map x).prod) x

Full source

@[fun_prop]
theorem hasStrictFDerivAt_list_prod' [Fintype ι] {l : List ι} {x : ι → 𝔸} :
    HasStrictFDerivAt (𝕜 := 𝕜) (fun x ↦ (l.map x).prod)
      (∑ i : Fin l.length, ((l.take i).map x).prod •
        smulRight (proj l[i]) ((l.drop (.succ i)).map x).prod) x := by
  induction l with
  | nil => simp [hasStrictFDerivAt_const]
  | cons a l IH =>
    simp only [List.map_cons, List.prod_cons, ← proj_apply (R := 𝕜) (φ := fun _ : ι ↦ 𝔸) a]
    exact .congr_fderiv (.mul' (ContinuousLinearMap.hasStrictFDerivAt _) IH)
      (by ext; simp [Fin.sum_univ_succ, Finset.mul_sum, mul_assoc, add_comm])

Strict Fréchet Differentiability of Finite Product in Normed Algebras

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $\mathbb{A}$ be a normed algebra over $\mathbb{K}$, and $\iota$ be a finite type. Given a list $l$ of elements in $\iota$ and a function $x \colon \iota \to \mathbb{A}$, the product function $x \mapsto \prod_{i \in l} x(i)$ is strictly Fréchet differentiable at $x$, with derivative given by the sum \[ \sum_{i=1}^{|l|} \left( \prod_{j < i} x(l[j]) \right) \cdot \left( \text{proj}_{l[i]} \right) \cdot \left( \prod_{j > i} x(l[j]) \right), \] where $\text{proj}_{l[i]}$ denotes the projection onto the $l[i]$-th component, and the products are taken over the elements of $l$ before and after the $i$-th position, respectively.

hasStrictFDerivAt_list_prod_finRange' theorem

 {n : ℕ} {x : Fin n → 𝔸} :
  HasStrictFDerivAt (𝕜 := 𝕜) (fun x ↦ ((List.finRange n).map x).prod)
    (∑ i : Fin n,
      (((List.finRange n).take i).map x).prod • smulRight (proj i) (((List.finRange n).drop (.succ i)).map x).prod)
    x

Full source

@[fun_prop]
theorem hasStrictFDerivAt_list_prod_finRange' {n : ℕ} {x : Fin n → 𝔸} :
    HasStrictFDerivAt (𝕜 := 𝕜) (fun x ↦ ((List.finRange n).map x).prod)
      (∑ i : Fin n, (((List.finRange n).take i).map x).prod •
        smulRight (proj i) (((List.finRange n).drop (.succ i)).map x).prod) x :=
  hasStrictFDerivAt_list_prod'.congr_fderiv <|
    Finset.sum_equiv (finCongr List.length_finRange) (by simp) (by simp [Fin.forall_iff])

Strict Fréchet Differentiability of Finite Product over $\mathrm{Fin}(n)$ in Normed Algebras

Informal description

Let $\mathbb{K}$ be a nontrivially normed field and $\mathbb{A}$ be a normed algebra over $\mathbb{K}$. For any natural number $n$ and function $x \colon \mathrm{Fin}(n) \to \mathbb{A}$, the product function $x \mapsto \prod_{i=1}^n x(i)$ is strictly Fréchet differentiable at $x$, with derivative given by the sum \[ \sum_{i=1}^n \left( \prod_{j < i} x(j) \right) \cdot \left( \text{proj}_i \right) \cdot \left( \prod_{j > i} x(j) \right), \] where $\text{proj}_i$ denotes the projection onto the $i$-th component.

hasStrictFDerivAt_list_prod_attach' theorem

 {l : List ι} {x : { i // i ∈ l } → 𝔸} :
  HasStrictFDerivAt (𝕜 := 𝕜) (fun x ↦ (l.attach.map x).prod)
    (∑ i : Fin l.length,
      ((l.attach.take i).map x).prod •
        smulRight (proj l.attach[i.cast List.length_attach.symm]) ((l.attach.drop (.succ i)).map x).prod)
    x

Full source

@[fun_prop]
theorem hasStrictFDerivAt_list_prod_attach' {l : List ι} {x : {i // i ∈ l} → 𝔸} :
    HasStrictFDerivAt (𝕜 := 𝕜) (fun x ↦ (l.attach.map x).prod)
      (∑ i : Fin l.length, ((l.attach.take i).map x).prod •
        smulRight (proj l.attach[i.cast List.length_attach.symm])
          ((l.attach.drop (.succ i)).map x).prod) x := by
  classical exact hasStrictFDerivAt_list_prod'.congr_fderiv <| Eq.symm <|
    Finset.sum_equiv (finCongr List.length_attach.symm) (by simp) (by simp)

Strict Fréchet Differentiability of Finite Product over List Attachment in Normed Algebras

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $\mathbb{A}$ be a normed algebra over $\mathbb{K}$, and $l$ be a list of elements in some index type $\iota$. Given a function $x \colon \{i \mid i \in l\} \to \mathbb{A}$ defined on the subtype of elements in $l$, the product function $x \mapsto \prod_{i \in l} x(i)$ is strictly Fréchet differentiable at $x$, with derivative given by the sum \[ \sum_{i=1}^{|l|} \left( \prod_{j < i} x(l[j]) \right) \cdot \left( \text{proj}_{l[i]} \right) \cdot \left( \prod_{j > i} x(l[j]) \right), \] where $\text{proj}_{l[i]}$ denotes the projection onto the $l[i]$-th component, and the products are taken over the elements of $l$ before and after the $i$-th position, respectively.

hasFDerivAt_list_prod' theorem

 [Fintype ι] {l : List ι} {x : ι → 𝔸'} :
  HasFDerivAt (𝕜 := 𝕜) (fun x ↦ (l.map x).prod)
    (∑ i : Fin l.length, ((l.take i).map x).prod • smulRight (proj l[i]) ((l.drop (.succ i)).map x).prod) x

Full source

@[fun_prop]
theorem hasFDerivAt_list_prod' [Fintype ι] {l : List ι} {x : ι → 𝔸'} :
    HasFDerivAt (𝕜 := 𝕜) (fun x ↦ (l.map x).prod)
      (∑ i : Fin l.length, ((l.take i).map x).prod •
        smulRight (proj l[i]) ((l.drop (.succ i)).map x).prod) x :=
  hasStrictFDerivAt_list_prod'.hasFDerivAt

Fréchet Differentiability of Finite Product in Normed Algebras

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $\mathbb{A}$ be a normed algebra over $\mathbb{K}$, and $\iota$ be a finite type. Given a list $l$ of elements in $\iota$ and a function $x \colon \iota \to \mathbb{A}$, the product function $x \mapsto \prod_{i \in l} x(i)$ is Fréchet differentiable at $x$, with derivative given by the sum \[ \sum_{i=1}^{|l|} \left( \prod_{j < i} x(l[j]) \right) \cdot \left( \text{proj}_{l[i]} \right) \cdot \left( \prod_{j > i} x(l[j]) \right), \] where $\text{proj}_{l[i]}$ denotes the projection onto the $l[i]$-th component, and the products are taken over the elements of $l$ before and after the $i$-th position, respectively.

hasFDerivAt_list_prod_finRange' theorem

 {n : ℕ} {x : Fin n → 𝔸} :
  HasFDerivAt (𝕜 := 𝕜) (fun x ↦ ((List.finRange n).map x).prod)
    (∑ i : Fin n,
      (((List.finRange n).take i).map x).prod • smulRight (proj i) (((List.finRange n).drop (.succ i)).map x).prod)
    x

Full source

@[fun_prop]
theorem hasFDerivAt_list_prod_finRange' {n : ℕ} {x : Fin n → 𝔸} :
    HasFDerivAt (𝕜 := 𝕜) (fun x ↦ ((List.finRange n).map x).prod)
      (∑ i : Fin n, (((List.finRange n).take i).map x).prod •
        smulRight (proj i) (((List.finRange n).drop (.succ i)).map x).prod) x :=
  (hasStrictFDerivAt_list_prod_finRange').hasFDerivAt

Fréchet Differentiability of Finite Product over $\mathrm{Fin}(n)$ in Normed Algebras

Informal description

Let $\mathbb{K}$ be a nontrivially normed field and $\mathbb{A}$ be a normed algebra over $\mathbb{K}$. For any natural number $n$ and function $x \colon \mathrm{Fin}(n) \to \mathbb{A}$, the product function $x \mapsto \prod_{i=1}^n x(i)$ is Fréchet differentiable at $x$, with derivative given by the sum \[ \sum_{i=1}^n \left( \prod_{j < i} x(j) \right) \cdot \left( \text{proj}_i \right) \cdot \left( \prod_{j > i} x(j) \right), \] where $\text{proj}_i$ denotes the projection onto the $i$-th component.

hasFDerivAt_list_prod_attach' theorem

 {l : List ι} {x : { i // i ∈ l } → 𝔸} :
  HasFDerivAt (𝕜 := 𝕜) (fun x ↦ (l.attach.map x).prod)
    (∑ i : Fin l.length,
      ((l.attach.take i).map x).prod •
        smulRight (proj l.attach[i.cast List.length_attach.symm]) ((l.attach.drop (.succ i)).map x).prod)
    x

Full source

@[fun_prop]
theorem hasFDerivAt_list_prod_attach' {l : List ι} {x : {i // i ∈ l} → 𝔸} :
    HasFDerivAt (𝕜 := 𝕜) (fun x ↦ (l.attach.map x).prod)
      (∑ i : Fin l.length, ((l.attach.take i).map x).prod •
        smulRight (proj l.attach[i.cast List.length_attach.symm])
          ((l.attach.drop (.succ i)).map x).prod) x := by
  classical exact hasStrictFDerivAt_list_prod_attach'.hasFDerivAt

Fréchet Differentiability of Finite Product over List Attachment in Normed Algebras

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $\mathbb{A}$ be a normed algebra over $\mathbb{K}$, and $l$ be a list of elements in some index type $\iota$. Given a function $x \colon \{i \mid i \in l\} \to \mathbb{A}$ defined on the subtype of elements in $l$, the product function $x \mapsto \prod_{i \in l} x(i)$ is Fréchet differentiable at $x$, with derivative given by the sum \[ \sum_{i=1}^{|l|} \left( \prod_{j < i} x(l[j]) \right) \cdot \left( \text{proj}_{l[i]} \right) \cdot \left( \prod_{j > i} x(l[j]) \right), \] where $\text{proj}_{l[i]}$ denotes the projection onto the $l[i]$-th component, and the products are taken over the elements of $l$ before and after the $i$-th position, respectively.

hasStrictFDerivAt_list_prod theorem

 [DecidableEq ι] [Fintype ι] {l : List ι} {x : ι → 𝔸'} :
  HasStrictFDerivAt (𝕜 := 𝕜) (fun x ↦ (l.map x).prod) (l.map fun i ↦ ((l.erase i).map x).prod • proj i).sum x

Full source

/--
Auxiliary lemma for `hasStrictFDerivAt_multiset_prod`.

For `NormedCommRing 𝔸'`, can rewrite as `Multiset` using `Multiset.prod_coe`.
-/
@[fun_prop]
theorem hasStrictFDerivAt_list_prod [DecidableEq ι] [Fintype ι] {l : List ι} {x : ι → 𝔸'} :
    HasStrictFDerivAt (𝕜 := 𝕜) (fun x ↦ (l.map x).prod)
      (l.map fun i ↦ ((l.erase i).map x).prod • proj i).sum x := by
  refine hasStrictFDerivAt_list_prod'.congr_fderiv ?_
  conv_rhs => arg 1; arg 2; rw [← List.finRange_map_get l]
  simp only [List.map_map, ← List.sum_toFinset _ (List.nodup_finRange _), List.toFinset_finRange,
    Function.comp_def, ((List.erase_getElem _).map _).prod_eq, List.eraseIdx_eq_take_drop_succ,
    List.map_append, List.prod_append, List.get_eq_getElem, Fin.getElem_fin, Nat.succ_eq_add_one]
  exact Finset.sum_congr rfl fun i _ ↦ by
    ext; simp only [smul_apply, smulRight_apply, smul_eq_mul]; ring

Strict Fréchet Differentiability of Finite Product in Normed Commutative Algebras

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $\mathbb{A}'$ be a normed commutative algebra over $\mathbb{K}$, and $\iota$ be a finite type with decidable equality. Given a list $l$ of elements in $\iota$ and a function $x \colon \iota \to \mathbb{A}'$, the product function $x \mapsto \prod_{i \in l} x(i)$ is strictly Fréchet differentiable at $x$, with derivative given by the sum \[ \sum_{i \in l} \left( \prod_{j \in l \setminus \{i\}} x(j) \right) \cdot \text{proj}_i, \] where $\text{proj}_i$ denotes the projection onto the $i$-th component.

hasStrictFDerivAt_multiset_prod theorem

 [DecidableEq ι] [Fintype ι] {u : Multiset ι} {x : ι → 𝔸'} :
  HasStrictFDerivAt (𝕜 := 𝕜) (fun x ↦ (u.map x).prod) (u.map (fun i ↦ ((u.erase i).map x).prod • proj i)).sum x

Full source

@[fun_prop]
theorem hasStrictFDerivAt_multiset_prod [DecidableEq ι] [Fintype ι] {u : Multiset ι} {x : ι → 𝔸'} :
    HasStrictFDerivAt (𝕜 := 𝕜) (fun x ↦ (u.map x).prod)
      (u.map (fun i ↦ ((u.erase i).map x).prod • proj i)).sum x :=
  u.inductionOn fun l ↦ by simpa using hasStrictFDerivAt_list_prod

Strict Fréchet Differentiability of Finite Multiset Product in Normed Commutative Algebras

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $\mathbb{A}'$ be a normed commutative algebra over $\mathbb{K}$, and $\iota$ be a finite type with decidable equality. Given a multiset $u$ of elements in $\iota$ and a function $x \colon \iota \to \mathbb{A}'$, the product function $x \mapsto \prod_{i \in u} x(i)$ is strictly Fréchet differentiable at $x$, with derivative given by the sum \[ \sum_{i \in u} \left( \prod_{j \in u \setminus \{i\}} x(j) \right) \cdot \text{proj}_i, \] where $\text{proj}_i$ denotes the projection onto the $i$-th component.

hasFDerivAt_multiset_prod theorem

 [DecidableEq ι] [Fintype ι] {u : Multiset ι} {x : ι → 𝔸'} :
  HasFDerivAt (𝕜 := 𝕜) (fun x ↦ (u.map x).prod) (Multiset.sum (u.map (fun i ↦ ((u.erase i).map x).prod • proj i))) x

Full source

@[fun_prop]
theorem hasFDerivAt_multiset_prod [DecidableEq ι] [Fintype ι] {u : Multiset ι} {x : ι → 𝔸'} :
    HasFDerivAt (𝕜 := 𝕜) (fun x ↦ (u.map x).prod)
      (Multiset.sum (u.map (fun i ↦ ((u.erase i).map x).prod • proj i))) x :=
  hasStrictFDerivAt_multiset_prod.hasFDerivAt

Fréchet Differentiability of Finite Multiset Product in Normed Commutative Algebras

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $\mathbb{A}'$ be a normed commutative algebra over $\mathbb{K}$, and $\iota$ be a finite type with decidable equality. Given a multiset $u$ of elements in $\iota$ and a function $x \colon \iota \to \mathbb{A}'$, the product function $x \mapsto \prod_{i \in u} x(i)$ is Fréchet differentiable at $x$, with derivative given by the sum \[ \sum_{i \in u} \left( \prod_{j \in u \setminus \{i\}} x(j) \right) \cdot \text{proj}_i, \] where $\text{proj}_i$ denotes the projection onto the $i$-th component.

hasStrictFDerivAt_finset_prod theorem

 [DecidableEq ι] [Fintype ι] {x : ι → 𝔸'} :
  HasStrictFDerivAt (𝕜 := 𝕜) (∏ i ∈ u, · i) (∑ i ∈ u, (∏ j ∈ u.erase i, x j) • proj i) x

Full source

theorem hasStrictFDerivAt_finset_prod [DecidableEq ι] [Fintype ι] {x : ι → 𝔸'} :
    HasStrictFDerivAt (𝕜 := 𝕜) (∏ i ∈ u, · i) (∑ i ∈ u, (∏ j ∈ u.erase i, x j) • proj i) x := by
  simp only [Finset.sum_eq_multiset_sum, Finset.prod_eq_multiset_prod]
  exact hasStrictFDerivAt_multiset_prod

Strict Fréchet Differentiability of Finite Product in Normed Commutative Algebras

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $\mathbb{A}'$ be a normed commutative algebra over $\mathbb{K}$, and $\iota$ be a finite type with decidable equality. Given a finite set $u \subseteq \iota$ and a function $x \colon \iota \to \mathbb{A}'$, the product function $x \mapsto \prod_{i \in u} x(i)$ is strictly Fréchet differentiable at $x$, with derivative given by the sum \[ \sum_{i \in u} \left( \prod_{j \in u \setminus \{i\}} x(j) \right) \cdot \text{proj}_i, \] where $\text{proj}_i$ denotes the projection onto the $i$-th component.

hasFDerivAt_finset_prod theorem

 [DecidableEq ι] [Fintype ι] {x : ι → 𝔸'} :
  HasFDerivAt (𝕜 := 𝕜) (∏ i ∈ u, · i) (∑ i ∈ u, (∏ j ∈ u.erase i, x j) • proj i) x

Full source

theorem hasFDerivAt_finset_prod [DecidableEq ι] [Fintype ι] {x : ι → 𝔸'} :
    HasFDerivAt (𝕜 := 𝕜) (∏ i ∈ u, · i) (∑ i ∈ u, (∏ j ∈ u.erase i, x j) • proj i) x :=
  hasStrictFDerivAt_finset_prod.hasFDerivAt

Fréchet Differentiability of Finite Product in Normed Commutative Algebras

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $\mathbb{A}'$ a normed commutative algebra over $\mathbb{K}$, and $\iota$ a finite type with decidable equality. Given a finite set $u \subseteq \iota$ and a function $x \colon \iota \to \mathbb{A}'$, the product function $x \mapsto \prod_{i \in u} x(i)$ is Fréchet differentiable at $x$, with derivative given by the sum \[ \sum_{i \in u} \left( \prod_{j \in u \setminus \{i\}} x(j) \right) \cdot \text{proj}_i, \] where $\text{proj}_i$ denotes the projection onto the $i$-th component.

HasStrictFDerivAt.list_prod' theorem

 {l : List ι} {x : E} (h : ∀ i ∈ l, HasStrictFDerivAt (f i ·) (f' i) x) :
  HasStrictFDerivAt (fun x ↦ (l.map (f · x)).prod)
    (∑ i : Fin l.length, ((l.take i).map (f · x)).prod • smulRight (f' l[i]) ((l.drop (.succ i)).map (f · x)).prod) x

Full source

@[fun_prop]
theorem HasStrictFDerivAt.list_prod' {l : List ι} {x : E}
    (h : ∀ i ∈ l, HasStrictFDerivAt (f i ·) (f' i) x) :
    HasStrictFDerivAt (fun x ↦ (l.map (f · x)).prod)
      (∑ i : Fin l.length, ((l.take i).map (f · x)).prod •
        smulRight (f' l[i]) ((l.drop (.succ i)).map (f · x)).prod) x := by
  simp_rw [Fin.getElem_fin, ← l.get_eq_getElem, ← List.finRange_map_get l, List.map_map]
  -- After #19108, we have to be optimistic with `:)`s; otherwise Lean decides it need to find
  -- `NormedAddCommGroup (List 𝔸)` which is nonsense.
  refine .congr_fderiv (hasStrictFDerivAt_list_prod_finRange'.comp x
    (hasStrictFDerivAt_pi.mpr fun i ↦ h (l.get i) (List.getElem_mem ..)) :) ?_
  ext m
  simp_rw [List.map_take, List.map_drop, List.map_map, comp_apply, sum_apply, smul_apply,
    smulRight_apply, proj_apply, pi_apply, Function.comp_def]

Strict Fréchet Differentiability of Finite Product of Differentiable Functions

Informal description

Let $E$ be a normed space over a non-discrete normed field $\mathbb{K}$, and let $\iota$ be an index type. Given a list $l$ of elements of $\iota$, a point $x \in E$, and for each $i \in l$ a function $f_i : E \to \mathbb{A}$ that is strictly Fréchet differentiable at $x$ with derivative $f'_i$, the product function $x \mapsto \prod_{i \in l} f_i(x)$ is strictly Fréchet differentiable at $x$ with derivative \[ \sum_{i=1}^{|l|} \left( \prod_{j < i} f_j(x) \right) \cdot \left( f'_i \right) \cdot \left( \prod_{j > i} f_j(x) \right), \] where $|l|$ denotes the length of the list $l$.

HasFDerivAt.list_prod' theorem

 {l : List ι} {x : E} (h : ∀ i ∈ l, HasFDerivAt (f i ·) (f' i) x) :
  HasFDerivAt (fun x ↦ (l.map (f · x)).prod)
    (∑ i : Fin l.length, ((l.take i).map (f · x)).prod • smulRight (f' l[i]) ((l.drop (.succ i)).map (f · x)).prod) x

Full source

/--
Unlike `HasFDerivAt.finset_prod`, supports non-commutative multiply and duplicate elements.
-/
@[fun_prop]
theorem HasFDerivAt.list_prod' {l : List ι} {x : E}
    (h : ∀ i ∈ l, HasFDerivAt (f i ·) (f' i) x) :
    HasFDerivAt (fun x ↦ (l.map (f · x)).prod)
      (∑ i : Fin l.length, ((l.take i).map (f · x)).prod •
        smulRight (f' l[i]) ((l.drop (.succ i)).map (f · x)).prod) x := by
  simp_rw [Fin.getElem_fin, ← l.get_eq_getElem, ← List.finRange_map_get l, List.map_map]
  refine .congr_fderiv (hasFDerivAt_list_prod_finRange'.comp x
    (hasFDerivAt_pi.mpr fun i ↦ h (l.get i) (l.get_mem i)) :) ?_
  ext m
  simp_rw [List.map_take, List.map_drop, List.map_map, comp_apply, sum_apply, smul_apply,
    smulRight_apply, proj_apply, pi_apply, Function.comp_def]

Fréchet Differentiability of Finite Product of Differentiable Functions

Informal description

Let $E$ be a normed space over a non-discrete normed field $\mathbb{K}$, and let $\iota$ be an index type. Given a list $l$ of elements of $\iota$, a point $x \in E$, and for each $i \in l$ a function $f_i : E \to \mathbb{A}$ that is Fréchet differentiable at $x$ with derivative $f'_i$, the product function $x \mapsto \prod_{i \in l} f_i(x)$ is Fréchet differentiable at $x$ with derivative \[ \sum_{i=1}^{|l|} \left( \prod_{j < i} f_j(x) \right) \cdot \left( f'_i \right) \cdot \left( \prod_{j > i} f_j(x) \right), \] where $|l|$ denotes the length of the list $l$.

HasFDerivWithinAt.list_prod' theorem

 {l : List ι} {x : E} (h : ∀ i ∈ l, HasFDerivWithinAt (f i ·) (f' i) s x) :
  HasFDerivWithinAt (fun x ↦ (l.map (f · x)).prod)
    (∑ i : Fin l.length, ((l.take i).map (f · x)).prod • smulRight (f' l[i]) ((l.drop (.succ i)).map (f · x)).prod) s x

Full source

@[fun_prop]
theorem HasFDerivWithinAt.list_prod' {l : List ι} {x : E}
    (h : ∀ i ∈ l, HasFDerivWithinAt (f i ·) (f' i) s x) :
    HasFDerivWithinAt (fun x ↦ (l.map (f · x)).prod)
      (∑ i : Fin l.length, ((l.take i).map (f · x)).prod •
        smulRight (f' l[i]) ((l.drop (.succ i)).map (f · x)).prod) s x := by
  simp_rw [Fin.getElem_fin, ← l.get_eq_getElem, ← List.finRange_map_get l, List.map_map]
  refine .congr_fderiv (hasFDerivAt_list_prod_finRange'.comp_hasFDerivWithinAt x
    (hasFDerivWithinAt_pi.mpr fun i ↦ h (l.get i) (l.get_mem i)) :) ?_
  ext m
  simp_rw [List.map_take, List.map_drop, List.map_map, comp_apply, sum_apply, smul_apply,
    smulRight_apply, proj_apply, pi_apply, Function.comp_def]

Fréchet Differentiability of Finite Product Within a Set

Informal description

Let $E$ be a normed space over a non-discrete normed field $\mathbb{K}$, $\iota$ be an index type, and $s \subseteq E$ be a subset. Given a list $l$ of elements of $\iota$, a point $x \in E$, and for each $i \in l$ a function $f_i : E \to \mathbb{A}$ that is Fréchet differentiable within $s$ at $x$ with derivative $f'_i$, the product function $x \mapsto \prod_{i \in l} f_i(x)$ is Fréchet differentiable within $s$ at $x$ with derivative \[ \sum_{i=1}^{|l|} \left( \prod_{j < i} f_j(x) \right) \cdot \left( f'_i \right) \cdot \left( \prod_{j > i} f_j(x) \right), \] where $|l|$ denotes the length of the list $l$.

fderiv_list_prod' theorem

 {l : List ι} {x : E} (h : ∀ i ∈ l, DifferentiableAt 𝕜 (f i ·) x) :
  fderiv 𝕜 (fun x ↦ (l.map (f · x)).prod) x =
    ∑ i : Fin l.length,
      ((l.take i).map (f · x)).prod • smulRight (fderiv 𝕜 (fun x ↦ f l[i] x) x) ((l.drop (.succ i)).map (f · x)).prod

Full source

theorem fderiv_list_prod' {l : List ι} {x : E}
    (h : ∀ i ∈ l, DifferentiableAt 𝕜 (f i ·) x) :
    fderiv 𝕜 (fun x ↦ (l.map (f · x)).prod) x =
      ∑ i : Fin l.length, ((l.take i).map (f · x)).prod •
        smulRight (fderiv 𝕜 (fun x ↦ f l[i] x) x) ((l.drop (.succ i)).map (f · x)).prod :=
  (HasFDerivAt.list_prod' fun i hi ↦ (h i hi).hasFDerivAt).fderiv

Fréchet Derivative of a Finite Product of Differentiable Functions

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ a normed space over $\mathbb{K}$, and $\iota$ an index type. Given a list $l$ of elements of $\iota$ and a point $x \in E$, suppose that for each $i \in l$, the function $f_i : E \to \mathbb{A}$ is differentiable at $x$. Then the Fréchet derivative at $x$ of the product function $x \mapsto \prod_{i \in l} f_i(x)$ is given by \[ \sum_{i=1}^{|l|} \left( \prod_{j < i} f_j(x) \right) \cdot \left( \text{fderiv}_{\mathbb{K}} (f_i) x \right) \cdot \left( \prod_{j > i} f_j(x) \right), \] where $|l|$ denotes the length of the list $l$.

fderivWithin_list_prod' theorem

 {l : List ι} {x : E} (hxs : UniqueDiffWithinAt 𝕜 s x) (h : ∀ i ∈ l, DifferentiableWithinAt 𝕜 (f i ·) s x) :
  fderivWithin 𝕜 (fun x ↦ (l.map (f · x)).prod) s x =
    ∑ i : Fin l.length,
      ((l.take i).map (f · x)).prod •
        smulRight (fderivWithin 𝕜 (fun x ↦ f l[i] x) s x) ((l.drop (.succ i)).map (f · x)).prod

Full source

theorem fderivWithin_list_prod' {l : List ι} {x : E}
    (hxs : UniqueDiffWithinAt 𝕜 s x) (h : ∀ i ∈ l, DifferentiableWithinAt 𝕜 (f i ·) s x) :
    fderivWithin 𝕜 (fun x ↦ (l.map (f · x)).prod) s x =
      ∑ i : Fin l.length, ((l.take i).map (f · x)).prod •
        smulRight (fderivWithin 𝕜 (fun x ↦ f l[i] x) s x) ((l.drop (.succ i)).map (f · x)).prod :=
  (HasFDerivWithinAt.list_prod' fun i hi ↦ (h i hi).hasFDerivWithinAt).fderivWithin hxs

Fréchet Derivative Within a Set of a Finite Product of Differentiable Functions

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ a normed space over $\mathbb{K}$, $\iota$ an index type, and $s \subseteq E$ a subset. Given a list $l$ of elements of $\iota$ and a point $x \in E$ where $s$ is uniquely differentiable at $x$, suppose that for each $i \in l$, the function $f_i : E \to \mathbb{A}$ is differentiable within $s$ at $x$. Then the Fréchet derivative within $s$ at $x$ of the product function $x \mapsto \prod_{i \in l} f_i(x)$ is given by \[ \sum_{i=1}^{|l|} \left( \prod_{j < i} f_j(x) \right) \cdot \left( \text{fderivWithin}_{\mathbb{K}} (f_i) s x \right) \cdot \left( \prod_{j > i} f_j(x) \right), \] where $|l|$ denotes the length of the list $l$.

HasStrictFDerivAt.multiset_prod theorem

 [DecidableEq ι] {u : Multiset ι} {x : E} (h : ∀ i ∈ u, HasStrictFDerivAt (g i ·) (g' i) x) :
  HasStrictFDerivAt (fun x ↦ (u.map (g · x)).prod) (u.map fun i ↦ ((u.erase i).map (g · x)).prod • g' i).sum x

Full source

@[fun_prop]
theorem HasStrictFDerivAt.multiset_prod [DecidableEq ι] {u : Multiset ι} {x : E}
    (h : ∀ i ∈ u, HasStrictFDerivAt (g i ·) (g' i) x) :
    HasStrictFDerivAt (fun x ↦ (u.map (g · x)).prod)
      (u.map fun i ↦ ((u.erase i).map (g · x)).prod • g' i).sum x := by
  simp only [← Multiset.attach_map_val u, Multiset.map_map]
  exact .congr_fderiv
    (hasStrictFDerivAt_multiset_prod.comp x <|
      hasStrictFDerivAt_pi.mpr fun i ↦ h (Subtype.val i) i.prop :)
    (by ext; simp [Finset.sum_multiset_map_count, u.erase_attach_map (g · x)])

Strict Fréchet Differentiability of Finite Multiset Product in Normed Algebras

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ be a normed space over $\mathbb{K}$, and $\iota$ be a finite type with decidable equality. Given a multiset $u$ of elements in $\iota$ and a family of functions $g_i \colon E \to \mathbb{A}'$ for $i \in \iota$, where $\mathbb{A}'$ is a normed commutative algebra over $\mathbb{K}$, suppose that for each $i \in u$, the function $g_i$ has a strict Fréchet derivative $g'_i$ at a point $x \in E$. Then the product function $x \mapsto \prod_{i \in u} g_i(x)$ has a strict Fréchet derivative at $x$ given by the sum \[ \sum_{i \in u} \left( \prod_{j \in u \setminus \{i\}} g_j(x) \right) \cdot g'_i. \]

HasFDerivAt.multiset_prod theorem

 [DecidableEq ι] {u : Multiset ι} {x : E} (h : ∀ i ∈ u, HasFDerivAt (g i ·) (g' i) x) :
  HasFDerivAt (fun x ↦ (u.map (g · x)).prod) (u.map fun i ↦ ((u.erase i).map (g · x)).prod • g' i).sum x

Full source

/--
Unlike `HasFDerivAt.finset_prod`, supports duplicate elements.
-/
@[fun_prop]
theorem HasFDerivAt.multiset_prod [DecidableEq ι] {u : Multiset ι} {x : E}
    (h : ∀ i ∈ u, HasFDerivAt (g i ·) (g' i) x) :
    HasFDerivAt (fun x ↦ (u.map (g · x)).prod)
      (u.map fun i ↦ ((u.erase i).map (g · x)).prod • g' i).sum x := by
  simp only [← Multiset.attach_map_val u, Multiset.map_map]
  exact .congr_fderiv
    (hasFDerivAt_multiset_prod.comp x <| hasFDerivAt_pi.mpr fun i ↦ h (Subtype.val i) i.prop :)
    (by ext; simp [Finset.sum_multiset_map_count, u.erase_attach_map (g · x)])

Fréchet Differentiability of Finite Multiset Product in Normed Algebras

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ be a normed space over $\mathbb{K}$, and $\iota$ be a finite type with decidable equality. Given a multiset $u$ of elements in $\iota$ and a family of functions $g_i \colon E \to \mathbb{A}'$ for $i \in \iota$, where $\mathbb{A}'$ is a normed commutative algebra over $\mathbb{K}$, suppose that for each $i \in u$, the function $g_i$ has a Fréchet derivative $g'_i$ at a point $x \in E$. Then the product function $x \mapsto \prod_{i \in u} g_i(x)$ has a Fréchet derivative at $x$ given by the sum \[ \sum_{i \in u} \left( \prod_{j \in u \setminus \{i\}} g_j(x) \right) \cdot g'_i. \]

HasFDerivWithinAt.multiset_prod theorem

 [DecidableEq ι] {u : Multiset ι} {x : E} (h : ∀ i ∈ u, HasFDerivWithinAt (g i ·) (g' i) s x) :
  HasFDerivWithinAt (fun x ↦ (u.map (g · x)).prod) (u.map fun i ↦ ((u.erase i).map (g · x)).prod • g' i).sum s x

Full source

@[fun_prop]
theorem HasFDerivWithinAt.multiset_prod [DecidableEq ι] {u : Multiset ι} {x : E}
    (h : ∀ i ∈ u, HasFDerivWithinAt (g i ·) (g' i) s x) :
    HasFDerivWithinAt (fun x ↦ (u.map (g · x)).prod)
      (u.map fun i ↦ ((u.erase i).map (g · x)).prod • g' i).sum s x := by
  simp only [← Multiset.attach_map_val u, Multiset.map_map]
  exact .congr_fderiv
    (hasFDerivAt_multiset_prod.comp_hasFDerivWithinAt x <|
      hasFDerivWithinAt_pi.mpr fun i ↦ h (Subtype.val i) i.prop :)
    (by ext; simp [Finset.sum_multiset_map_count, u.erase_attach_map (g · x)])

Fréchet Differentiability of Finite Multiset Product Within a Set

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ be a normed space over $\mathbb{K}$, and $\iota$ be a finite type with decidable equality. Given a multiset $u$ of elements in $\iota$, a set $s \subseteq E$, a point $x \in E$, and a family of functions $g_i \colon E \to \mathbb{A}'$ for $i \in \iota$ where $\mathbb{A}'$ is a normed commutative algebra over $\mathbb{K}$, suppose that for each $i \in u$, the function $g_i$ has a Fréchet derivative $g'_i$ at $x$ within $s$. Then the product function $x \mapsto \prod_{i \in u} g_i(x)$ has a Fréchet derivative at $x$ within $s$ given by the sum \[ \sum_{i \in u} \left( \prod_{j \in u \setminus \{i\}} g_j(x) \right) \cdot g'_i. \]

fderiv_multiset_prod theorem

 [DecidableEq ι] {u : Multiset ι} {x : E} (h : ∀ i ∈ u, DifferentiableAt 𝕜 (g i ·) x) :
  fderiv 𝕜 (fun x ↦ (u.map (g · x)).prod) x = (u.map fun i ↦ ((u.erase i).map (g · x)).prod • fderiv 𝕜 (g i) x).sum

Full source

theorem fderiv_multiset_prod [DecidableEq ι] {u : Multiset ι} {x : E}
    (h : ∀ i ∈ u, DifferentiableAt 𝕜 (g i ·) x) :
    fderiv 𝕜 (fun x ↦ (u.map (g · x)).prod) x =
      (u.map fun i ↦ ((u.erase i).map (g · x)).prod • fderiv 𝕜 (g i) x).sum :=
  (HasFDerivAt.multiset_prod fun i hi ↦ (h i hi).hasFDerivAt).fderiv

Fréchet Derivative of Multiset Product in Normed Algebras

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ a normed space over $\mathbb{K}$, $\iota$ a finite type with decidable equality, and $\mathbb{A}'$ a normed commutative algebra over $\mathbb{K}$. Given a multiset $u$ of elements in $\iota$ and a point $x \in E$, suppose that for each $i \in u$, the function $g_i \colon E \to \mathbb{A}'$ is differentiable at $x$. Then the Fréchet derivative of the product function $x \mapsto \prod_{i \in u} g_i(x)$ at $x$ is given by \[ \sum_{i \in u} \left( \prod_{j \in u \setminus \{i\}} g_j(x) \right) \cdot f'_i, \] where $f'_i$ is the Fréchet derivative of $g_i$ at $x$.

fderivWithin_multiset_prod theorem

 [DecidableEq ι] {u : Multiset ι} {x : E} (hxs : UniqueDiffWithinAt 𝕜 s x)
  (h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (g i ·) s x) :
  fderivWithin 𝕜 (fun x ↦ (u.map (g · x)).prod) s x =
    (u.map fun i ↦ ((u.erase i).map (g · x)).prod • fderivWithin 𝕜 (g i) s x).sum

Full source

theorem fderivWithin_multiset_prod [DecidableEq ι] {u : Multiset ι} {x : E}
    (hxs : UniqueDiffWithinAt 𝕜 s x) (h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (g i ·) s x) :
    fderivWithin 𝕜 (fun x ↦ (u.map (g · x)).prod) s x =
      (u.map fun i ↦ ((u.erase i).map (g · x)).prod • fderivWithin 𝕜 (g i) s x).sum :=
  (HasFDerivWithinAt.multiset_prod fun i hi ↦ (h i hi).hasFDerivWithinAt).fderivWithin hxs

Fréchet Derivative of Multiset Product Within a Set

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ a normed space over $\mathbb{K}$, $\iota$ a finite type with decidable equality, and $\mathbb{A}'$ a normed commutative algebra over $\mathbb{K}$. Given a multiset $u$ of elements in $\iota$, a subset $s \subseteq E$, and a point $x \in E$ where $s$ is uniquely differentiable at $x$, suppose that for each $i \in u$, the function $g_i \colon E \to \mathbb{A}'$ is differentiable at $x$ within $s$. Then the Fréchet derivative of the product function $x \mapsto \prod_{i \in u} g_i(x)$ at $x$ within $s$ is given by \[ \sum_{i \in u} \left( \prod_{j \in u \setminus \{i\}} g_j(x) \right) \cdot f'_i, \] where $f'_i$ is the Fréchet derivative of $g_i$ at $x$ within $s$.

HasStrictFDerivAt.finset_prod theorem

 [DecidableEq ι] {x : E} (hg : ∀ i ∈ u, HasStrictFDerivAt (g i) (g' i) x) :
  HasStrictFDerivAt (∏ i ∈ u, g i ·) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) x

Full source

theorem HasStrictFDerivAt.finset_prod [DecidableEq ι] {x : E}
    (hg : ∀ i ∈ u, HasStrictFDerivAt (g i) (g' i) x) :
    HasStrictFDerivAt (∏ i ∈ u, g i ·) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) x := by
  simpa [← Finset.prod_attach u] using .congr_fderiv
    (hasStrictFDerivAt_finset_prod.comp x <| hasStrictFDerivAt_pi.mpr fun i ↦ hg i i.prop)
    (by ext; simp [Finset.prod_erase_attach (g · x), ← u.sum_attach])

Strict Fréchet Differentiability of Finite Product in Normed Commutative Algebras

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ be a normed space over $\mathbb{K}$, and $\iota$ be a finite type with decidable equality. Given a finite set $u \subseteq \iota$ and a family of functions $g_i \colon E \to \mathbb{A}$ for $i \in u$, where $\mathbb{A}$ is a normed commutative algebra over $\mathbb{K}$, suppose each $g_i$ has a strict Fréchet derivative $g'_i$ at a point $x \in E$. Then the product function $x \mapsto \prod_{i \in u} g_i(x)$ has a strict Fréchet derivative at $x$ given by \[ \sum_{i \in u} \left( \prod_{j \in u \setminus \{i\}} g_j(x) \right) \cdot g'_i. \]

HasFDerivAt.finset_prod theorem

 [DecidableEq ι] {x : E} (hg : ∀ i ∈ u, HasFDerivAt (g i) (g' i) x) :
  HasFDerivAt (∏ i ∈ u, g i ·) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) x

Full source

theorem HasFDerivAt.finset_prod [DecidableEq ι] {x : E}
    (hg : ∀ i ∈ u, HasFDerivAt (g i) (g' i) x) :
    HasFDerivAt (∏ i ∈ u, g i ·) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) x := by
  simpa [← Finset.prod_attach u] using .congr_fderiv
    (hasFDerivAt_finset_prod.comp x <| hasFDerivAt_pi.mpr fun i ↦ hg (Subtype.val i) i.prop :)
    (by ext; simp [Finset.prod_erase_attach (g · x), ← u.sum_attach])

Fréchet Derivative of Finite Product of Differentiable Functions

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ a normed space over $\mathbb{K}$, and $\mathbb{A}$ a normed commutative algebra over $\mathbb{K}$. Given a finite set $u$ with decidable equality, a family of functions $g_i \colon E \to \mathbb{A}$ for $i \in u$, and a point $x \in E$, suppose each $g_i$ has a Fréchet derivative $g'_i$ at $x$. Then the product function $x \mapsto \prod_{i \in u} g_i(x)$ has a Fréchet derivative at $x$ given by \[ \sum_{i \in u} \left( \prod_{j \in u \setminus \{i\}} g_j(x) \right) \cdot g'_i. \]

HasFDerivWithinAt.finset_prod theorem

 [DecidableEq ι] {x : E} (hg : ∀ i ∈ u, HasFDerivWithinAt (g i) (g' i) s x) :
  HasFDerivWithinAt (∏ i ∈ u, g i ·) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) s x

Full source

theorem HasFDerivWithinAt.finset_prod [DecidableEq ι] {x : E}
    (hg : ∀ i ∈ u, HasFDerivWithinAt (g i) (g' i) s x) :
    HasFDerivWithinAt (∏ i ∈ u, g i ·) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) s x := by
  simpa [← Finset.prod_attach u] using .congr_fderiv
    (hasFDerivAt_finset_prod.comp_hasFDerivWithinAt x <|
      hasFDerivWithinAt_pi.mpr fun i ↦ hg (Subtype.val i) i.prop :)
    (by ext; simp [Finset.prod_erase_attach (g · x), ← u.sum_attach])

Fréchet Derivative of Finite Product Within a Set

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ a normed space over $\mathbb{K}$, and $\iota$ a finite type with decidable equality. Given a finite set $u \subseteq \iota$ and a family of functions $g_i \colon E \to \mathbb{A}$ for $i \in u$, where $\mathbb{A}$ is a normed commutative algebra over $\mathbb{K}$, suppose each $g_i$ has a Fréchet derivative $g'_i$ at a point $x \in E$ within a set $s \subseteq E$. Then the product function $x \mapsto \prod_{i \in u} g_i(x)$ has a Fréchet derivative at $x$ within $s$ given by \[ \sum_{i \in u} \left( \prod_{j \in u \setminus \{i\}} g_j(x) \right) \cdot g'_i. \]

fderiv_finset_prod theorem

 [DecidableEq ι] {x : E} (hg : ∀ i ∈ u, DifferentiableAt 𝕜 (g i) x) :
  fderiv 𝕜 (∏ i ∈ u, g i ·) x = ∑ i ∈ u, (∏ j ∈ u.erase i, (g j x)) • fderiv 𝕜 (g i) x

Full source

theorem fderiv_finset_prod [DecidableEq ι] {x : E} (hg : ∀ i ∈ u, DifferentiableAt 𝕜 (g i) x) :
    fderiv 𝕜 (∏ i ∈ u, g i ·) x = ∑ i ∈ u, (∏ j ∈ u.erase i, (g j x)) • fderiv 𝕜 (g i) x :=
  (HasFDerivAt.finset_prod fun i hi ↦ (hg i hi).hasFDerivAt).fderiv

Leibniz Rule for Fréchet Derivative of Finite Product of Differentiable Functions

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ a normed space over $\mathbb{K}$, and $\mathbb{A}$ a normed commutative algebra over $\mathbb{K}$. Given a finite set $u$ with decidable equality and a family of differentiable functions $g_i \colon E \to \mathbb{A}$ for $i \in u$, the Fréchet derivative of the product function $x \mapsto \prod_{i \in u} g_i(x)$ at a point $x \in E$ is given by \[ \sum_{i \in u} \left( \prod_{j \in u \setminus \{i\}} g_j(x) \right) \cdot f'(g_i)(x), \] where $f'(g_i)(x)$ denotes the Fréchet derivative of $g_i$ at $x$.

fderivWithin_finset_prod theorem

 [DecidableEq ι] {x : E} (hxs : UniqueDiffWithinAt 𝕜 s x) (hg : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (g i) s x) :
  fderivWithin 𝕜 (∏ i ∈ u, g i ·) s x = ∑ i ∈ u, (∏ j ∈ u.erase i, (g j x)) • fderivWithin 𝕜 (g i) s x

Full source

theorem fderivWithin_finset_prod [DecidableEq ι] {x : E} (hxs : UniqueDiffWithinAt 𝕜 s x)
    (hg : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (g i) s x) :
    fderivWithin 𝕜 (∏ i ∈ u, g i ·) s x =
      ∑ i ∈ u, (∏ j ∈ u.erase i, (g j x)) • fderivWithin 𝕜 (g i) s x :=
  (HasFDerivWithinAt.finset_prod fun i hi ↦ (hg i hi).hasFDerivWithinAt).fderivWithin hxs

Fréchet Derivative of Finite Product Within a Set: Leibniz Rule for Differentiable Functions

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ a normed space over $\mathbb{K}$, and $\iota$ a finite type with decidable equality. Given a finite set $u \subseteq \iota$ and a family of differentiable functions $g_i \colon E \to \mathbb{A}$ for $i \in u$, where $\mathbb{A}$ is a normed commutative algebra over $\mathbb{K}$, and a point $x \in E$ where $s \subseteq E$ is uniquely differentiable at $x$, the Fréchet derivative of the product function $x \mapsto \prod_{i \in u} g_i(x)$ within $s$ at $x$ is given by \[ \sum_{i \in u} \left( \prod_{j \in u \setminus \{i\}} g_j(x) \right) \cdot f'(g_i)(x), \] where $f'(g_i)(x)$ denotes the Fréchet derivative of $g_i$ within $s$ at $x$.

hasFDerivAt_ringInverse theorem

(x : Rˣ) : HasFDerivAt Ring.inverse (-mulLeftRight 𝕜 R ↑x⁻¹ ↑x⁻¹) x

Full source

/-- At an invertible element `x` of a normed algebra `R`, the Fréchet derivative of the inversion
operation is the linear map `fun t ↦ - x⁻¹ * t * x⁻¹`.

TODO (low prio): prove a version without assumption `[HasSummableGeomSeries R]` but within the set
of units. -/
@[fun_prop]
theorem hasFDerivAt_ringInverse (x : Rˣ) :
    HasFDerivAt Ring.inverse (-mulLeftRight 𝕜 R ↑x⁻¹ ↑x⁻¹) x :=
  have : (fun t : R => Ring.inverse (↑x + t) - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹) =o[𝓝 0] id :=
    (inverse_add_norm_diff_second_order x).trans_isLittleO (isLittleO_norm_pow_id one_lt_two)
  by simpa [hasFDerivAt_iff_isLittleO_nhds_zero] using this

Fréchet derivative of inversion at a unit: $D(\text{Ring.inverse})(x)(t) = -x^{-1} t x^{-1}$

Informal description

Let $R$ be a normed algebra over a nontrivially normed field $\mathbb{K}$ with summable geometric series, and let $x$ be a unit in $R$. The Fréchet derivative of the inversion operation $\text{Ring.inverse}$ at $x$ is the continuous linear map $t \mapsto -x^{-1} \cdot t \cdot x^{-1}$.

differentiableAt_inverse theorem

{x : R} (hx : IsUnit x) : DifferentiableAt 𝕜 (@Ring.inverse R _) x

Full source

@[fun_prop]
theorem differentiableAt_inverse {x : R} (hx : IsUnit x) :
    DifferentiableAt 𝕜 (@Ring.inverse R _) x :=
  let ⟨u, hu⟩ := hx; hu ▸ (hasFDerivAt_ringInverse u).differentiableAt

Differentiability of Ring Inversion at Units

Informal description

For any element $x$ in a normed algebra $R$ over a nontrivially normed field $\mathbb{K}$ with summable geometric series, if $x$ is a unit (i.e., invertible), then the ring inversion function $\text{Ring.inverse}$ is differentiable at $x$.

differentiableWithinAt_inverse theorem

{x : R} (hx : IsUnit x) (s : Set R) : DifferentiableWithinAt 𝕜 (@Ring.inverse R _) s x

Full source

@[fun_prop]
theorem differentiableWithinAt_inverse {x : R} (hx : IsUnit x) (s : Set R) :
    DifferentiableWithinAt 𝕜 (@Ring.inverse R _) s x :=
  (differentiableAt_inverse hx).differentiableWithinAt

Differentiability of Ring Inversion Within a Subset at Units

Informal description

Let $R$ be a normed algebra over a nontrivially normed field $\mathbb{K}$ with summable geometric series. For any unit $x \in R$ (i.e., $x$ is invertible) and any subset $s \subseteq R$, the ring inversion function $\text{Ring.inverse}$ is differentiable at $x$ within $s$.

differentiableOn_inverse theorem

: DifferentiableOn 𝕜 (@Ring.inverse R _) {x | IsUnit x}

Full source

@[fun_prop]
theorem differentiableOn_inverse : DifferentiableOn 𝕜 (@Ring.inverse R _) {x | IsUnit x} :=
  fun _x hx => differentiableWithinAt_inverse hx _

Differentiability of Ring Inversion on the Set of Units

Informal description

Let $R$ be a normed algebra over a nontrivially normed field $\mathbb{K}$ with summable geometric series. The ring inversion function $\text{Ring.inverse}$ is differentiable on the set of units $\{x \in R \mid \text{IsUnit } x\}$.

fderiv_inverse theorem

(x : Rˣ) : fderiv 𝕜 (@Ring.inverse R _) x = -mulLeftRight 𝕜 R ↑x⁻¹ ↑x⁻¹

Full source

theorem fderiv_inverse (x : Rˣ) : fderiv 𝕜 (@Ring.inverse R _) x = -mulLeftRight 𝕜 R ↑x⁻¹ ↑x⁻¹ :=
  (hasFDerivAt_ringInverse x).fderiv

Fréchet Derivative of Ring Inversion at a Unit: $D(\text{Ring.inverse})(x)(t) = -x^{-1} t x^{-1}$

Informal description

Let $R$ be a normed algebra over a nontrivially normed field $\mathbb{K}$ with summable geometric series, and let $x$ be a unit in $R$. The Fréchet derivative of the ring inversion function $\text{Ring.inverse}$ at $x$ is given by the continuous linear map $t \mapsto -x^{-1} \cdot t \cdot x^{-1}$.

hasStrictFDerivAt_ringInverse theorem

(x : Rˣ) : HasStrictFDerivAt Ring.inverse (-mulLeftRight 𝕜 R ↑x⁻¹ ↑x⁻¹) x

Full source

theorem hasStrictFDerivAt_ringInverse (x : Rˣ) :
    HasStrictFDerivAt Ring.inverse (-mulLeftRight 𝕜 R ↑x⁻¹ ↑x⁻¹) x := by
  convert (analyticAt_inverse (𝕜 := 𝕜) x).hasStrictFDerivAt
  exact (fderiv_inverse x).symm

Strict Fréchet Differentiability of Ring Inversion at a Unit: $D(\text{Ring.inverse})(x)(t) = -x^{-1} t x^{-1}$

Informal description

Let $R$ be a normed algebra over a nontrivially normed field $\mathbb{K}$ with summable geometric series, and let $x$ be a unit in $R$. The ring inversion function $\text{Ring.inverse}$ has strict Fréchet derivative at $x$ given by the continuous linear map $t \mapsto -x^{-1} \cdot t \cdot x^{-1}$.

DifferentiableWithinAt.inverse theorem

 (hf : DifferentiableWithinAt 𝕜 h S z) (hz : IsUnit (h z)) : DifferentiableWithinAt 𝕜 (fun x => Ring.inverse (h x)) S z

Full source

@[fun_prop]
theorem DifferentiableWithinAt.inverse (hf : DifferentiableWithinAt 𝕜 h S z) (hz : IsUnit (h z)) :
    DifferentiableWithinAt 𝕜 (fun x => Ring.inverse (h x)) S z :=
  (differentiableAt_inverse hz).comp_differentiableWithinAt z hf

Differentiability of Ring Inverse Composition within a Set

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $R$ a normed algebra over $\mathbb{K}$ with summable geometric series, and $h : E \to R$ a function differentiable at $z \in E$ within a set $S \subseteq E$. If $h(z)$ is a unit in $R$, then the function $x \mapsto \text{Ring.inverse}(h(x))$ is differentiable at $z$ within $S$.

DifferentiableAt.inverse theorem

(hf : DifferentiableAt 𝕜 h z) (hz : IsUnit (h z)) : DifferentiableAt 𝕜 (fun x => Ring.inverse (h x)) z

Full source

@[simp, fun_prop]
theorem DifferentiableAt.inverse (hf : DifferentiableAt 𝕜 h z) (hz : IsUnit (h z)) :
    DifferentiableAt 𝕜 (fun x => Ring.inverse (h x)) z :=
  (differentiableAt_inverse hz).comp z hf

Differentiability of Ring Inverse at a Point for Differentiable Functions

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $R$ be a normed algebra over $\mathbb{K}$ with summable geometric series, and $h : E \to R$ be a function differentiable at a point $z \in E$. If $h(z)$ is a unit in $R$, then the function $x \mapsto \text{Ring.inverse}(h(x))$ is differentiable at $z$.

DifferentiableOn.inverse theorem

 (hf : DifferentiableOn 𝕜 h S) (hz : ∀ x ∈ S, IsUnit (h x)) : DifferentiableOn 𝕜 (fun x => Ring.inverse (h x)) S

Full source

@[fun_prop]
theorem DifferentiableOn.inverse (hf : DifferentiableOn 𝕜 h S) (hz : ∀ x ∈ S, IsUnit (h x)) :
    DifferentiableOn 𝕜 (fun x => Ring.inverse (h x)) S := fun x h => (hf x h).inverse (hz x h)

Differentiability of pointwise ring inverse on a set

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $R$ a normed algebra over $\mathbb{K}$ with summable geometric series, and $h : E \to R$ a function differentiable on a set $S \subseteq E$. If for every $x \in S$, $h(x)$ is a unit in $R$, then the function $x \mapsto \text{Ring.inverse}(h(x))$ is differentiable on $S$.

Differentiable.inverse theorem

(hf : Differentiable 𝕜 h) (hz : ∀ x, IsUnit (h x)) : Differentiable 𝕜 fun x => Ring.inverse (h x)

Full source

@[simp, fun_prop]
theorem Differentiable.inverse (hf : Differentiable 𝕜 h) (hz : ∀ x, IsUnit (h x)) :
    Differentiable 𝕜 fun x => Ring.inverse (h x) := fun x => (hf x).inverse (hz x)

Differentiability of the pointwise ring inverse for globally differentiable functions

Informal description

Let $\mathbb{K}$ be a nontrivially normed field and $R$ be a normed algebra over $\mathbb{K}$ with summable geometric series. If $h : E \to R$ is a differentiable function and $h(x)$ is a unit in $R$ for every $x \in E$, then the function $x \mapsto \text{Ring.inverse}(h(x))$ is differentiable on $E$.

hasStrictFDerivAt_inv' theorem

{x : R} (hx : x ≠ 0) : HasStrictFDerivAt Inv.inv (-mulLeftRight 𝕜 R x⁻¹ x⁻¹) x

Full source

/-- At an invertible element `x` of a normed division algebra `R`, the inversion is strictly
differentiable, with derivative the linear map `fun t ↦ - x⁻¹ * t * x⁻¹`. For a nicer formula in
the commutative case, see `hasStrictFDerivAt_inv`. -/
theorem hasStrictFDerivAt_inv' {x : R} (hx : x ≠ 0) :
    HasStrictFDerivAt Inv.inv (-mulLeftRight 𝕜 R x⁻¹ x⁻¹) x := by
  simpa using hasStrictFDerivAt_ringInverse (Units.mk0 _ hx)

Strict Fréchet Differentiability of Inversion at Nonzero Elements: $D(\text{inv})(x)(t) = -x^{-1} t x^{-1}$

Informal description

Let $R$ be a normed division algebra over a nontrivially normed field $\mathbb{K}$ with summable geometric series. For any nonzero element $x \in R$, the inversion operation $\text{Inv.inv}$ has strict Fréchet derivative at $x$ given by the continuous linear map $t \mapsto -x^{-1} \cdot t \cdot x^{-1}$.

hasFDerivAt_inv' theorem

{x : R} (hx : x ≠ 0) : HasFDerivAt Inv.inv (-mulLeftRight 𝕜 R x⁻¹ x⁻¹) x

Full source

/-- At an invertible element `x` of a normed division algebra `R`, the Fréchet derivative of the
inversion operation is the linear map `fun t ↦ - x⁻¹ * t * x⁻¹`. For a nicer formula in the
commutative case, see `hasFDerivAt_inv`. -/
@[fun_prop]
theorem hasFDerivAt_inv' {x : R} (hx : x ≠ 0) :
    HasFDerivAt Inv.inv (-mulLeftRight 𝕜 R x⁻¹ x⁻¹) x := by
  simpa using hasFDerivAt_ringInverse (Units.mk0 _ hx)

Fréchet derivative of inversion at a nonzero element: $D(\text{inv})(x)(t) = -x^{-1} t x^{-1}$

Informal description

Let $R$ be a normed division algebra over a nontrivially normed field $\mathbb{K}$ with summable geometric series. For any nonzero element $x \in R$, the Fréchet derivative of the inversion operation $\text{Inv.inv}$ at $x$ is the continuous linear map $t \mapsto -x^{-1} \cdot t \cdot x^{-1}$.

differentiableAt_inv theorem

{x : R} (hx : x ≠ 0) : DifferentiableAt 𝕜 Inv.inv x

Full source

@[fun_prop]
theorem differentiableAt_inv {x : R} (hx : x ≠ 0) : DifferentiableAt 𝕜 Inv.inv x :=
  (hasFDerivAt_inv' hx).differentiableAt

Differentiability of Inversion at Nonzero Elements in Normed Division Algebras

Informal description

Let $R$ be a normed division algebra over a nontrivially normed field $\mathbb{K}$ with summable geometric series. For any nonzero element $x \in R$, the inversion operation $\text{Inv.inv}$ is differentiable at $x$.

differentiableWithinAt_inv theorem

{x : R} (hx : x ≠ 0) (s : Set R) : DifferentiableWithinAt 𝕜 (fun x => x⁻¹) s x

Full source

@[fun_prop]
theorem differentiableWithinAt_inv {x : R} (hx : x ≠ 0) (s : Set R) :
    DifferentiableWithinAt 𝕜 (fun x => x⁻¹) s x :=
  (differentiableAt_inv hx).differentiableWithinAt

Differentiability of inversion within a subset at nonzero points

Informal description

Let $R$ be a normed division algebra over a nontrivially normed field $\mathbb{K}$ with summable geometric series. For any nonzero element $x \in R$ and any subset $s \subseteq R$, the inversion function $x \mapsto x^{-1}$ is differentiable at $x$ within the set $s$.

differentiableOn_inv theorem

: DifferentiableOn 𝕜 (fun x : R => x⁻¹) {x | x ≠ 0}

Full source

@[fun_prop]
theorem differentiableOn_inv : DifferentiableOn 𝕜 (fun x : R => x⁻¹) {x | x ≠ 0} := fun _x hx =>
  differentiableWithinAt_inv hx _

Differentiability of Inversion on Nonzero Elements in Normed Division Algebras

Informal description

Let $R$ be a normed division algebra over a nontrivially normed field $\mathbb{K}$ with summable geometric series. The inversion function $x \mapsto x^{-1}$ is differentiable on the set $\{x \in R \mid x \neq 0\}$.

fderiv_inv' theorem

{x : R} (hx : x ≠ 0) : fderiv 𝕜 Inv.inv x = -mulLeftRight 𝕜 R x⁻¹ x⁻¹

Full source

/-- Non-commutative version of `fderiv_inv` -/
theorem fderiv_inv' {x : R} (hx : x ≠ 0) : fderiv 𝕜 Inv.inv x = -mulLeftRight 𝕜 R x⁻¹ x⁻¹ :=
  (hasFDerivAt_inv' hx).fderiv

Fréchet Derivative of Inversion at Nonzero Point: $D(\text{inv})(x)(t) = -x^{-1} t x^{-1}$

Informal description

Let $R$ be a normed division algebra over a nontrivially normed field $\mathbb{K}$ with summable geometric series. For any nonzero element $x \in R$, the Fréchet derivative of the inversion operation $\text{Inv.inv}$ at $x$ is given by the continuous linear map $t \mapsto -x^{-1} \cdot t \cdot x^{-1}$.

fderivWithin_inv' theorem

 {s : Set R} {x : R} (hx : x ≠ 0) (hxs : UniqueDiffWithinAt 𝕜 s x) :
  fderivWithin 𝕜 (fun x => x⁻¹) s x = -mulLeftRight 𝕜 R x⁻¹ x⁻¹

Full source

/-- Non-commutative version of `fderivWithin_inv` -/
theorem fderivWithin_inv' {s : Set R} {x : R} (hx : x ≠ 0) (hxs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 (fun x => x⁻¹) s x = -mulLeftRight 𝕜 R x⁻¹ x⁻¹ := by
  rw [DifferentiableAt.fderivWithin (differentiableAt_inv hx) hxs]
  exact fderiv_inv' hx

Fréchet Derivative of Inversion Within a Set at Nonzero Points: $D(\text{inv}_s)(x)(t) = -x^{-1} t x^{-1}$

Informal description

Let $R$ be a normed division algebra over a nontrivially normed field $\mathbb{K}$ with summable geometric series, and let $s \subseteq R$ be a subset. For any nonzero element $x \in s$ where $s$ is uniquely differentiable at $x$ (i.e., the tangent cone at $x$ spans a dense subspace of $R$), the Fréchet derivative of the inversion operation $x \mapsto x^{-1}$ within $s$ at $x$ is given by the continuous linear map $t \mapsto -x^{-1} \cdot t \cdot x^{-1}$.

DifferentiableWithinAt.inv theorem

(hf : DifferentiableWithinAt 𝕜 h S z) (hz : h z ≠ 0) : DifferentiableWithinAt 𝕜 (fun x => (h x)⁻¹) S z

Full source

@[fun_prop]
theorem DifferentiableWithinAt.inv (hf : DifferentiableWithinAt 𝕜 h S z) (hz : h z ≠ 0) :
    DifferentiableWithinAt 𝕜 (fun x => (h x)⁻¹) S z :=
  (differentiableAt_inv hz).comp_differentiableWithinAt z hf

Differentiability of Pointwise Inverse within a Set at a Point

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $R$ a normed division algebra over $\mathbb{K}$ with summable geometric series, and $h : E \to R$ a function. If $h$ is differentiable at $z \in E$ within a set $S \subseteq E$ and $h(z) \neq 0$, then the function $x \mapsto (h(x))^{-1}$ is differentiable at $z$ within $S$.

DifferentiableAt.inv theorem

(hf : DifferentiableAt 𝕜 h z) (hz : h z ≠ 0) : DifferentiableAt 𝕜 (fun x => (h x)⁻¹) z

Full source

@[simp, fun_prop]
theorem DifferentiableAt.inv (hf : DifferentiableAt 𝕜 h z) (hz : h z ≠ 0) :
    DifferentiableAt 𝕜 (fun x => (h x)⁻¹) z :=
  (differentiableAt_inv hz).comp z hf

Differentiability of Pointwise Inversion at Nonzero Points

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $R$ be a normed division algebra over $\mathbb{K}$ with summable geometric series, and $h : E \to R$ be a function differentiable at a point $z \in E$. If $h(z) \neq 0$, then the function $x \mapsto (h(x))^{-1}$ is differentiable at $z$.

DifferentiableOn.inv theorem

(hf : DifferentiableOn 𝕜 h S) (hz : ∀ x ∈ S, h x ≠ 0) : DifferentiableOn 𝕜 (fun x => (h x)⁻¹) S

Full source

@[fun_prop]
theorem DifferentiableOn.inv (hf : DifferentiableOn 𝕜 h S) (hz : ∀ x ∈ S, h x ≠ 0) :
    DifferentiableOn 𝕜 (fun x => (h x)⁻¹) S := fun x h => (hf x h).inv (hz x h)

Differentiability of Pointwise Inverse on a Set

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $R$ a normed division algebra over $\mathbb{K}$ with summable geometric series, and $h : E \to R$ a function. If $h$ is differentiable on a set $S \subseteq E$ and $h(x) \neq 0$ for all $x \in S$, then the function $x \mapsto (h(x))^{-1}$ is differentiable on $S$.

Differentiable.inv theorem

(hf : Differentiable 𝕜 h) (hz : ∀ x, h x ≠ 0) : Differentiable 𝕜 fun x => (h x)⁻¹

Full source

@[simp, fun_prop]
theorem Differentiable.inv (hf : Differentiable 𝕜 h) (hz : ∀ x, h x ≠ 0) :
    Differentiable 𝕜 fun x => (h x)⁻¹ := fun x => (hf x).inv (hz x)

Differentiability of the Pointwise Inverse of a Nonvanishing Differentiable Function

Informal description

Let $\mathbb{K}$ be a nontrivially normed field and $R$ be a normed division algebra over $\mathbb{K}$ with summable geometric series. If $h : E \to R$ is a differentiable function such that $h(x) \neq 0$ for all $x \in E$, then the function $x \mapsto (h(x))^{-1}$ is differentiable on $E$.