Physlib

Physlib.Mathematics.FDerivCurry

fderiv currying lemmas

Various lemmas related to fderiv on curried/uncurried functions.

24 declarations

theorem

The Total Derivative of an Uncurried Function is the Sum of its Partial Derivatives

Let k\mathbf{k} be a nontrivially normed field, and let X,Y,ZX, Y, Z be normed spaces over k\mathbf{k}. Let f:X→Y→Zf: X \to Y \to Z be a curried function and F:X×Y→ZF: X \times Y \to Z be its uncurried version, defined by F(x,y)=f(x)(y)F(x, y) = f(x)(y). If FF is differentiable at (x,y)(x, y), then for any vector (dx,dy)∈X×Y(dx, dy) \in X \times Y, the Fréchet derivative DF(x,y)DF(x, y) applied to (dx,dy)(dx, dy) is given by the sum of the partial derivatives: DF(x,y)(dx,dy)=D(x′↦f(x′,y))(x)(dx)+D(y′↦f(x,y′))(y)(dy)DF(x, y)(dx, dy) = D(x' \mapsto f(x', y))(x)(dx) + D(y' \mapsto f(x, y'))(y)(dy) where D(x′↦f(x′,y))(x)D(x' \mapsto f(x', y))(x) denotes the derivative of ff with respect to the first argument at xx, and D(y′↦f(x,y′))(y)D(y' \mapsto f(x, y'))(y) denotes the derivative of ff with respect to the second argument at yy.

theorem

The partial derivative of f(x,y)f(x, y) with respect to xx equals Df(x,y)(dx,0)Df(x, y)(dx, 0)

Let k\mathbf{k} be a nontrivially normed field, and let X,Y,ZX, Y, Z be normed spaces over k\mathbf{k}. Let f:X×Y→Zf: X \times Y \to Z be a function that is differentiable at (x,y)∈X×Y(x, y) \in X \times Y. Then for any vector dx∈Xdx \in X, the Fréchet derivative of the function x′↦f(x′,y)x' \mapsto f(x', y) at xx applied to dxdx is equal to the Fréchet derivative of ff at (x,y)(x, y) applied to the vector (dx,0)(dx, 0): D(x′↦f(x′,y))(x)(dx)=Df(x,y)(dx,0)D(x' \mapsto f(x', y))(x)(dx) = Df(x, y)(dx, 0)

theorem

The Fréchet Derivative of the Second Partial Map is the Total Derivative at (0,dy)(0, dy)

Let k\mathbf{k} be a nontrivially normed field, and let X,Y,ZX, Y, Z be normed spaces over k\mathbf{k}. Let f:X×Y→Zf: X \times Y \to Z be a function. If ff is differentiable at (x,y)∈X×Y(x, y) \in X \times Y, then for any vector dy∈Ydy \in Y, the Fréchet derivative of the partial map y′↦f(x,y′)y' \mapsto f(x, y') evaluated at yy and applied to dydy is equal to the total Fréchet derivative of ff at (x,y)(x, y) applied to the vector (0,dy)(0, dy): D(y′↦f(x,y′))(y)(dy)=Df(x,y)(0,dy)D(y' \mapsto f(x, y'))(y)(dy) = Df(x, y)(0, dy)

theorem

DF=(Dxf∘π1)+(Dyf∘π2)DF = (D_x f \circ \pi_1) + (D_y f \circ \pi_2) for uncurried functions

Let k\mathbf{k} be a nontrivially normed field, and let X,Y,ZX, Y, Z be normed spaces over k\mathbf{k}. Let f:X→Y→Zf: X \to Y \to Z be a function and let F:X×Y→ZF: X \times Y \to Z be its uncurried version, defined by F(x,y)=f(x)(y)F(x, y) = f(x)(y). If FF is differentiable, then its Fréchet derivative DFDF is given by the map: DF=(x,y)↦D(x′↦f(x′,y))(x)∘π1+D(y′↦f(x,y′))(y)∘π2DF = (x, y) \mapsto D(x' \mapsto f(x', y))(x) \circ \pi_1 + D(y' \mapsto f(x, y'))(y) \circ \pi_2 where π1:X×Y→X\pi_1: X \times Y \to X and π2:X×Y→Y\pi_2: X \times Y \to Y are the canonical projections from the product space, and D(x′↦f(x′,y))(x)D(x' \mapsto f(x', y))(x) and D(y′↦f(x,y′))(y)D(y' \mapsto f(x, y'))(y) denote the partial derivatives with respect to the first and second arguments, respectively.

