HasFDerivWithinAt.hasGradientWithinAt
theorem HasFDerivWithinAt.hasGradientWithinAt :
∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
[inst_3 : CompleteSpace F] {f : F → 𝕜} {x : F} {frechet : F →L[𝕜] 𝕜} {s : Set F},
HasFDerivWithinAt f frechet s x → HasGradientWithinAt f ((InnerProductSpace.toDual 𝕜 F).symm frechet) s x
This theorem, named `HasFDerivWithinAt.hasGradientWithinAt`, is an alias of the forward direction of the `hasFDerivWithinAt_iff_hasGradientWithinAt` theorem. It states that for any real or complex-like field `𝕜`, any normed additive commutative group `F` that also forms an inner product space over `𝕜`, and any function `f : F → 𝕜`, if `f` has a Fréchet derivative `frechet` at some point `x` within a set `s` of `F`, then `f` also has a gradient at `x` within `s`. The gradient is related to the Fréchet derivative by the inverse of the Fréchet-Riesz representation mapping from `F` to its dual space.
More concisely: If a real or complex-function `f` has a Fréchet derivative at some point `x` in a set `s` of a normed additive commutative group `F` that forms an inner product space, then `f` has a gradient at `x` within `s`, which is related to the Fréchet derivative through the inverse of the Fréchet-Riesz representation mapping.
|
HasGradientWithinAt.hasFDerivWithinAt
theorem HasGradientWithinAt.hasFDerivWithinAt :
∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
[inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F} {s : Set F},
HasGradientWithinAt f f' s x → HasFDerivWithinAt f ((InnerProductSpace.toDual 𝕜 F) f') s x
The theorem `HasGradientWithinAt.hasFDerivWithinAt` states that given a field `𝕜`, a normed additive commutative group `F`, an inner product space over `𝕜` and `F`, and a complete space `F`, if a function `f` from `F` to `𝕜` has a gradient `f'` at a point `x` within a subset `s` of `F`, then the function `f` has a Fréchet derivative (`HasFDerivWithinAt`) within the subset `s` at the point `x`, and this Fréchet derivative is the dual representation (`InnerProductSpace.toDual`) of `f'`. The dual representation here refers to the Fréchet-Riesz representation theorem, which states that any linear form (dual space element) in a Hilbert space `E` can be uniquely represented as an inner product with some `y : E`.
More concisely: Given a field 𝕜, a normed additive commutative group F, an inner product space over 𝕜 and F, and a complete space F, if a function f from F to 𝕜 has a gradient f' at x in F that lies within a subset s of F, then f has a Fréchet derivative f'_F within s at x equal to the inner product representation of f'.
|
HasFDerivAt.hasGradientAt
theorem HasFDerivAt.hasGradientAt :
∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
[inst_3 : CompleteSpace F] {f : F → 𝕜} {x : F} {frechet : F →L[𝕜] 𝕜},
HasFDerivAt f frechet x → HasGradientAt f ((InnerProductSpace.toDual 𝕜 F).symm frechet) x
This theorem, referred to as an alias of the forward direction of `hasFDerivAt_iff_hasGradientAt`, states that for any type `𝕜` which behaves like a real or complex number, any type `F` which is a normed additive commutative group with an inner product space over `𝕜` and is a complete space, a function `f` from `F` to `𝕜`, a point `x` in `F`, and Fréchet derivative `frechet` (a continuous linear map from `F` to `𝕜`), if `f` has Fréchet derivative `frechet` at `x`, then `f` also has a gradient at `x`. The gradient is represented as the inverse of mapping from `F` to its dual space under the Fréchet-Riesz representation applied to `frechet`. This theorem is essentially describing the relationship between the Fréchet derivative and the gradient of a function in the context of a Hilbert space.
More concisely: In a complete normed additive commutative group with an inner product space over a real or complex number field, if a function has a continuous linear Fréchet derivative at a point, then it has a gradient represented as the inverse image of its derivative under the Fréchet-Riesz representation.
|
HasGradientAt.hasFDerivAt
theorem HasGradientAt.hasFDerivAt :
∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
[inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F},
HasGradientAt f f' x → HasFDerivAt f ((InnerProductSpace.toDual 𝕜 F) f') x
This theorem, called "HasGradientAt.hasFDerivAt", is an alias for the forward direction of "hasGradientAt_iff_hasFDerivAt". It states that for any type 𝕜, and any function 'f' from type F → 𝕜, if 'f' has a gradient 'f'' at a point 'x' (where 𝕜, F and 'x' are of type F), then 'f' has a Fréchet derivative at 'x', which is the continuous linear map associated with 'f'' through the Fréchet-Riesz representation (given by the function InnerProductSpace.toDual). This theorem holds under the conditions that 𝕜 has a scalar multiplication operation, F is a normed commutative additive group and a complete space, and there is an inner product space over 𝕜 and F.
More concisely: If a function from a normed commutative additive group into a Banach space with an inner product has a gradient at a point, then it has a Fréchet derivative at that point, which is the continuous linear map associated with the gradient through the Fréchet-Riesz representation.
|