PhyslibSearch

Physlib.Mathematics.VariationalCalculus.HasVarAdjDeriv

32 declarations

theorem

Smoothness of F(v)F(v) from existence of variational adjoint derivative of FF

#apply_smooth_of_smooth

Let F:(XU)(XV)F: (X \to U) \to (X \to V) be an operator between function spaces that possesses a variational adjoint derivative FF' at uu. If v:XUv: X \to U is a smooth function (of class CC^\infty), then its image under the operator FF, given by F(v):XVF(v): X \to V, is also a smooth function.

theorem

Smoothness of F(u)F(u) from existence of variational adjoint derivative at uu

#apply_smooth_self

Let F:(XU)(XV)F: (X \to U) \to (X \to V) be an operator between function spaces. Suppose FF possesses a variational adjoint derivative FF' at a function u:XUu: X \to U. Then the function F(u):XVF(u): X \to V is infinitely differentiable (of class CC^\infty).

theorem

sF(ϕ(s,))(x)s \mapsto F(\phi(s, \cdot))(x) is CC^\infty for smooth families ϕ\phi and operators with variational adjoint derivatives

#smooth_R

Suppose an operator F:(XU)(XV)F: (X \to U) \to (X \to V) has a variational adjoint derivative at a function u:XUu: X \to U. Let ϕ:R×XU\phi: \mathbb{R} \times X \to U be an infinitely differentiable (CC^\infty) family of functions, where the mapping (s,x)ϕ(s,x)(s, x) \mapsto \phi(s, x) is smooth. Then, for any fixed point xXx \in X, the function mapping the parameter sRs \in \mathbb{R} to the value of the operator FF evaluated at the function ϕ(s,)\phi(s, \cdot) and then evaluated at xx, given by sF(ϕ(s,))(x), s \mapsto F(\phi(s, \cdot))(x), is infinitely differentiable (CC^\infty) with respect to ss.

theorem

sF(u0+sδu)(x)s \mapsto F(u_0 + s \delta u)(x) is CC^\infty for operators with variational adjoint derivatives

#smooth_linear

Suppose an operator F:(XU)(XV)F: (X \to U) \to (X \to V) has a variational adjoint derivative at u:XUu: X \to U. Let ϕ:R×XU\phi: \mathbb{R} \times X \to U be an infinitely differentiable (CC^\infty) family of functions. Let u0:XUu_0: X \to U be the function u0(x)=ϕ(0,x)u_0(x) = \phi(0, x) and let δu:XU\delta u: X \to U be the partial derivative of ϕ\phi with respect to its first argument at 00, given by δu(x)=ϕ(s,x)ss=0\delta u(x) = \left. \frac{\partial \phi(s, x)}{\partial s} \right|_{s=0}. Then, for any fixed point xXx \in X, the function mapping sRs' \in \mathbb{R} to the value of the operator FF evaluated at the linear variation u0+sδuu_0 + s' \delta u and then evaluated at xx, given by sF(u0+sδu)(x), s' \mapsto F(u_0 + s' \delta u)(x), is infinitely differentiable (CC^\infty) with respect to ss'.

theorem

sF(u+sδu)(x)s \mapsto F(u + s \delta u)(x) is CC^\infty for operators with variational adjoint derivatives

#smooth_adjoint

Suppose an operator F:(XU)(XV)F: (X \to U) \to (X \to V) has a variational adjoint derivative at the function u:XUu: X \to U. Then, for any infinitely differentiable (smooth) function δu:XU\delta u: X \to U and any fixed point xXx \in X, the function mapping sRs \in \mathbb{R} to the value of the operator at the perturbed function u+sδuu + s \delta u evaluated at xx, given by sF(u+sδu)(x), s \mapsto F(u + s \delta u)(x), is infinitely differentiable (CC^\infty) with respect to ss.

theorem

sF(u0+sδu)(x)s \mapsto F(u_0 + s \delta u)(x) is differentiable for operators with variational adjoint derivatives

#differentiable_linear

