English
Iterating partial derivatives along a finite family of directions m: Fin n → E yields the iterated partial derivative on Schwartz space, defined recursively by pderivCLM and the previous iterates.
Русский
Повторное взятие частных производных вдоль конечного набора направлений m: Fin n → E даёт итеративную частную производную на пространстве Шварца, определяемую рекурсивно через pderivCLM и предыдущие итерации.
LaTeX
$$$\text{iteratedPDeriv} 𝕜\, m : (Fin\, n \to E) \to 𝓢(E, F) \toL 𝓢(E, F)$$$
Lean4
/-- The iterated partial derivative (or directional derivative) as a continuous linear map on
Schwartz space. -/
def iteratedPDeriv {n : ℕ} : (Fin n → E) → 𝓢(E, F) →L[𝕜] 𝓢(E, F) :=
Nat.recOn n (fun _ => ContinuousLinearMap.id 𝕜 _) fun _ rec x => (pderivCLM 𝕜 (x 0)).comp (rec (Fin.tail x))
