multilinear right curry

Stream: maths

[Heather Macbeth]

I would like to use multilinear_map.curry_right (link), which turns a multilinear map $A:V_0\times \cdots \times V_{n}\to W$ to a multilinear map $\widehat A:V_0\times \cdots \times V_{n-1}\to\operatorname{Hom}(V_{n},W)$. However, I would like to choose my index $i\in \{0,1,\ldots n\}$, instead of always having $i=n$.

Does the library offer a clever way to do this? Or is the naive way (juggling permutations of $\{0,1,\ldots n\}$) the only way?

[Yury G. Kudryashov]

We should ask @Sebastien Gouezel

[Heather Macbeth]

Yes, when he wakes up ...

[Heather Macbeth]

To be more precise, I am curious about whether one could, and whether one should, develop the theory along these lines (apologies if my fintype code is not very idiomatic):

import linear_algebra.multilinear

open_locale big_operators
variables {R : Type*} [comm_ring R]
variables {ι : Type*} [fintype ι] [decidable_eq ι]
variables {M₁ : ι → Type*} [∀i, add_comm_monoid (M₁ i)] [∀i, semimodule R (M₁ i)]
variables {M₂ : Type*} [add_comm_monoid M₂] [semimodule R M₂]

def snoc' {i₀ : ι} (m : Π (i : {i // i ≠ i₀}), M₁ ↑i) (x : M₁ i₀) : Π (i : ι), M₁ i :=
λ i, if h : i = i₀ then by {rw h, exact x} else m ⟨i, h⟩