Suppose an operator F:(XU)(XV)F: (X \to U) \to (X \to V) has a variational adjoint derivative at u:XUu: X \to U. Let ϕ:R×XU\phi: \mathbb{R} \times X \to U be an infinitely differentiable (CC^\infty) family of functions. Let u0:XUu_0: X \to U be the function u0(x)=ϕ(0,x)u_0(x) = \phi(0, x) and let δu:XU\delta u: X \to U be the partial derivative of ϕ\phi with respect to its first argument at s=0s=0, given by δu(x)=ϕ(s,x)ss=0\delta u(x) = \left. \frac{\partial \phi(s, x)}{\partial s} \right|_{s=0}. Then, for any fixed point xXx \in X, the function mapping sRs' \in \mathbb{R} to the value of the operator FF evaluated at the linear variation u0+sδuu_0 + s' \delta u and then evaluated at xx, given by sF(u0+sδu)(x), s' \mapsto F(u_0 + s' \delta u)(x), is differentiable with respect to ss'.

theorem

ddsF(ϕ(s))=ddsF(ϕ(0)+sϕ˙(0))\frac{d}{ds} F(\phi(s)) = \frac{d}{ds} F(\phi(0) + s \dot{\phi}(0)) for linear operators FF

#linearize_of_linear

Let F:(XU)(XV)F: (X \to U) \to (X \to V) be an operator mapping between function spaces. Suppose FF is linear on smooth functions, meaning that for all smooth ϕ1,ϕ2:XU\phi_1, \phi_2: X \to U and cRc \in \mathbb{R}, F(ϕ1+ϕ2)=F(ϕ1)+F(ϕ2)F(\phi_1 + \phi_2) = F(\phi_1) + F(\phi_2) and F(cϕ1)=cF(ϕ1)F(c \cdot \phi_1) = c \cdot F(\phi_1). Additionally, assume that for any smooth family of functions ϕ:R×XU\phi: \mathbb{R} \times X \to U, the derivative at s=0s=0 commutes with FF at any point xXx \in X: ddss=0F(ϕ(s,))(x)=F(ϕss=0)(x). \left. \frac{d}{ds} \right|_{s=0} F(\phi(s, \cdot))(x) = F\left( \left. \frac{\partial \phi}{\partial s} \right|_{s=0} \right)(x). Then, for any such smooth ϕ\phi and any xXx \in X, the derivative of FF applied to the path ϕ(s,)\phi(s, \cdot) is equal to the derivative of FF applied to the first-order linear approximation of ϕ\phi at s=0s=0: ddss=0F(ϕ(s,))(x)=ddss=0F(yϕ(0,y)+sϕss=0(y))(x). \left. \frac{d}{ds} \right|_{s=0} F(\phi(s, \cdot))(x) = \left. \frac{d}{ds} \right|_{s=0} F\left( y \mapsto \phi(0, y) + s \cdot \left. \frac{\partial \phi}{\partial s} \right|_{s=0}(y) \right)(x).

theorem

The variational adjoint of the linearization of a linear operator FF is its adjoint FF'

#deriv_adjoint_of_linear

Let F:(XU)(XV)F: (X \to U) \to (X \to V) be an operator between function spaces that is linear on the space of smooth functions, meaning F(ϕ1+ϕ2)=F(ϕ1)+F(ϕ2)F(\phi_1 + \phi_2) = F(\phi_1) + F(\phi_2) and F(cϕ)=cF(ϕ)F(c \cdot \phi) = c \cdot F(\phi) for any cRc \in \mathbb{R} and smooth functions ϕ,ϕ1,ϕ2:XU\phi, \phi_1, \phi_2: X \to U. Suppose u:XUu: X \to U is a smooth function and FF has a variational adjoint FF'. Then the linear operator that maps a variation δu:XU\delta u: X \to U to the directional derivative of FF at uu, defined by δu(xddss=0F(u+sδu)(x)), \delta u \mapsto \left( x \mapsto \left. \frac{d}{ds} \right|_{s=0} F(u + s \delta u)(x) \right), has FF' as its variational adjoint.

theorem

The Variational Adjoint Derivative of a Linear Operator is its Variational Adjoint

#hasVarAdjDerivAt_of_hasVarAdjoint_of_linear