theorem

The Total Derivative on a Product Space is the Sum of Partial Derivatives Composed with Projections

Let k\mathbf{k} be a nontrivially normed field, and let X,Y,ZX, Y, Z be normed spaces over k\mathbf{k}. Let f:X×Y→Zf: X \times Y \to Z be a function that is differentiable at a point (x,y)∈X×Y(x, y) \in X \times Y. Then the Fréchet derivative of ff at (x,y)(x, y), denoted by Df(x,y)Df(x, y), is equal to the sum of its partial derivatives composed with the coordinate projections: Df(x,y)=D(x′↦f(x′,y))(x)∘π1+D(y′↦f(x,y′))(y)∘π2Df(x, y) = D(x' \mapsto f(x', y))(x) \circ \pi_1 + D(y' \mapsto f(x, y'))(y) \circ \pi_2 where π1:X×Y→X\pi_1: X \times Y \to X and π2:X×Y→Y\pi_2: X \times Y \to Y are the canonical continuous linear projections onto the first and second factors, respectively.

theorem

Df=(Dxf∘π1)+(Dyf∘π2)Df = (D_x f \circ \pi_1) + (D_y f \circ \pi_2) for functions on product spaces

Let k\mathbf{k} be a nontrivially normed field, and let X,Y,ZX, Y, Z be normed spaces over k\mathbf{k}. Let f:X×Y→Zf: X \times Y \to Z be a differentiable function. The Fréchet derivative of ff, denoted by DfDf, is given by the map: Df(x,y)=D(x′↦f(x′,y))(x)∘π1+D(y′↦f(x,y′))(y)∘π2Df(x, y) = D(x' \mapsto f(x', y))(x) \circ \pi_1 + D(y' \mapsto f(x, y'))(y) \circ \pi_2 where π1:X×Y→X\pi_1: X \times Y \to X and π2:X×Y→Y\pi_2: X \times Y \to Y are the canonical continuous linear projections onto the first and second factors, respectively. Here D(x′↦f(x′,y))(x)D(x' \mapsto f(x', y))(x) and D(y′↦f(x,y′))(y)D(y' \mapsto f(x, y'))(y) represent the partial derivatives with respect to the first and second variables at the point (x,y)(x, y).

theorem

Df(x)(dx)(y)=D(x↦f(x)y)(x)(dx)Df(x)(dx)(y) = D(x \mapsto f(x)y)(x)(dx)

Let XX, YY, and ZZ be normed spaces over a field k\mathbb{k}. Let f:X→Lk(Y,Z)f: X \to \mathcal{L}_{\mathbb{k}}(Y, Z) be a function that is differentiable at x∈Xx \in X, where Lk(Y,Z)\mathcal{L}_{\mathbb{k}}(Y, Z) denotes the space of continuous linear maps from YY to ZZ. For any y∈Yy \in Y and any vector dx∈Xdx \in X, the Fréchet derivative of ff at xx applied to dxdx and then evaluated at yy is equal to the Fréchet derivative of the map x↦f(x)yx \mapsto f(x)y at xx applied to dxdx: Df(x)(dx)(y)=D(x↦f(x)y)(x)(dx) Df(x)(dx)(y) = D(x \mapsto f(x)y)(x)(dx)

theorem

Chain Rule for the Derivative of an Uncurried Function in the First Variable

Let X,Y,ZX, Y, Z be normed spaces over a field k\mathbb{k}, and let f:X→Y→Zf: X \to Y \to Z be a function. Let f^:X×Y→Z\hat{f} : X \times Y \to Z denote the uncurried version of ff (where f^(x,y)=f(x)(y)\hat{f}(x, y) = f(x)(y)). If f^\hat{f} is differentiable, then for any fixed y∈Yy \in Y, the Fréchet derivative of the partial function x↦f^(x,y)x \mapsto \hat{f}(x, y) is equal to the composition of the Fréchet derivative of f^\hat{f} and the Fréchet derivative of the inclusion map x↦(x,y)x \mapsto (x, y). That is: D(x↦f^(x,y))=x↦Df^(x,y)∘D(x↦(x,y)) D(x \mapsto \hat{f}(x, y)) = x \mapsto D\hat{f}(x, y) \circ D(x \mapsto (x, y)) where DD denotes the Fréchet derivative `fderiv 𝕜`.

