English
Definition of the iterated derivative component of a multilinear map: it is a multilinear map depending on a subset s and a bijection e : α ≃ s, built by restricting the original map outside s and varying the directions v_j.
Русский
Определение компоненты повторной производной для многолинейной карты: это многолинейная карта, зависящая от подмножества s и биекции e : α ≃ s, строимая путём ограничения исходной карты вне s и задания направлений v_j.
LaTeX
$${\text{iteratedFDerivComponent} : MultilinearMap R (f i) (..) → MultilinearMap R (..)}$$
Lean4
/-- One of the components of the iterated derivative of a multilinear map. Given a bijection `e`
between a type `α` (typically `Fin k`) and a subset `s` of `ι`, this component is a multilinear map
of `k` vectors `v₁, ..., vₖ`, mapping them to `f (x₁, (v_{e.symm 2})₂, x₃, ...)`, where at
indices `i` in `s` one uses the `i`-th coordinate of the vector `v_{e.symm i}` and otherwise one
uses the `i`-th coordinate of a reference vector `x`.
This is multilinear in the components of `x` outside of `s`, and in the `v_j`. -/
noncomputable def iteratedFDerivComponent {α : Type*} (f : MultilinearMap R M₁ M₂) {s : Set ι} (e : α ≃ s)
[DecidablePred (· ∈ s)] :
MultilinearMap R (fun (i : { a : ι // a ∉ s }) ↦ M₁ i) (MultilinearMap R (fun (_ : α) ↦ (∀ i, M₁ i)) M₂)
where
toFun := fun z ↦
{ toFun := fun v ↦ domDomRestrictₗ f (fun i ↦ i ∈ s) z (fun i ↦ v (e.symm i) i)
map_update_add' := by classical simp [iteratedFDeriv_aux]
map_update_smul' := by classical simp [iteratedFDeriv_aux] }
map_update_add' := by intros; ext; simp
map_update_smul' := by intros; ext; simp
