linearDeriv — Mathlib

English

For a bounded bilinear map f, the map p ↦ f.deriv(p) is a bounded linear map from E × F to G.

Русский

Для ограниченного билинейного отображения f отображение p ↦ f.deriv(p) является ограниченным линейным отображением из E × F в G.

LaTeX

$$$IsBoundedLinearMap 𝕜 (\lambda p: E \times F, h.deriv p)$$$

Lean4

/-- Definition of the derivative of a bilinear map `f`, given at a point `p` by
`q ↦ f(p.1, q.2) + f(q.1, p.2)` as in the standard formula for the derivative of a product.
We define this function here as a linear map `E × F →ₗ[𝕜] G`, then `IsBoundedBilinearMap.deriv`
strengthens it to a continuous linear map `E × F →L[𝕜] G`.
-/
def linearDeriv (h : IsBoundedBilinearMap 𝕜 f) (p : E × F) : E × F →ₗ[𝕜] G :=
  (h.toContinuousLinearMap.deriv₂ p).toLinearMap

Похожие утверждения