theorem

Chain Rule for the Derivative of an Uncurried Function in the Second Variable

Let X,Y,X, Y, and ZZ be normed spaces over a field k\mathbb{k}, and let f:X→Y→Zf: X \to Y \to Z be a function. Let f^:X×Y→Z\hat{f} : X \times Y \to Z denote the uncurried version of ff (where f^(x,y)=f(x)(y)\hat{f}(x, y) = f(x)(y)). If f^\hat{f} is differentiable, then for any fixed x∈Xx \in X, the Fréchet derivative of the partial function y↦f^(x,y)y \mapsto \hat{f}(x, y) is equal to the composition of the Fréchet derivative of f^\hat{f} and the Fréchet derivative of the inclusion map y↦(x,y)y \mapsto (x, y). That is: D(y↦f^(x,y))=y↦Df^(x,y)∘D(y↦(x,y)) D(y \mapsto \hat{f}(x, y)) = y \mapsto D\hat{f}(x, y) \circ D(y \mapsto (x, y)) where DD denotes the Fréchet derivative `fderiv 𝕜`.

theorem

Value of the Partial Fréchet Derivative in the First Variable

Let X,Y,ZX, Y, Z be normed spaces over a field k\mathbb{k} and f:X→Y→Zf: X \to Y \to Z be a function. Let f^:X×Y→Z\hat{f}: X \times Y \to Z denote the uncurried version of ff, defined by f^(x,y)=f(x)(y)\hat{f}(x, y) = f(x)(y). If f^\hat{f} is differentiable, then for any x,dx∈Xx, dx \in X and y∈Yy \in Y, the value of the Fréchet derivative of the partial map x′↦f(x′,y)x' \mapsto f(x', y) at the point xx applied to the vector dxdx is given by: (D(x′↦f(x′,y))(x))(dx)=(Df^(x,y))((D(x′↦(x′,y))(x))(dx)) (D(x' \mapsto f(x', y))(x))(dx) = (D\hat{f}(x, y)) ((D(x' \mapsto (x', y))(x))(dx)) where DD denotes the Fréchet derivative `fderiv 𝕜`.

theorem

The Fréchet derivative of y↦f(x,y)y \mapsto f(x, y) equals the derivative of the uncurried function composed with the derivative of y↦(x,y)y \mapsto (x, y)

Let k\mathbb{k} be a normed field and X,Y,ZX, Y, Z be normed spaces over k\mathbb{k}. Let f:X→Y→Zf: X \to Y \to Z be a function such that its uncurried form f~:X×Y→Z\tilde{f}: X \times Y \to Z (defined by (x,y)↦f(x)(y)(x, y) \mapsto f(x)(y)) is differentiable. For any fixed x∈Xx \in X and points y,dy∈Yy, dy \in Y, the Fréchet derivative of the partial map y′↦f(x)(y′)y' \mapsto f(x)(y') at yy applied to the increment dydy is given by: (D(y′↦f(x,y′))∣y)(dy)=Df~(x,y)((D(y′↦(x,y′))∣y)(dy)) \left( D(y' \mapsto f(x, y')) \big|_y \right) (dy) = D\tilde{f}(x, y) \left( \left( D(y' \mapsto (x, y')) \big|_y \right) (dy) \right) where DD denotes the Fréchet derivative.

theorem

The Fréchet derivative of y′↦(x,y′)y' \mapsto (x, y') is inr\text{inr}

For any x∈Xx \in X and y∈Yy \in Y, the Fréchet derivative of the map y′↦(x,y′)y' \mapsto (x, y') at the point yy is the canonical continuous linear injection of the second factor into the product, inr:Y→X×Y\text{inr} : Y \to X \times Y, which is defined by dy↦(0,dy)dy \mapsto (0, dy).

theorem

The Fréchet derivative of x↦(x,y)x \mapsto (x, y) is inl\text{inl}

