ContinuousLinearMap.hasStrictFDerivAt
theorem ContinuousLinearMap.hasStrictFDerivAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F]
(e : E βL[π] F) {x : E}, HasStrictFDerivAt (βe) e x
This theorem states that for any continuous linear map `e` from a normed additive commutative group `E` over a nontrivially normed field `π` to another normed additive commutative group `F` over the same field, the map has a strict Frechet derivative at any point `x` in `E`. In other words, it says that the derivative of the continuous linear map at any point is just the map itself.
More concisely: Given a continuous linear map `e` from a normed additive commutative group `E` over a nontrivially normed field `π` to another normed additive commutative group `F` over the same field, the map has a strict Frechet derivative equal to itself at every point in `E`.
|
IsBoundedLinearMap.differentiableAt
theorem IsBoundedLinearMap.differentiableAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{x : E}, IsBoundedLinearMap π f β DifferentiableAt π f x
This theorem states that for any nontrivially normed field `π`, normed additive commutative groups `E` and `F`, and a normed space over `π` for `E` and `F`, if `f` is a function from `E` to `F` and `f` is a bounded linear map, then `f` is differentiable at any point `x` in `E`. In other words, there exists a derivative for the function `f` at the point `x`.
More concisely: Given a nontrivially normed field `π`, any normed additive commutative groups `E` and `F`, and a normed space over `π` for both `E` and `F`, if `f` is a bounded linear map from `E` to `F`, then `f` is differentiable at every point in `E`.
|
ContinuousLinearMap.hasFDerivAt
theorem ContinuousLinearMap.hasFDerivAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F]
(e : E βL[π] F) {x : E}, HasFDerivAt (βe) e x
This theorem states that for any nontrivially normed field `π`, normed add commutative group `E`, and normed space `F` over `π`, a continuous linear map `e` from `E` to `F` has itself as its derivative at any point `x` in `E`. It says that the map given by `e` satisfies the condition that `f x' = f x + f' (x' - x) + o (x' - x)` as `x'` tends to `x`, where `f` is the function defined by `e` and `f'` is the derivative function, which is also `e` in this case.
More concisely: For any continuous linear map `e` from a normed additive group `E` to a normed space `F` over a nontrivially normed field `π`, `e` is its own derivative at any point `x` in `E`, i.e., `e(x') = e(x) + e(x'-x) + o(x'-x)` as `x'` approaches `x`.
|
ContinuousLinearMap.differentiable
theorem ContinuousLinearMap.differentiable :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F]
(e : E βL[π] F), Differentiable π βe
The theorem `ContinuousLinearMap.differentiable` states that for any continuous linear map `e` from a normed addtive commutative group `E` to another such group `F`, both equipped with a normed space structure over a non-trivially normed field `π`, the map `e` is differentiable at every point of `E`. In other words, all continuous linear maps are differentiable everywhere.
More concisely: Every continuous linear map between normed additive commutative groups, equipped with normed space structures over a non-trivially normed field, is differentiable.
|
ContinuousLinearMap.differentiableAt
theorem ContinuousLinearMap.differentiableAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F]
(e : E βL[π] F) {x : E}, DifferentiableAt π (βe) x
The theorem `ContinuousLinearMap.differentiableAt` states that for any point `x` in a normed vector space `E` over a nontrivially normed field `π`, and for any continuous linear map `e` from `E` to another normed vector space `F` over the same field `π`, the function represented by `e` is differentiable at `x`. In other words, it states that every continuous linear map is differentiable at every point of its domain.
More concisely: Every continuous linear map between normed vector spaces is differentiable at every point in its domain.
|
ContinuousLinearMap.hasFDerivAtFilter
theorem ContinuousLinearMap.hasFDerivAtFilter :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F]
(e : E βL[π] F) {x : E} {L : Filter E}, HasFDerivAtFilter (βe) e x L
This theorem states that, for any non-trivially normed field π, normed addition-commutative groups E and F, and normed spaces over E and F, a continuous linear map `e` from E to F has a Frechet derivative at a point `x` under a given filter `L`. The derivative is the map `e` itself. The Frechet derivative is a generalization of the derivative of a function at a point, suitable for use in infinite-dimensional spaces.
More concisely: Given a non-trivially normed field π, a continuous linear map `e` from a normed additive group `E` to another `F`, and a point `x` in `E` under filter `L`, the Frechet derivative of `e` at `x` exists and equals `e`.
|