def multilinear_map.curry_right' (A : multilinear_map R M₁ M₂) (i₀ : ι) :
  multilinear_map R (λ (i : { i : ι // i ≠ i₀}), M₁ (i : ι)) (M₁ i₀ →ₗ[R] M₂) :=
{ to_fun := λ m,
  { to_fun    := λ x, A (snoc' m x),
    map_add'  := _,
    map_smul' := _ },
  map_add' := _,
  map_smul' := _ }

[Sebastien Gouezel]

Currently, the library is only designed with fin n in mind, because this is what I needed for iterated derivatives. If you have an application where the more general situation you describe is useful, I say go for it!

My only worry would be that the type {i : fin (n+1) // i \ne n} is not the same as fin n, so one could not readily express the n + 1-th derivative in this formalism. Maybe generalize even more, considering two types \alpha and \beta and a structure containing a map from \alpha to \beta, an element x of \beta, and the information that the map is a bijection between \alpha and \beta - {x}? (In other words, instead of using a subtype, use the universal property of the subtype). In this setup, I am not sure it is worth doing it dependently (i.e., should M1 i depend on i or just be a constant?), since the dependent case will be even more painful -- it will depend on your applications.

[Sebastien Gouezel]

Thinking back about it, there is something else missing: a multilinear function on a sum type can be seen as a multilinear function on the first factor, taking values in multilinear functions on the second factor. This is the most general currying version for multilinear maps, and probably the one we should implement. So, my suggestion would be to implement the following:

• a bijection of index types gives an equiv between multilinear maps
• on a sum type, currying multilinear maps into multilinear maps to multilinear maps
• compose these and the equiv between 1-multilinear maps and linear maps to express everything.

Does it look reasonable?

[Heather Macbeth]

Thanks! Yes, it does. Before I try this refactor, let me tell you the application I had in mind: I want to state the formula for the derivative of the multilinear map
$A:V_0\times V_1\times \cdots \times V_n\to W$
at $(x_0,\ldots x_n)$, which is the linear map
$(v_0,\ldots v_n)\mapsto A(v_0,x_1,\ldots x_n)+A(x_0,v_1,x_2,\ldots x_n)+\cdots+A(x_0,\ldots x_{n-1},v_n)$.
There isn't a good way of stating this without the refactor, is there?

[Sebastien Gouezel]

You can also go the direct route, defining this function with something like

def my_derivative [fintype ι] (f : multilinear_map R M₁ M₂) (x : Πi, M₁ i) : (Πi, M₁ i) →ₗ[R] M₂ :=
{ to_fun := λ v, (∑ i, f (update x i (v i))),
  map_add' := sorry,
  map_smul' := sorry, }

I think this would be less painful (by far!) than the refactor :-)

[Heather Macbeth]

Ah, this is great, I didn't know about update. Thanks for saving me from that rabbit hole!

[Sebastien Gouezel]

All the multilinear algebra is expressed with update, this is the way we describe what happens when we change just one variable.

[Heather Macbeth]

Thinking about this some more -- the advantage of doing it via the giant refactor is that the derivative of a $(n+1)$-multilinear function is expressed in terms of $n$-multilinear functions, which allows one to prove the existence of second, third, etc. derivatives by induction. I don't see a way of making that work if I go the direct way, do you?

[Heather Macbeth]

But what I could instead do is to use explicit formulas involving update for the second, third, ... derivatives.

[Heather Macbeth]

@Sebastien Gouezel, sorry, you might have missed this last question?

[Sebastien Gouezel]

It is not clear to me how the refactor would help here, in fact. I am afraid it will be messy in any case. Something which would probably be less messy is to express the iterated derivatives of $v \mapsto A(v, \dotsc, v)$ when $A$ is $n$-multilinear, because the formula is much nicer. So, everything depends on what you really need or want.

To see if the refactor is worth it or not, you could try to write down just the statements, assuming that the refactor is done, and see if it helps or not.

[Sebastien Gouezel]

In fact, even the pen and paper version is ugly to write here!

[Heather Macbeth]

Let $\widehat A_i:V_0\times \cdots\times V_{i-1}\times V_{i+1}\times\cdots \times V_{n}\to\operatorname{Hom}(V_{i},W)$ be the $i$-th right curry of the $(n+1)$-multilinear map $A:V_0\times \cdots \times V_{n}\to W$. Then $\widehat A_i$ is a $n$-multilinear map.

The derivative of $A$ is the sum over i of
$p_i\circ \widehat A_i \circ q_i$
where $p_i:\operatorname{Hom}(V_{i},W)\to \operatorname{Hom}(V_0\times\cdots \times V_n,W)$ is the induced linear map from the projection $:V_0\times\cdots \times V_n\to V_i$ (lcomp W in Lean), and $q_i:V_0\times\cdots \times V_n\to V_0\times \cdots\times V_{i-1}\times V_{i+1}\times\cdots \times V_{n}$ is the projection.

So, linear composed with $n$-multilinear composed with linear; then if one has as an inductive hypothesis that $n$-multilinears are smooth, it follows that $(n+1)$-multilinears are smooth. Am I underestimating the difficulty of this argument? :)

[Sebastien Gouezel]

Do you want to know that a multilinear map is smooth, or do you want a formula for the iterated derivative? If you just want smoothness, your argument is perfect (and very smooth :)

[Heather Macbeth]

I can do whatever you think is most useful for mathlib, but my own goal is just the smoothness (I am trying to do the inverse function theorem in the smooth category, following, eg, Example 8.12.11 here)

[Sebastien Gouezel]

For this proof, you only need to know that bilinear maps are smooth, right? And this we already know, I think.

[Heather Macbeth]

Oh, really? What file is it in? I missed that.

[Sebastien Gouezel]

docs#is_bounded_bilinear_map.times_cont_diff

[Sebastien Gouezel]

Ah crap, this is not the right syntax

[Johan Commelin]

You need an s

[Johan Commelin]

docs#xyzzy

[Sebastien Gouezel]

Thanks!

[Sebastien Gouezel]

I use it to prove that the composition of smooth functions is smooth, essentially following the proof in the link you gave.

[Heather Macbeth]

This is great, thanks. I knew about normed_space.multilinear but hadn't realised there was an is_bounded_bilinear_map inside normed_space.bounded_linear_maps.