Let k\mathbb{k} be a normed field and X,YX, Y be normed spaces over k\mathbb{k}. For any fixed y∈Yy \in Y, the Fréchet derivative of the map x↦(x,y)x \mapsto (x, y) at any point x∈Xx \in X is equal to the canonical continuous linear inclusion inl:X→X×Y\text{inl} : X \to X \times Y, which is defined by v↦(v,0)v \mapsto (v, 0).

theorem

Differentiability of (x,y)↦f(x,y)  ⟹  (x, y) \mapsto f(x, y) \implies differentiability of x↦f(x,y)x \mapsto f(x, y) at xx

Let k\mathbb{k} be a normed field and X,Y,ZX, Y, Z be normed spaces over k\mathbb{k}. If a function f:X→Y→Zf: X \to Y \to Z is such that its uncurried version (x,y)↦f(x,y)(x, y) \mapsto f(x, y) is differentiable, then for any fixed y∈Yy \in Y and any point x∈Xx \in X, the partial map x′↦f(x′,y)x' \mapsto f(x', y) is differentiable at xx.

theorem

Differentiability of an uncurried function implies differentiability in its second argument

Let k\mathbb{k} be a normed field and X,Y,ZX, Y, Z be normed spaces over k\mathbb{k}. Let f:X→(Y→Z)f : X \to (Y \to Z) be a function. If the uncurried function (x,y)↦f(x,y)(x, y) \mapsto f(x, y) is differentiable on X×YX \times Y, then for any fixed x∈Xx \in X, the map y′↦f(x,y′)y' \mapsto f(x, y') is differentiable at the point y∈Yy \in Y.

theorem

The partial derivative of a C2C^2 function with respect to its first argument is differentiable.

Let k\mathbb{k} be a scalar field, and let X,YX, Y, and ZZ be normed spaces over k\mathbb{k}. Let f:X×Y→Zf: X \times Y \to Z be a function (represented in the formal statement as the uncurrying of f:X→Y→Zf: X \to Y \to Z). If ff is C2C^2 (twice continuously differentiable), then for any fixed y∈Yy \in Y, the Fréchet derivative of the partial map x↦f(x,y)x \mapsto f(x, y) is differentiable.

theorem

If ff is C2C^2, then y↦D2f(x,y)y \mapsto D_2 f(x, y) is differentiable

Let f:X→Y→Zf: X \to Y \to Z be a function between normed vector spaces over a field k\mathbb{k}. If the uncurried function (x,y)↦f(x,y)(x, y) \mapsto f(x, y) is twice continuously differentiable (C2C^2), then for any fixed x∈Xx \in X, the map y↦Dyf(x,y)y \mapsto D_y f(x, y), which assigns to each yy the Fréchet derivative of the partial function y′↦f(x,y′)y' \mapsto f(x, y'), is differentiable.

theorem

The partial derivative y↦D1f(x,y)y \mapsto D_1 f(x, y) of a C2C^2 function is differentiable

Let k\mathbb{k} be a normed field, and X,Y,ZX, Y, Z be normed spaces over k\mathbb{k}. Let f:X×Y→Zf: X \times Y \to Z be a function whose uncurried form (x,y)↦f(x,y)(x, y) \mapsto f(x, y) is twice continuously Fréchet differentiable (C2C^2). For any fixed x∈Xx \in X, the mapping y↦D1f(x,y)y \mapsto D_1 f(x, y) is differentiable, where D1f(x,y)D_1 f(x, y) denotes the Fréchet derivative of the partial map x′↦f(x′,y)x' \mapsto f(x', y) evaluated at xx.

theorem

f∈C2  ⟹  y↦D1f(x,y)(δx)f \in C^2 \implies y \mapsto D_1 f(x, y)(\delta x) is differentiable

Let k\mathbb{k} be a normed field, and X,Y,ZX, Y, Z be normed spaces over k\mathbb{k}. Let f:X×Y→Zf: X \times Y \to Z be a function such that its uncurried form (x,y)↦f(x,y)(x, y) \mapsto f(x, y) is twice continuously Fréchet differentiable (C2C^2). For any fixed x∈Xx \in X and direction vector δx∈X\delta x \in X, the mapping y↦(D1f(x,y))(δx)y \mapsto (D_1 f(x, y))(\delta x) is differentiable with respect to yy, where D1f(x,y)D_1 f(x, y) denotes the Fréchet derivative of the partial map x′↦f(x′,y)x' \mapsto f(x', y) evaluated at xx.

