Physlib.Mathematics.Calculus.AdjFDeriv
Adjoint Fréchet derivative
`adjFDeriv 𝕜 f x = (fderiv 𝕜 f x).adjoint`
The main purpose of defining `adjFDeriv` is to compute `gradient f x = adjFDeriv 𝕜 f x 1`. The advantage of working with `adjFDeriv` is that we can formulate composition theorem.
The reason why we do not want to compute `fderiv` and then `adjoint` is that to compute `fderiv 𝕜 f` or `adjoint f` we decompose `f = f₁ ∘ ... ∘ fₙ` and then apply composition theorem. The problem is that this decomposition has to be done differently for `fderiv` and `adjoint`. The problem is that when working with `fderiv` the natural product type is `X × Y` but when working with `adjoint` the natural product is `WithLp 2 (X × Y)`. For example:
32 declarations
Adjoint Fréchet derivative
Given a function between two inner product spaces and over a field , let denote the Fréchet derivative of at the point . The adjoint Fréchet derivative at is the adjoint of this linear map, denoted . For a vector , the function returns the value , which is the unique vector satisfying for all .
if has an adjoint Fréchet derivative at
Let and be inner product spaces over a field . For a function and a point , if has an adjoint Fréchet derivative at (expressed by the proposition `HasAdjFDerivAt 𝕜 f f' x`), then the defined adjoint Fréchet derivative is equal to .
Differentiability at implies existence of adjoint Fréchet derivative
Let and be complete generalized inner product spaces over a field . If a function is Fréchet differentiable at a point , then possesses an adjoint Fréchet derivative at , which is given by the adjoint of its Fréchet derivative, denoted as .
The mapping is a bounded bilinear map over
Let and be real inner product spaces. The map that sends a pair to , where is the adjoint of the continuous linear map , is a bounded bilinear map over .
Let be a real normed space, and let and be complete real generalized inner product spaces. Suppose is a function such that for every and , the partial map has an adjoint Fréchet derivative at . If is as a function of , then the map from to is . Here, the adjoint Fréchet derivative is the adjoint of the linear map , satisfying for all and .
Let be an inner product space over a field (where is typically or ). For any function that is Fréchet differentiable at a point , the gradient is equal to the adjoint Fréchet derivative of at applied to the unit . That is, , where denotes the adjoint of the Fréchet derivative .
The identity map has the identity as its adjoint Fréchet derivative at any point
Let be an inner product space over a field . For any , the identity function defined by has an adjoint Fréchet derivative at which is the identity function .
The Adjoint Fréchet Derivative of the Identity Function is the Identity Map
Let be an inner product space over a field . The adjoint Fréchet derivative of the identity function , defined by , is the identity map at every point. Specifically, for any point and any vector , the adjoint Fréchet derivative satisfies .
The Adjoint Fréchet Derivative of the Identity Map is the Identity Map
Let be an inner product space over a field . The adjoint Fréchet derivative of the identity function is the identity map at every point. Specifically, for any point and any vector , the adjoint Fréchet derivative satisfies .
The adjoint Fréchet derivative of a constant function is zero
Let and be inner product spaces over a field . For any point and any value , the constant function defined by has an adjoint Fréchet derivative at given by the zero linear map .
The adjoint Fréchet derivative of a constant function is zero
Let and be inner product spaces over a field . For any constant , let be the constant function . The adjoint Fréchet derivative of is zero at every point , meaning that for all and all vectors , .
Chain Rule for Adjoint Fréchet Derivatives
Let , and be inner product spaces over a field . Let and be functions. Suppose has an adjoint Fréchet derivative at a point , and has an adjoint Fréchet derivative at the point . Then the composition has an adjoint Fréchet derivative at given by the composition of the adjoint derivatives .
Chain Rule for Adjoint Fréchet Derivatives:
Let , and be complete inner product spaces over a field . Suppose is a function differentiable at a point and is a function differentiable at . The adjoint Fréchet derivative of the composition at is the composition of the adjoint Fréchet derivatives of at and at . That is, for any : In terms of the adjoint of the Fréchet derivative operator , this is expressed as:
The adjoint Fréchet derivative of is
Let , and be inner product spaces over a field . Suppose and are functions such that at a point , has an adjoint Fréchet derivative and has an adjoint Fréchet derivative . Then the map defined by has an adjoint Fréchet derivative at given by the map . Here, the product space is equipped with the standard product inner product .
The adjoint Fréchet derivative of is
Let , and be generalized inner product spaces over a field . If a function has an adjoint Fréchet derivative at a point , then the map (the projection onto the first component) has an adjoint Fréchet derivative at given by the function .
The adjoint Fréchet derivative of is
Let , and be complete generalized inner product spaces over a field . For a function that is Fréchet differentiable at a point , the adjoint Fréchet derivative of its first component (where ) at is given by the linear map . Here, denotes the adjoint Fréchet derivative of at . The product space is equipped with the standard product inner product .
The adjoint Fréchet derivative of the first projection is
Let and be complete generalized inner product spaces over a field . For the projection map defined by , its adjoint Fréchet derivative at any point is the linear map that sends to the pair .
The adjoint Fréchet derivative of is
Let , and be inner product spaces over a field . Let be a function and . If has an adjoint Fréchet derivative at , then the map (the projection onto the second component) also has an adjoint Fréchet derivative at , which is given by the linear map .
Adjoint Fréchet derivative of is
Let , and be complete generalized inner product spaces over a field . Let be a function that is differentiable at a point . Then the adjoint Fréchet derivative of the map (the projection of onto its second component) at is given by the linear map that sends to , where denotes the adjoint Fréchet derivative of at .
The adjoint Fréchet derivative of is
Let and be complete inner product spaces over a field . The adjoint Fréchet derivative of the second projection map , defined by , at any point is the linear map from to that sends to .
The adjoint Fréchet derivative of is
Let , and be inner product spaces over a field . Let be a function, and let . Suppose that: 1. The uncurried function is differentiable at . 2. The partial map has an adjoint Fréchet derivative at . 3. The partial map has an adjoint Fréchet derivative at . Then the uncurried function has an adjoint Fréchet derivative at given by the map from into .
The adjoint Fréchet derivative of is the pair of partial adjoint derivatives
Let , and be complete inner product spaces over a field . Let be a function such that the uncurried function is differentiable at a point . The adjoint Fréchet derivative of at , denoted , is given by: for all , where is the adjoint Fréchet derivative of the partial map at , and is the adjoint Fréchet derivative of the partial map at .
The adjoint Fréchet derivative of is
Let and be inner product spaces over a field . If a function has an adjoint Fréchet derivative at a point , then the function also has an adjoint Fréchet derivative at , given by the map .
Let and be complete inner product spaces over a field . If a function is Fréchet differentiable at a point , then the adjoint Fréchet derivative of the negated function at is equal to the negation of the adjoint Fréchet derivative of at . In terms of the adjoint operator , this is expressed as: Specifically, for any vector , the value is .
has adjoint Fréchet derivative
Let and be inner product spaces over a field . If are functions such that has an adjoint Fréchet derivative at and has an adjoint Fréchet derivative at , then the sum function (defined by ) has an adjoint Fréchet derivative at given by (defined by ).
Let and be complete inner product spaces over a field . If are functions differentiable at , then the adjoint Fréchet derivative of their sum at is the sum of their individual adjoint Fréchet derivatives at . That is, where denotes the adjoint of the Fréchet derivative of at .
The adjoint Fréchet derivative of is
Let and be inner product spaces over a field . Suppose are functions that have adjoint Fréchet derivatives at a point , respectively. Then the function (defined by ) has an adjoint Fréchet derivative at given by (defined by ).
Adjoint Fréchet Derivative of is
Let and be complete inner product spaces over a field . Suppose are functions that are Fréchet differentiable at a point . Then the adjoint Fréchet derivative of the difference at is equal to the difference of the adjoint Fréchet derivatives of and at . That is, for any vector : Using the notation for the adjoint of the Fréchet derivative, this can be written as:
Adjoint Fréchet Derivative of the Product
Let and be generalized inner product spaces over a field (where is or ). Suppose is a map with an adjoint Fréchet derivative at , and is a map with an adjoint Fréchet derivative at . Then the adjoint Fréchet derivative of the scalar-vector product at the point is the linear map given by: where denotes the conjugate of and denotes the inner product on .
Adjoint Fréchet Derivative of the Product
Let and be complete inner product spaces over a field (where is or ). If and are differentiable at a point , then the adjoint Fréchet derivative of the scalar-vector product at is the linear map given by: where and denote the adjoint Fréchet derivatives of and at respectively, and denotes the inner product on .
Adjoint Fréchet Derivative of the Inner Product
Let be a real generalized inner product space. For the inner product function defined by , the adjoint Fréchet derivative at any point is the linear map from to defined by: for any .
Adjoint Fréchet Derivative of Inner Product is
Let be a real generalized inner product space. For the inner product function defined by , the adjoint Fréchet derivative at any point is the linear map from to defined by: for any .
