Commit 2024-05-08 13:10 6d1b4e77

feat: iterated derivative of a continuous multilinear map (#12207) Consider a multilinear map f : E^n -> F. Then its k-th derivative can be written as follows, given a basepoint x : E^n and k vectors v_1, ..., v_k : E^n:

D^k f (x; v_1, ..., v_k) = \sum f (x_1, (v_{e.symm 2})_2, x_3, ..., (v_{e.symm n))_n)

where in the sum at each index i one uses either the i-th coordinate of x, or the i-th coordinate of one of the vectors v_j, and each v_j has to appear exactly once in this expression. The sum is parameterized by the embeddings e of Fin k in Fin n. This expression is a little bit cumbersome to write down and to use, but it gives nice explicit bounds on ||D^k f|| that are useful to study Fourier transforms. The PR introduces the formal definition of each term in the sum (as an object which is multilinear in the coordinates of x outside the range of e, and in the v_j), and then proves that the sum is indeed the iterated derivative of f.