theorem

f∈C2f \in C^2 implies x↦Dyf(x,y)x \mapsto D_y f(x, y) is differentiable

Let X,YX, Y, and ZZ be normed spaces over a field k\mathbb{k}. Let f:X×Y→Zf: X \times Y \to Z be a function such that its uncurried form (x,y)↦f(x,y)(x, y) \mapsto f(x, y) is twice continuously differentiable (C2C^2). For any fixed y∈Yy \in Y, the function that maps xx to the Fréchet derivative of the partial map y′↦f(x,y′)y' \mapsto f(x, y') evaluated at yy is differentiable with respect to xx.

theorem

f∈C2f \in C^2 implies x↦Dyf(x,y)(δy)x \mapsto D_y f(x, y)(\delta y) is differentiable

Let X,YX, Y, and ZZ be normed spaces over a field k\mathbb{k}. Let f:X×Y→Zf: X \times Y \to Z be a function such that its uncurried form (x,y)↦f(x,y)(x, y) \mapsto f(x, y) is twice continuously differentiable (C2C^2). For any fixed y∈Yy \in Y and δy∈Y\delta y \in Y, the function that maps xx to the Fréchet derivative of the partial map y′↦f(x,y′)y' \mapsto f(x, y') evaluated at yy and then applied to the vector δy\delta y is differentiable with respect to xx.

theorem

f∈C2  ⟹  y↦D1f(x,y)(dx)f \in C^2 \implies y \mapsto D_1 f(x, y)(dx) is differentiable at yy

Let k\mathbb{k} be a normed field, and X,Y,ZX, Y, Z be normed spaces over k\mathbb{k}. Let f:X×Y→Zf: X \times Y \to Z be a function such that its uncurried form (x,y)↦f(x,y)(x, y) \mapsto f(x, y) is twice continuously Fréchet differentiable (C2C^2). For any fixed x∈Xx \in X and direction vector dx∈Xdx \in X, the mapping y′↦(D1f(x,y′))(dx)y' \mapsto (D_1 f(x, y'))(dx) is differentiable at y∈Yy \in Y, where D1f(x,y′)D_1 f(x, y') denotes the Fréchet derivative of the partial map x′↦f(x′,y′)x' \mapsto f(x', y') evaluated at xx.

theorem

f∈C2f \in C^2 implies x↦Dyf(x,y)(δy)x \mapsto D_y f(x, y)(\delta y) is differentiable at xx

Let X,YX, Y, and ZZ be normed spaces over a field k\mathbb{k}. Let f:X×Y→Zf: X \times Y \to Z be a function such that its uncurried form (x,y)↦f(x,y)(x, y) \mapsto f(x, y) is twice continuously differentiable (C2C^2). For any fixed y∈Yy \in Y and vector δy∈Y\delta y \in Y, the function that maps x′x' to the Fréchet derivative of the partial map y′↦f(x′,y′)y' \mapsto f(x', y') evaluated at yy and applied to the vector δy\delta y is differentiable at xx.

theorem

Symmetry of mixed partial Fréchet derivatives for C2C^2 functions

Let k\mathbb{k} be a normed field that is either the real numbers R\mathbb{R} or the complex numbers C\mathbb{C}. Let X,Y,X, Y, and ZZ be normed spaces over k\mathbb{k}. Suppose f:X×Y→Zf: X \times Y \to Z is a twice continuously Fréchet differentiable (C2C^2) function. For any points x∈X,y∈Yx \in X, y \in Y and vectors dx∈X,dy∈Ydx \in X, dy \in Y, the mixed partial derivatives commute: D1(x′↦D2f(x′,y)(dy))(x)(dx)=D2(y′↦D1f(x,y′)(dx))(y)(dy) D_1 (x' \mapsto D_2 f(x', y)(dy))(x)(dx) = D_2 (y' \mapsto D_1 f(x, y')(dx))(y)(dy) where D1D_1 denotes the partial Fréchet derivative with respect to the first variable and D2D_2 denotes the partial Fréchet derivative with respect to the second variable.