Let F:(XU)(XV)F: (X \to U) \to (X \to V) be an operator between function spaces. Suppose FF satisfies the following conditions: 1. **Linearity:** FF is linear on the space of smooth functions, i.e., F(ϕ1+ϕ2)=F(ϕ1)+F(ϕ2)F(\phi_1 + \phi_2) = F(\phi_1) + F(\phi_2) and F(cϕ)=cF(ϕ)F(c \cdot \phi) = c \cdot F(\phi) for any cRc \in \mathbb{R} and smooth functions ϕ,ϕ1,ϕ2:XU\phi, \phi_1, \phi_2: X \to U. 2. **Smoothness:** FF maps any smooth family of functions ϕ:R×XU\phi: \mathbb{R} \times X \to U to a smooth function on R×X\mathbb{R} \times X defined by (s,x)F(ϕ(s,))(x)(s, x) \mapsto F(\phi(s, \cdot))(x). 3. **Commutativity of Differentiation:** For any smooth family ϕ:R×XU\phi: \mathbb{R} \times X \to U, the derivative at s=0s=0 commutes with FF at any point xXx \in X: ddss=0F(ϕ(s,))(x)=F(ϕss=0)(x). \left. \frac{d}{ds} \right|_{s=0} F(\phi(s, \cdot))(x) = F\left( \left. \frac{\partial \phi}{\partial s} \right|_{s=0} \right)(x). If u:XUu: X \to U is a smooth function and FF has a variational adjoint FF', then the variational adjoint derivative of FF at uu is FF'.

theorem

The variational adjoint derivative of the identity operator is the identity operator

#id

Let u:XUu: X \to U be a CC^\infty smooth function. The identity operator F:(XU)(XU)F : (X \to U) \to (X \to U) defined by F(ϕ)=ϕF(\phi) = \phi has a variational adjoint derivative at uu given by the identity operator F(ψ)=ψF'(\psi) = \psi.

theorem

Variational Adjoint Derivative of a Constant Functional is Zero

#const

Let u:XUu: X \to U and v:XVv: X \to V be CC^\infty smooth functions. The constant functional F:(XU)(XV)F: (X \to U) \to (X \to V) defined by F(ϕ)=vF(\phi) = v for all ϕ\phi has a variational adjoint derivative at uu given by the zero operator F(ψ)=0F'(\psi) = 0.

theorem

Chain Rule for Variational Adjoint Derivatives: (FG)=GF(F \circ G)' = G' \circ F'

#comp

Let F:(YV)(ZW)F: (Y \to V) \to (Z \to W) and G:(XU)(YV)G: (X \to U) \to (Y \to V) be operators between function spaces, and let u:XUu: X \to U be a function. If FF has a variational adjoint derivative FF' at the point G(u)G(u) and GG has a variational adjoint derivative GG' at the point uu, then the composition FGF \circ G has a variational adjoint derivative at uu given by the composition of the adjoint derivatives in reverse order, GFG' \circ F'.

theorem

Agreement on Smooth Functions Preserves Variational Adjoint Derivative

#congr

Let F,G:(XU)(YV)F, G: (X \to U) \to (Y \to V) be functionals and u:XUu: X \to U be a function. Suppose that FF has a variational adjoint derivative FF' at uu (denoted by HasVarAdjDerivAt F F u\text{HasVarAdjDerivAt } F \ F' \ u). If FF and GG agree on all smooth functions, i.e., F(ϕ)=G(ϕ)F(\phi) = G(\phi) for every smooth function ϕ:XU\phi: X \to U (ϕC\phi \in C^\infty), then GG also has FF' as its variational adjoint derivative at uu.

theorem

Uniqueness of Variational Adjoint Derivative on Test Functions

#unique_on_test_functions

Let XX and YY be spaces, where XX is equipped with a measure that is finite on compact sets and strictly positive on non-empty open sets. Let F:(XU)(YV)F: (X \to U) \to (Y \to V) be a functional. If FF' and GG' are both variational adjoint derivatives of FF at u:XUu: X \to U (satisfying the `HasVarAdjDerivAt` condition), then for any test function ϕ:YV\phi: Y \to V (i.e., a smooth function with compact support), it holds that Fϕ=GϕF' \phi = G' \phi.

theorem

Uniqueness of Variational Adjoint Derivative on Smooth Functions

#unique

