PhyslibSearch

Physlib.Mathematics.InnerProductSpace.Calculus

5 declarations

definition

Fréchet derivative of the inner product at pp as a continuous linear map

#fderivInnerCLM'

For a generalized inner product space EE over R\mathbb{R}, this definition provides the Fréchet derivative of the inner product ⟨⋅,⋅⟩\langle \cdot, \cdot \rangle at a point p=(x,y)∈E×Ep = (x, y) \in E \times E. The result is a continuous linear map from E×EE \times E to R\mathbb{R}.

theorem

Fréchet derivative of the inner product t↦⟨f(t),g(t)⟩t \mapsto \langle f(t), g(t) \rangle

#inner'

Let EE be a normed space and FF be a generalized real inner product space. If f,g:E→Ff, g: E \to F are functions such that ff has a Fréchet derivative f′f' at x∈Ex \in E and gg has a Fréchet derivative g′g' at xx, then the function t↦⟨f(t),g(t)⟩t \mapsto \langle f(t), g(t) \rangle has a Fréchet derivative at xx. This derivative is the continuous linear map given by the composition of the Fréchet derivative of the inner product operation at (f(x),g(x))(f(x), g(x)) and the product of the derivatives f′f' and g′g'.

theorem

The Fréchet derivative of ⟨f(t),g(t)⟩\langle f(t), g(t) \rangle at xx applied to yy is ⟨f(x),Dgx(y)⟩+⟨Dfx(y),g(x)⟩\langle f(x), Dg_x(y) \rangle + \langle Df_x(y), g(x) \rangle

#fderiv_inner_apply'

Let EE be a normed space and FF be a real generalized inner product space. Suppose f,g:E→Ff, g: E \to F are functions that are differentiable at x∈Ex \in E. Then for any vector y∈Ey \in E, the Fréchet derivative of the inner product function t↦⟨f(t),g(t)⟩t \mapsto \langle f(t), g(t) \rangle at the point xx applied to yy is given by: D(⟨f,g⟩)x(y)=⟨f(x),Dgx(y)⟩+⟨Dfx(y),g(x)⟩, D(\langle f, g \rangle)_x(y) = \langle f(x), Dg_x(y) \rangle + \langle Df_x(y), g(x) \rangle, where DfxDf_x and DgxDg_x denote the Fréchet derivatives of ff and gg at xx, respectively.

theorem

The derivative of ⟨f(t),g(t)⟩\langle f(t), g(t) \rangle is ⟨f(x),g′(x)⟩+⟨f′(x),g(x)⟩\langle f(x), g'(x) \rangle + \langle f'(x), g(x) \rangle

#deriv_inner_apply'

Let FF be a real generalized inner product space. Suppose f,g:R→Ff, g: \mathbb{R} \to F are functions that are differentiable at x∈Rx \in \mathbb{R}. Then the derivative of the inner product function t↦⟨f(t),g(t)⟩t \mapsto \langle f(t), g(t) \rangle at the point xx is given by: ddt⟨f(t),g(t)⟩∣t=x=⟨f(x),g′(x)⟩+⟨f′(x),g(x)⟩ \frac{d}{dt} \langle f(t), g(t) \rangle \Big|_{t=x} = \langle f(x), g'(x) \rangle + \langle f'(x), g(x) \rangle where f′(x)f'(x) and g′(x)g'(x) denote the derivatives of ff and gg at xx, respectively.

theorem

f,gf, g differentiable   ⟹  ⟨f,g⟩\implies \langle f, g \rangle differentiable

#inner'

Let EE be a real normed space and FF be a real generalized inner product space. For functions f,g:E→Ff, g : E \to F and a point x∈Ex \in E, if ff and gg are differentiable at xx, then the function t↦⟨f(t),g(t)⟩t \mapsto \langle f(t), g(t) \rangle is differentiable at xx.