pderivCLM — Mathlib

English

The directional derivative operator pderivCLM 𝕜 m on Schwartz(E, F) is the composition of the evaluation map with the derivative operator in direction m.

Русский

Директивная производная pderivCLM 𝕜 m на Schwartz(E,F) является композицией отображения значения и оператора производной по направлению m.

LaTeX

$$$pderivCLM 𝕜\, m : 𝓢(E, F) \toL 𝓢(E, F)$$$

Lean4

/-- The partial derivative (or directional derivative) in the direction `m : E` as a
continuous linear map on Schwartz space. -/
def pderivCLM (m : E) : 𝓢(E, F) →L[𝕜] 𝓢(E, F) :=
  (SchwartzMap.evalCLM m).comp (fderivCLM 𝕜)

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