IsBoundedBilinearMap.differentiableAt
theorem IsBoundedBilinearMap.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]
{G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace π G] {b : E Γ F β G},
IsBoundedBilinearMap π b β β (p : E Γ F), DifferentiableAt π b p
This theorem states that for any non-trivially normed field π, if we have a bounded bilinear map `b` from a Cartesian product of two normed vector spaces `E` and `F` into a normed vector space `G` over the field π, then `b` is differentiable at any point `p` in `E Γ F`. In other words, the bounded bilinear map `b` admits a derivative at every point in the domain `E Γ F`.
More concisely: For any non-trivially normed field π and bounded bilinear map `b` from the Cartesian product of two normed vector spaces `E` and `F` into a normed vector space `G`, `b` is differentiable at every point in `E Γ F`.
|
IsBoundedBilinearMap.hasFDerivAt
theorem IsBoundedBilinearMap.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]
{G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace π G] {b : E Γ F β G}
(h : IsBoundedBilinearMap π b) (p : E Γ F), HasFDerivAt b (h.deriv p) p
This theorem states that for any non-trivially normed field `π`, normed additive commutative groups `E`, `F`, and `G`, and the associated normed spaces, if the function `b` from pairs of `E` and `F` to `G` is a bounded bilinear map, then at any point `p` from the pair of `E` and `F`, `b` has a derivative. The derivative of `b` at `p` is the result of the function `IsBoundedBilinearMap.deriv` applied to `b` and `p`. In other words, the change in `b` near `p` can be accurately approximated by the function `IsBoundedBilinearMap.deriv h p`.
More concisely: Given a non-trivially normed field `π`, and normed additive commutative groups `E`, `F`, and `G`, if `b` is a bounded bilinear map from `E Γ F` to `G`, then `b` has a derivative at any point in `E Γ F`, which is given by the function `IsBoundedBilinearMap.deriv h` where `h` is the evaluation map at that point.
|