English
Let f be a continuous multilinear map on a family of normed spaces, with a finite index set ι. Fix a subset s ⊆ ι and a bijection e: α ≃ s from a finite type α. For any family of vectors v indexed by {a ∈ ι : a ∉ s} and any function w: α → (∀ i, E_i), the k-th iterated derivative component of f along e, evaluated at v and w, equals the original map f applied to a vector whose entries in s are replaced by the corresponding entries coming from w via e, while entries outside s come from v. This expresses how the derivative component is obtained by substituting appropriate coordinates.
Русский
Пусть f — непрерывно многочленово-линейная отображение от семейства нормированных пространств с конечным индексом ι. Пусть s ⊆ ι и существует биекция e: α ≃ s. Для любой семейки векторов v, индексированной по {a ∈ ι : a ∉ s}, и для функции w: α → (∀ i, E_i), вернемая k-я компонентa итеративной производной f по выборке e: α → s равна f, примененному к вектору, у которого координаты из s заменены соответствующими координатами из w через e, а координаты вне s взяты из v. Это формулирует, как компонент итеративной производной получается заменой соответствующих координат.
LaTeX
$$$f.iteratedFDerivComponent\,e\,v\,w = f\Big(\lambda j. \text{if } j\in s\;\text{then } w (e^{-1}(j), h) \text{ else } v (j, h)\Big)$$$
Lean4
@[simp]
theorem iteratedFDerivComponent_apply {α : Type*} [Fintype α] (f : ContinuousMultilinearMap 𝕜 E₁ G) {s : Set ι}
(e : α ≃ s) [DecidablePred (· ∈ s)] (v : ∀ i : { a : ι // a ∉ s }, E₁ i) (w : α → (∀ i, E₁ i)) :
f.iteratedFDerivComponent e v w = f (fun j ↦ if h : j ∈ s then w (e.symm ⟨j, h⟩) j else v ⟨j, h⟩) := by
simp [iteratedFDerivComponent, MultilinearMap.iteratedFDerivComponent, MultilinearMap.domDomRestrictₗ]
