Physlib.Mathematics.VariationalCalculus.HasVarAdjDeriv
Variational adjoint derivative
Variational adjoint derivative of `F` at `u` is a generalization of `(fderiv ℝ F u).adjoint` to function spaces. In particular, variational gradient is an analog of `gradient F u := (fderiv ℝ F u).adjoint 1`.
The definition of `HasVarAdjDerivAt` is constructed exactly such that we can prove composition theorem saying ``` HasVarAdjDerivAt F F' (G u)) → HasVarAdjDerivAt G G' u → HasVarAdjDerivAt (F ∘ G) (G' ∘ F') u ``` This theorem is the main tool to mechanistically compute variational gradient.
32 declarations
Smoothness of from existence of variational adjoint derivative of
Let 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
Let 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
Suppose 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
Suppose 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
Suppose 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
Suppose 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
Let 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
Let 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
Let 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
Let 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
Let 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:
Let 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
Let 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
Let 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
Let 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
Let 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
Suppose 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
Suppose 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
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
Let 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)
Let 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
Suppose 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
Suppose 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
Let 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
Let 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
Let 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
Let 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 .
Let 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
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
Let 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
Let 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
Let 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 .
