ContinuousLinearMap.hasDerivAtFilter
theorem ContinuousLinearMap.hasDerivAtFilter :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {L : Filter 𝕜} (e : 𝕜 →L[𝕜] F), HasDerivAtFilter (⇑e) (e 1) x L
The theorem `ContinuousLinearMap.hasDerivAtFilter` states that for any non-trivial normed field `𝕜`, normed additive commutative group `F`, and normed space over `𝕜` and `F`, for any point `x` and filter `L` on `𝕜`, and any continuous linear map `e` from `𝕜` to `F`, the map `e` has a derivative at the point `x` as `x` goes along the filter `L`. The derivative is given by the application of `e` to 1. In mathematical terms, if `e` is a continuous linear map, then the equation `f(x') = f(x) + (x' - x) * f'(x) + o(x' - x)` holds where `x'` converges along the filter `L` and `f'` is the derivative of `f` at `x`.
More concisely: For any non-trivial normed field `𝕜`, normed additive commutative group `F`, and continuous linear map `e` from `𝕜` to `F`, if `x` is a point in `𝕜` and `L` is a filter on `𝕜`, then `e` has a derivative `e(1)` at `x` along the filter `L`, i.e., `e(x') = e(x) + (x' - x) * e(1) + o(1)` as `x'` converges to `x` through `L`.
|
ContinuousLinearMap.hasDerivAt
theorem ContinuousLinearMap.hasDerivAt :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace 𝕜 F] {x : 𝕜} (e : 𝕜 →L[𝕜] F), HasDerivAt (⇑e) (e 1) x
The theorem `ContinuousLinearMap.hasDerivAt` states that, for any type `𝕜` endowed with a non-trivially normed field structure, any type `F` forming a normed additive commutative group over `𝕜`, and any element `x` from `𝕜`, if `e` is a continuous linear map from `𝕜` to `F`, then `e` has a derivative at every point `x` in `𝕜`, and the derivative is `e` applied to `1`. In other words, this theorem ensures that the derivative of a continuous linear map is just the map itself applied to one, and this holds true at any point in the domain.
More concisely: For any normed field `𝕜`, normed additive commutative group `F` over `𝕜`, and continuous linear map `e` from `𝕜` to `F`, the derivative of `e` at any point `x` in `𝕜` is `e` itself.
|
LinearMap.hasDerivAtFilter
theorem LinearMap.hasDerivAtFilter :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {L : Filter 𝕜} (e : 𝕜 →ₗ[𝕜] F), HasDerivAtFilter (⇑e) (e 1) x L
The theorem `LinearMap.hasDerivAtFilter` asserts that for any nontrivially normed field `𝕜`, a normed additive commutative group `F`, and a normed space over `𝕜` and `F`, given any point `x` from `𝕜`, a filter `L` on `𝕜`, and a linear map `e` from `𝕜` to `F`, the function obtained by applying `e` has a derivative at `x` along the filter `L`. The derivative is the result of applying `e` to `1`. This means, in simpler terms, that the function represented by the linear map `e` changes at the point `x` at a rate given by the application of `e` to `1`, as `x` approaches along the filter `L`.
More concisely: Given a nontrivially normed field `𝕜`, a normed additive commutative group `F`, a normed space over `𝕜` and `F`, a point `x` in `𝕜`, a filter `L` on `𝕜`, and a linear map `e` from `𝕜` to `F`, the derivative of `e` at `x` along the filter `L` exists and is equal to `e 1`.
|