Multiindex notation

Stream: Is there code for X?

[Moritz Doll]

Is there multiindex notation in lean? I.e., for $x \in \mathbb{R}^d$ and $\alpha \in \mathbb{N}^d$ the definitions $x^\alpha \coloneqq \prod_k x_k^{\alpha_k}$ and $\partial^\alpha f(x) \coloneqq \partial_{x_1}^{\alpha_1} \dotsc \partial_{x_d}^{\alpha_d} f(x)$.

[Patrick Massot]

I don't think so

[Patrick Massot]

We have very little support for partial derivatives. We always use the full derivative, as a (continuous) linear map.

[Eric Wieser]

I think the former might be (a • to_add x).to_mul, but I doubt you actually want to do that

[Moritz Doll]

Is there any reason to avoid partial derivatives for the definition of the Schwartz spaces?

[Sebastien Gouezel]

The question would rather be, is there any reason to use them? The condition would just be that, for any n, the norm of the n-th derivative decays faster than any polynomial at infinity, no need of partial derivatives to state this.

[Sebastien Gouezel]

Note that, in a general finite-dimensional real vector space, there is no preferred coordinate basis, so using partial derivatives would mean choosing an arbitrary basis first, which is not very natural.

[Moritz Doll]

you need partial derivatives at the latest if you want to calculate the Fourier transform of a polynomial. Also, polynomials in general vector spaces are probably awkward to handle (I haven't found any code for that); you could just take powers of the norm, but that makes the seminorms really messy.

[Heather Macbeth]

@Moritz Doll For polynomials in general vector spaces, we could use the symmetric algebra, or we could do a finitely-supported analogue of docs#formal_multilinear_series .

[Heather Macbeth]

(Not necessarily advocating this -- co-ordinates are convenient -- just thinking about how it would go to continue to eschew them!)

[Heather Macbeth]

So something like

def abstract_mv_polynomial
  (𝕜 : Type*) [nondiscrete_normed_field 𝕜]
  (E : Type*) [normed_group E] [normed_space 𝕜 E]
  (F : Type*) [normed_group F] [normed_space 𝕜 F] :=
Π₀ (n : ℕ), (E [×n]→L[𝕜] F)

where the Π₀, which you might not have seen before, is notation for docs#dfinsupp

[Heather Macbeth]

I would be curious if @Yourong Zang would comment here too. He encountered some fairly hairy issues last summer trying to do do multiple-derivatives in our Fréchet derivative framework.

[Heather Macbeth]

This was for arguments such as the one in the PDF linked in this message.

[Heather Macbeth]

At the time, I meant to go through his draft code and try to extract some #mwe for discussion explaining why it was so painful, but I didn't get around to it.