Physlib.Mathematics.VariationalCalculus.HasVarAdjDeriv
32 declarations
Smoothness of from existence of variational adjoint derivative of
#apply_smooth_of_smoothLet be an operator between function spaces that possesses a variational adjoint derivative at . If is a smooth function (of class ), then its image under the operator , given by , is also a smooth function.
Smoothness of from existence of variational adjoint derivative at
#apply_smooth_selfLet be an operator between function spaces. Suppose possesses a variational adjoint derivative at a function . Then the function is infinitely differentiable (of class ).
is for smooth families and operators with variational adjoint derivatives
#smooth_RSuppose an operator has a variational adjoint derivative at a function . Let be an infinitely differentiable () family of functions, where the mapping is smooth. Then, for any fixed point , the function mapping the parameter to the value of the operator evaluated at the function and then evaluated at , given by is infinitely differentiable () with respect to .
is for operators with variational adjoint derivatives
#smooth_linearSuppose an operator has a variational adjoint derivative at . Let be an infinitely differentiable () family of functions. Let be the function and let be the partial derivative of with respect to its first argument at , given by . Then, for any fixed point , the function mapping to the value of the operator evaluated at the linear variation and then evaluated at , given by is infinitely differentiable () with respect to .
is for operators with variational adjoint derivatives
#smooth_adjointSuppose an operator has a variational adjoint derivative at the function . Then, for any infinitely differentiable (smooth) function and any fixed point , the function mapping to the value of the operator at the perturbed function evaluated at , given by is infinitely differentiable () with respect to .
is differentiable for operators with variational adjoint derivatives
#differentiable_linearSuppose an operator has a variational adjoint derivative at . Let be an infinitely differentiable () family of functions. Let be the function and let be the partial derivative of with respect to its first argument at , given by . Then, for any fixed point , the function mapping to the value of the operator evaluated at the linear variation and then evaluated at , given by is differentiable with respect to .
for linear operators
#linearize_of_linearLet be an operator mapping between function spaces. Suppose is linear on smooth functions, meaning that for all smooth and , and . Additionally, assume that for any smooth family of functions , the derivative at commutes with at any point : Then, for any such smooth and any , the derivative of applied to the path is equal to the derivative of applied to the first-order linear approximation of at :
The variational adjoint of the linearization of a linear operator is its adjoint
#deriv_adjoint_of_linearLet be an operator between function spaces that is linear on the space of smooth functions, meaning and for any and smooth functions . Suppose is a smooth function and has a variational adjoint . Then the linear operator that maps a variation to the directional derivative of at , defined by has as its variational adjoint.
The Variational Adjoint Derivative of a Linear Operator is its Variational Adjoint
#hasVarAdjDerivAt_of_hasVarAdjoint_of_linearLet be an operator between function spaces. Suppose satisfies the following conditions: 1. **Linearity:** is linear on the space of smooth functions, i.e., and for any and smooth functions . 2. **Smoothness:** maps any smooth family of functions to a smooth function on defined by . 3. **Commutativity of Differentiation:** For any smooth family , the derivative at commutes with at any point : If is a smooth function and has a variational adjoint , then the variational adjoint derivative of at is .
The variational adjoint derivative of the identity operator is the identity operator
#idLet be a smooth function. The identity operator defined by has a variational adjoint derivative at given by the identity operator .
Variational Adjoint Derivative of a Constant Functional is Zero
#constLet and be smooth functions. The constant functional defined by for all has a variational adjoint derivative at given by the zero operator .
Chain Rule for Variational Adjoint Derivatives:
#compLet and be operators between function spaces, and let be a function. If has a variational adjoint derivative at the point and has a variational adjoint derivative at the point , then the composition has a variational adjoint derivative at given by the composition of the adjoint derivatives in reverse order, .
Agreement on Smooth Functions Preserves Variational Adjoint Derivative
#congrLet be functionals and be a function. Suppose that has a variational adjoint derivative at (denoted by ). If and agree on all smooth functions, i.e., for every smooth function (), then also has as its variational adjoint derivative at .
Uniqueness of Variational Adjoint Derivative on Test Functions
#unique_on_test_functionsLet and be spaces, where is equipped with a measure that is finite on compact sets and strictly positive on non-empty open sets. Let be a functional. If and are both variational adjoint derivatives of at (satisfying the `HasVarAdjDerivAt` condition), then for any test function (i.e., a smooth function with compact support), it holds that .
Uniqueness of Variational Adjoint Derivative on Smooth Functions
#uniqueLet and be normed real inner product spaces equipped with measures, where has a measure that is finite on compact sets and strictly positive on non-empty open sets, and is finite-dimensional. Let be a functional. If has two variational adjoint derivatives and at a point (denoted by and ), then for every smooth function (), it holds that .
Variational Adjoint Derivative of the Product Operator
#prodLet be a space equipped with a measure that is finite on compact sets. Let and be operators. Suppose has a variational adjoint derivative at the function , and has a variational adjoint derivative at . Then the product operator , defined by , has a variational adjoint derivative at given by: where and are the component functions of such that .
Variational adjoint of the first component of an operator is applied to the zero-padded input
#fstSuppose an operator has a variational adjoint derivative at a function . Then the operator that maps a function to the first component of , given by , also has a variational adjoint derivative at . This variational adjoint derivative is the operator that maps a function to the value of evaluated at the function .
Variational adjoint of the second component of an operator is applied to the zero-prefixed input
#sndSuppose an operator has a variational adjoint derivative at a function . Then the operator that maps a function to the second component of , given by , also has a variational adjoint derivative at . This variational adjoint derivative is the operator that maps a function to the value of evaluated at the function .
The variational adjoint of the derivative operator is the negative derivative operator
#deriv'Let be a smooth function. Let be the operator that maps a function to its derivative . Then the variational adjoint derivative of at is the operator that maps a function to its negative derivative .
The variational adjoint derivative of is
#derivLet be an operator between function spaces. If has a variational adjoint derivative at the function , then the operator mapping to the derivative has a variational adjoint derivative at given by the mapping .
Variational Adjoint Derivative of Pointwise Mapping (fmap)
#fmapLet and be complete generalized inner product spaces over . Let be a smooth () function. Let be a map such that the uncurried function is , and for each , the map has an adjoint Fréchet derivative at the point . Consider the operator acting on functions defined by pointwise application: Then, the variational adjoint derivative of at is the operator that maps a function to the function:
The variational adjoint derivative of is
#negSuppose is an operator mapping functions from to functions from . If is the variational adjoint derivative of at , then the operator mapping to has a variational adjoint derivative at given by the mapping .
The variational adjoint derivative of is
#addSuppose and are operators mapping functions from to functions from . If has a variational adjoint derivative at , and has a variational adjoint derivative at , then the sum operator defined by has a variational adjoint derivative at given by the operator .
The variational adjoint derivative of is
#sumLet be a finite index set. For each , let be an operator mapping functions from to functions from . Suppose that for each , has a variational adjoint derivative at a smooth function . Then the sum operator , defined by , has a variational adjoint derivative at given by the operator , where for any function ,
Product Rule for Variational Adjoint Derivatives
#mulLet be operators. Suppose and have variational adjoint derivatives and at a function , respectively. Then the pointwise product operator , defined by , has a variational adjoint derivative at given by the operator , where for any function , In more concise notation, the variational adjoint derivative is , where the products inside the arguments are pointwise products of functions.
The Variational Adjoint Derivative of is
#const_mulLet be an operator. Suppose has a variational adjoint derivative at a function . For any constant scalar , the operator defined by the pointwise multiplication has a variational adjoint derivative at , given by: where denotes the function .
Variational Adjoint Derivative of Pointwise Multiplication by a Fixed Smooth Function
#fun_mulLet and be spaces. Let be an infinitely differentiable function (). Suppose an operator possesses a variational adjoint derivative at a function . Then the operator , defined by the pointwise product , has a variational adjoint derivative at given by the operator , where for any function : Here, denotes the pointwise product .
The variational adjoint derivative of the directional derivative is .
#fderivLet be a finite-dimensional real vector space equipped with an additive Haar measure (volume). Let be a smooth function. For a fixed vector , consider the operator that maps a function to its Fréchet derivative at in the direction , denoted by . The variational adjoint derivative of this operator at is the operator that maps a function to the negative of its directional derivative, .
The variational adjoint derivative of is
#fderiv'Let be a finite-dimensional real vector space equipped with an additive Haar measure. Let be an operator between function spaces, and let be its variational adjoint derivative at a point . For a fixed vector , consider the operator that maps a function to the directional derivative of in the direction , denoted by . The variational adjoint derivative of this operator at is given by the operator that maps a function to , where is the negative directional derivative of .
The variational adjoint derivative of the gradient is
#gradientLet be an infinitely smooth () function. Consider the operator that maps a scalar function to its gradient field . The variational adjoint derivative of this gradient operator at is the operator that maps a vector field to the negative of its divergence, .
The variational adjoint derivative of is
#gradLet be an infinitely smooth () function. The variational adjoint derivative of the gradient operator , defined by for scalar functions , at the point is the negative divergence operator , defined by for vector fields .
The Variational Adjoint Derivative of is
#divLet be a natural number representing the dimension of the space, and let be a smooth () function. The variational adjoint derivative of the divergence operator at is the operator that maps a scalar field to its negative gradient .