Let XX and YY be normed real inner product spaces equipped with measures, where XX has a measure that is finite on compact sets and strictly positive on non-empty open sets, and YY is finite-dimensional. Let F:(XU)(YV)F: (X \to U) \to (Y \to V) be a functional. If FF has two variational adjoint derivatives FF' and GG' at a point u:XUu: X \to U (denoted by HasVarAdjDerivAt F F u\text{HasVarAdjDerivAt } F \ F' \ u and HasVarAdjDerivAt F G u\text{HasVarAdjDerivAt } F \ G' \ u), then for every smooth function ϕ:YV\phi: Y \to V (ϕC\phi \in C^\infty), it holds that Fϕ=GϕF' \phi = G' \phi.

theorem

Variational Adjoint Derivative of the Product Operator (F,G)(F, G)

#prod

Let XX be a space equipped with a measure that is finite on compact sets. Let F:(XU)(XV)F: (X \to U) \to (X \to V) and G:(XU)(XW)G: (X \to U) \to (X \to W) be operators. Suppose FF has a variational adjoint derivative FF' at the function u:XUu: X \to U, and GG has a variational adjoint derivative GG' at uu. Then the product operator H:(XU)(XV×W)H: (X \to U) \to (X \to V \times W), defined by H(ϕ)(x)=(F(ϕ)(x),G(ϕ)(x))H(\phi)(x) = (F(\phi)(x), G(\phi)(x)), has a variational adjoint derivative HH' at uu given by: H(ψ)(x)=F(ψ1)(x)+G(ψ2)(x) H'(\psi)(x) = F'(\psi_1)(x) + G'(\psi_2)(x) where ψ1:XV\psi_1: X \to V and ψ2:XW\psi_2: X \to W are the component functions of ψ:XV×W\psi: X \to V \times W such that ψ(x)=(ψ1(x),ψ2(x))\psi(x) = (\psi_1(x), \psi_2(x)).

theorem

Variational adjoint of the first component of an operator FF is FF' applied to the zero-padded input

#fst

Suppose an operator F:(XU)(XW×V)F: (X \to U) \to (X \to W \times V) has a variational adjoint derivative FF' at a function u:XUu: X \to U. Then the operator that maps a function ϕ:XU\phi: X \to U to the first component of F(ϕ)F(\phi), given by x(F(ϕ)(x))1x \mapsto (F(\phi)(x))_1, also has a variational adjoint derivative at uu. This variational adjoint derivative is the operator that maps a function ψ:XW\psi: X \to W to the value of FF' evaluated at the function x(ψ(x),0)x' \mapsto (\psi(x'), 0).

theorem

Variational adjoint of the second component of an operator FF is FF' applied to the zero-prefixed input

#snd

Suppose an operator F:(XU)(XW×V)F: (X \to U) \to (X \to W \times V) has a variational adjoint derivative FF' at a function u:XUu: X \to U. Then the operator that maps a function ϕ:XU\phi: X \to U to the second component of F(ϕ)F(\phi), given by x(F(ϕ)(x))2x \mapsto (F(\phi)(x))_2, also has a variational adjoint derivative at uu. This variational adjoint derivative is the operator that maps a function ψ:XV\psi: X \to V to the value of FF' evaluated at the function x(0,ψ(x))x' \mapsto (0, \psi(x')).

theorem

The variational adjoint of the derivative operator is the negative derivative operator

#deriv'

Let u:RUu: \mathbb{R} \to U be a CC^\infty smooth function. Let FF be the operator that maps a function ϕ:RU\phi: \mathbb{R} \to U to its derivative dϕdx\frac{d\phi}{dx}. Then the variational adjoint derivative of FF at uu is the operator that maps a function ϕ\phi to its negative derivative dϕdx-\frac{d\phi}{dx}.

theorem

The variational adjoint derivative of ddxF\frac{d}{dx} F is F(ddx)F' \circ (-\frac{d}{dx})

#deriv

Let F:(RU)(RV)F: (\mathbb{R} \to U) \to (\mathbb{R} \to V) be an operator between function spaces. If FF has a variational adjoint derivative FF' at the function u:RUu: \mathbb{R} \to U, then the operator mapping ϕ\phi to the derivative ddx(F(ϕ))\frac{d}{dx}(F(\phi)) has a variational adjoint derivative at uu given by the mapping ψF(dψdx)\psi \mapsto F'(-\frac{d\psi}{dx}).

theorem

Variational Adjoint Derivative of Pointwise Mapping (fmap)

#fmap

