English
Second formulation of the auxiliary equality for iterated derivatives with the same setup, emphasizing the symmetry in variables.
Русский
Вторая формулировка вспомогательного равенства для итеративной производной с тем же набором переменных, подчёркивающая симметрию переменных.
LaTeX
$$$$ \text{iteratedFDeriv_aux}(s,e,m,a,z) = \text{iterated form involving } e \, \text{and} \ z $$$$
Lean4
/-- Given a predicate `P`, one may associate to a multilinear map `f` a multilinear map
from the elements satisfying `P` to the multilinear maps on elements not satisfying `P`.
In other words, splitting the variables into two subsets one gets a multilinear map into
multilinear maps.
This is a linear map version of the function `MultilinearMap.domDomRestrict`. -/
def domDomRestrictₗ (f : MultilinearMap R M₁ M₂) (P : ι → Prop) [DecidablePred P] :
MultilinearMap R (fun (i : { a : ι // ¬P a }) => M₁ i) (MultilinearMap R (fun (i : { a : ι // P a }) => M₁ i) M₂)
where
toFun := fun z ↦ domDomRestrict f P z
map_update_add' := by
intro h m i x y
classical
ext v
simp [domDomRestrict_aux_right]
map_update_smul' := by
intro h m i c x
classical
ext v
simp [domDomRestrict_aux_right]
