HasFDerivAt.restrictScalars
theorem HasFDerivAt.restrictScalars :
β (π : Type u_1) [inst : NontriviallyNormedField π] {π' : Type u_2} [inst_1 : NontriviallyNormedField π']
[inst_2 : NormedAlgebra π π'] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace π E]
[inst_5 : NormedSpace π' E] [inst_6 : IsScalarTower π π' E] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
[inst_8 : NormedSpace π F] [inst_9 : NormedSpace π' F] [inst_10 : IsScalarTower π π' F] {f : E β F}
{f' : E βL[π'] F} {x : E}, HasFDerivAt f f' x β HasFDerivAt f (ContinuousLinearMap.restrictScalars π f') x
The theorem `HasFDerivAt.restrictScalars` states that for any non-trivially normed fields `π` and `π'` with a normed algebra structure between them, any normed additive commutative groups `E` and `F` made into normed spaces over `π` and `π'` which also forms a scalar tower, if a function `f : E β F` has a continuous linear map `f' : E βL[π'] F` as its derivative at a point `x` in `E` (i.e., `HasFDerivAt f f' x`), then `f` also has the derivative `ContinuousLinearMap.restrictScalars π f'`, which is the restriction of `f'` to the scalars `π`, at the same point `x` (i.e., `HasFDerivAt f (ContinuousLinearMap.restrictScalars π f') x`). In other words, the derivative of the function `f` remains the same when we restrict the scalars from `π'` to `π`.
More concisely: The theorem asserts that if a continuous linear map is the derivative of a function between two normed vector spaces over non-trivially normed fields and forms a scalar tower, then the restriction of the linear map to the base field is also the derivative of the function at that point.
|
HasFDerivWithinAt.restrictScalars
theorem HasFDerivWithinAt.restrictScalars :
β (π : Type u_1) [inst : NontriviallyNormedField π] {π' : Type u_2} [inst_1 : NontriviallyNormedField π']
[inst_2 : NormedAlgebra π π'] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace π E]
[inst_5 : NormedSpace π' E] [inst_6 : IsScalarTower π π' E] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
[inst_8 : NormedSpace π F] [inst_9 : NormedSpace π' F] [inst_10 : IsScalarTower π π' F] {f : E β F}
{f' : E βL[π'] F} {s : Set E} {x : E},
HasFDerivWithinAt f f' s x β HasFDerivWithinAt f (ContinuousLinearMap.restrictScalars π f') s x
This theorem, `HasFDerivWithinAt.restrictScalars`, states that for any non-trivially normed fields `π` and `π'` and any normed algebra structure between them, given a set of elements `E` with a normed add commutative group structure and a normed space over `π` and `π'`, and assuming that `π'` is a scalar tower over `E`, if we have another set `F` with a similar structure and `π'` is a scalar tower over `F`, then for any function `f` from `E` to `F` and a continuous linear map `f'` from `E` to `F` over `π'`, and a set `s` of elements in `E` and an element `x` in `E`, if `f` has a derivative within the set `s` at the point `x`, then `f` also has a derivative within the set `s` at the point `x` when we restrict the scalars to `π` in the continuous linear map `f'`.
More concisely: If `π` and `π'` are non-trivially normed fields with a normed algebra structure between them, `E` and `F` are normed spaces with commutative additive groups over `π` and `π'`, `π'` is a scalar tower over both `E` and `F`, `f` is a function from `E` to `F` with a derivative within `s` at `x` in `E`, and `f'` is a continuous linear map from `E` to `F` over `π'`, then `f` has a derivative within `s` at `x` when restricting scalars to `π` in `f'`.
|