Let UU and VV be complete generalized inner product spaces over R\mathbb{R}. Let u:XUu: X \to U be a smooth (CC^\infty) function. Let f:XUVf: X \to U \to V be a map such that the uncurried function (x,y)f(x,y)(x, y) \mapsto f(x, y) is CC^\infty, and for each xXx \in X, the map f(x,):UVf(x, \cdot): U \to V has an adjoint Fréchet derivative f(x,u(x))f'(x, u(x)) at the point u(x)u(x). Consider the operator FF acting on functions ϕ:XU\phi: X \to U defined by pointwise application: (Fϕ)(x)=f(x,ϕ(x)).(F\phi)(x) = f(x, \phi(x)). Then, the variational adjoint derivative of FF at uu is the operator that maps a function ψ:XV\psi: X \to V to the function: xf(x,u(x))(ψ(x)).x \mapsto f'(x, u(x))(\psi(x)).

theorem

The variational adjoint derivative of F-F is F-F'

#neg

Suppose FF is an operator mapping functions from XUX \to U to functions from XVX \to V. If FF' is the variational adjoint derivative of FF at uu, then the operator mapping ϕ\phi to F(ϕ)-F(\phi) has a variational adjoint derivative at uu given by the mapping ψF(ψ)\psi \mapsto -F'(\psi).

theorem

The variational adjoint derivative of F+GF + G is F+GF' + G'

#add

Suppose FF and GG are operators mapping functions from XUX \to U to functions from XVX \to V. If FF has a variational adjoint derivative FF' at u:XUu: X \to U, and GG has a variational adjoint derivative GG' at uu, then the sum operator defined by ϕF(ϕ)+G(ϕ)\phi \mapsto F(\phi) + G(\phi) has a variational adjoint derivative at uu given by the operator ψF(ψ)+G(ψ)\psi \mapsto F'(\psi) + G'(\psi).

theorem

The variational adjoint derivative of Fi\sum F_i is Fi\sum F'_i

#sum

Let ι\iota be a finite index set. For each iιi \in \iota, let FiF_i be an operator mapping functions from XUX \to U to functions from XVX \to V. Suppose that for each iιi \in \iota, FiF_i has a variational adjoint derivative FiF'_i at a CC^\infty smooth function u:XUu: X \to U. Then the sum operator SS, defined by (Sϕ)(x)=iιFi(ϕ)(x)(S\phi)(x) = \sum_{i \in \iota} F_i(\phi)(x), has a variational adjoint derivative at uu given by the operator SS', where for any function ψ:XV\psi: X \to V, S(ψ)(x)=iιFi(ψ)(x).S'(\psi)(x) = \sum_{i \in \iota} F'_i(\psi)(x).

theorem

Product Rule for Variational Adjoint Derivatives

#mul

Let F,G:(XU)(XR)F, G: (X \to U) \to (X \to \mathbb{R}) be operators. Suppose FF and GG have variational adjoint derivatives FF' and GG' at a function u:XUu: X \to U, respectively. Then the pointwise product operator HH, defined by (Hϕ)(x)=F(ϕ)(x)G(ϕ)(x)(H\phi)(x) = F(\phi)(x) \cdot G(\phi)(x), has a variational adjoint derivative at uu given by the operator HH', where for any function ψ:XR\psi: X \to \mathbb{R}, H(ψ)(x)=F(xψ(x)G(u)(x))(x)+G(xF(u)(x)ψ(x))(x).H'(\psi)(x) = F'(x \mapsto \psi(x)G(u)(x))(x) + G'(x \mapsto F(u)(x)\psi(x))(x). In more concise notation, the variational adjoint derivative is H(ψ)=F(ψG(u))+G(ψF(u))H'(\psi) = F'(\psi \cdot G(u)) + G'(\psi \cdot F(u)), where the products inside the arguments are pointwise products of functions.

theorem

The Variational Adjoint Derivative of cFc F is F(cψ)F'(c \psi)

#const_mul

Let F:(XU)(XR)F: (X \to U) \to (X \to \mathbb{R}) be an operator. Suppose FF has a variational adjoint derivative FF' at a function u:XUu: X \to U. For any constant scalar cRc \in \mathbb{R}, the operator HH defined by the pointwise multiplication (Hϕ)(x)=cF(ϕ)(x)(H\phi)(x) = c \cdot F(\phi)(x) has a variational adjoint derivative HH' at uu, given by: H(ψ)=F(cψ)H'(\psi) = F'(c \cdot \psi) where cψc \cdot \psi denotes the function xcψ(x)x' \mapsto c \psi(x').

