English
The map x ↦ f.linearDeriv x evaluated at y equals the finite sum over i of f (update x i (y_i))
Русский
Пусть y — вектор; тогда f.linearDeriv x применительно к y равняется сумме по i от f(... обновление ...).
LaTeX
$$$ f.linearDeriv x y = \\sum_i f (update x i (y i)) $$$
Lean4
/-- Given a multilinear map `f` on `(i : ι) → M i`, a (decidable) predicate `P` on `ι` and
an element `z` of `(i : {a // ¬ P a}) → M₁ i`, construct a multilinear map on
`(i : {a // P a}) → M₁ i)` whose value at `x` is `f` evaluated at the vector with `i`th coordinate
`x i` if `P i` and `z i` otherwise.
The naming is similar to `MultilinearMap.domDomCongr`: here we are applying the restriction to the
domain of the domain.
For a linear map version, see `MultilinearMap.domDomRestrictₗ`.
-/
def domDomRestrict (f : MultilinearMap R M₁ M₂) (P : ι → Prop) [DecidablePred P] (z : (i : { a : ι // ¬P a }) → M₁ i) :
MultilinearMap R (fun (i : { a : ι // P a }) => M₁ i) M₂
where
toFun x := f (fun j ↦ if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩)
map_update_add' x i a
b := by
classical
repeat (rw [domDomRestrict_aux])
simp only [MultilinearMap.map_update_add]
map_update_smul' z i c
a := by
classical
repeat (rw [domDomRestrict_aux])
simp only [MultilinearMap.map_update_smul]