theorem

Variational Adjoint Derivative of Pointwise Multiplication by a Fixed Smooth Function ff

#fun_mul

Let XX and UU be spaces. Let f:XRf: X \to \mathbb{R} be an infinitely differentiable function (fC(X,R)f \in C^\infty(X, \mathbb{R})). Suppose an operator F:(XU)(XR)F: (X \to U) \to (X \to \mathbb{R}) possesses a variational adjoint derivative FF' at a function u:XUu: X \to U. Then the operator HH, defined by the pointwise product (Hϕ)(x)=f(x)F(ϕ)(x)(H\phi)(x) = f(x)F(\phi)(x), has a variational adjoint derivative at uu given by the operator HH', where for any function ψ:XR\psi: X \to \mathbb{R}: H(ψ)=F(fψ)H'(\psi) = F'(f \cdot \psi) Here, fψf \cdot \psi denotes the pointwise product xf(x)ψ(x)x' \mapsto f(x')\psi(x').

theorem

The variational adjoint derivative of the directional derivative Dϕ[dx]D\phi[dx] is Dψ[dx]-D\psi[dx].

#fderiv

Let XX be a finite-dimensional real vector space equipped with an additive Haar measure (volume). Let u:XUu: X \to U be a smooth function. For a fixed vector dxXdx \in X, consider the operator that maps a function ϕ:XU\phi: X \to U to its Fréchet derivative at xx in the direction dxdx, denoted by Dϕ(x)[dx]D\phi(x)[dx]. The variational adjoint derivative of this operator at uu is the operator that maps a function ψ\psi to the negative of its directional derivative, Dψ(x)[dx]-D\psi(x)[dx].

theorem

The variational adjoint derivative of D(F(ϕ))[dx]D(F(\phi))[dx] is F(Dψ[dx])F'(-D\psi[dx])

#fderiv'

Let XX be a finite-dimensional real vector space equipped with an additive Haar measure. Let F:(XU)(XV)F: (X \to U) \to (X \to V) be an operator between function spaces, and let FF' be its variational adjoint derivative at a point uu. For a fixed vector dxXdx \in X, consider the operator that maps a function ϕ\phi to the directional derivative of F(ϕ)F(\phi) in the direction dxdx, denoted by xD(F(ϕ))(x)[dx]x \mapsto D(F(\phi))(x)[dx]. The variational adjoint derivative of this operator at uu is given by the operator that maps a function ψ\psi to F(ψ)F'(\psi^*), where ψ(x)=Dψ(x)[dx]\psi^*(x') = -D\psi(x')[dx] is the negative directional derivative of ψ\psi.

theorem

The variational adjoint derivative of the gradient ϕ\nabla \phi is divψ-\text{div} \psi

#gradient

Let u:Space dRu: \text{Space } d \to \mathbb{R} be an infinitely smooth (CC^\infty) function. Consider the operator that maps a scalar function ϕ:Space dR\phi: \text{Space } d \to \mathbb{R} to its gradient field ϕ\nabla \phi. The variational adjoint derivative of this gradient operator at uu is the operator that maps a vector field ψ\psi to the negative of its divergence, divψ-\text{div} \psi.

theorem

The variational adjoint derivative of \nabla is div-\text{div}

#grad

Let u:Space dRu: \text{Space } d \to \mathbb{R} be an infinitely smooth (CC^\infty) function. The variational adjoint derivative of the gradient operator FF, defined by F(ϕ)=ϕF(\phi) = \nabla \phi for scalar functions ϕ:Space dR\phi: \text{Space } d \to \mathbb{R}, at the point uu is the negative divergence operator FF', defined by F(ψ)=divψF'(\psi) = -\text{div} \psi for vector fields ψ\psi.

theorem

The Variational Adjoint Derivative of div\text{div} is -\nabla

#div

Let dd be a natural number representing the dimension of the space, and let u:Space dRdu: \text{Space } d \to \mathbb{R}^d be a smooth (CC^\infty) function. The variational adjoint derivative of the divergence operator ϕdiv ϕ\phi \mapsto \text{div } \phi at uu is the operator that maps a scalar field ψ\psi to its negative gradient ψ-\nabla \psi.