Zulip Chat Archive

Stream: maths

Topic: multilinear right curry


view this post on Zulip Heather Macbeth (Jul 06 2020 at 22:46):

I would like to use multilinear_map.curry_right (link), which turns a multilinear map A:V0××VnWA:V_0\times \cdots \times V_{n}\to W to a multilinear map A^:V0××Vn1Hom(Vn,W)\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{0,1,n}i\in \{0,1,\ldots n\}, instead of always having i=ni=n.

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

view this post on Zulip Yury G. Kudryashov (Jul 06 2020 at 23:45):

We should ask @Sebastien Gouezel

view this post on Zulip Heather Macbeth (Jul 06 2020 at 23:47):

Yes, when he wakes up ...

view this post on Zulip Heather Macbeth (Jul 07 2020 at 05:47):

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' := _ }

view this post on Zulip Sebastien Gouezel (Jul 07 2020 at 06:43):

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.

view this post on Zulip Sebastien Gouezel (Jul 07 2020 at 09:13):

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?

view this post on Zulip Heather Macbeth (Jul 07 2020 at 14:18):

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:V0×V1××VnWA:V_0\times V_1\times \cdots \times V_n\to W
at (x0,xn)(x_0,\ldots x_n), which is the linear map
(v0,vn)A(v0,x1,xn)+A(x0,v1,x2,xn)++A(x0,xn1,vn)(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?

view this post on Zulip Sebastien Gouezel (Jul 07 2020 at 14:51):

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 :-)

view this post on Zulip Heather Macbeth (Jul 07 2020 at 16:44):

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

view this post on Zulip Sebastien Gouezel (Jul 07 2020 at 16:46):

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

view this post on Zulip Heather Macbeth (Jul 07 2020 at 17:09):

Thinking about this some more -- the advantage of doing it via the giant refactor is that the derivative of a (n+1)(n+1)-multilinear function is expressed in terms of nn-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?

view this post on Zulip Heather Macbeth (Jul 07 2020 at 17:09):

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

view this post on Zulip Heather Macbeth (Jul 08 2020 at 12:12):

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

view this post on Zulip Sebastien Gouezel (Jul 08 2020 at 12:17):

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 vA(v,,v)v \mapsto A(v, \dotsc, v) when AA is nn-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.

view this post on Zulip Sebastien Gouezel (Jul 08 2020 at 12:24):

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

view this post on Zulip Heather Macbeth (Jul 08 2020 at 12:34):

Let A^i:V0××Vi1×Vi+1××VnHom(Vi,W)\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 ii-th right curry of the (n+1)(n+1)-multilinear map A:V0××VnWA:V_0\times \cdots \times V_{n}\to W. Then A^i\widehat A_i is a nn-multilinear map.

The derivative of AA is the sum over i of
piA^iqip_i\circ \widehat A_i \circ q_i
where pi:Hom(Vi,W)Hom(V0××Vn,W)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 :V0××VnVi:V_0\times\cdots \times V_n\to V_i (lcomp W in Lean), and qi:V0××VnV0××Vi1×Vi+1××Vnq_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 nn-multilinear composed with linear; then if one has as an inductive hypothesis that nn-multilinears are smooth, it follows that (n+1)(n+1)-multilinears are smooth. Am I underestimating the difficulty of this argument? :)

view this post on Zulip Sebastien Gouezel (Jul 08 2020 at 12:37):

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 :)

view this post on Zulip Heather Macbeth (Jul 08 2020 at 12:42):

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)

view this post on Zulip Sebastien Gouezel (Jul 08 2020 at 12:49):

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

view this post on Zulip Heather Macbeth (Jul 08 2020 at 12:54):

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

view this post on Zulip Sebastien Gouezel (Jul 08 2020 at 12:54):

docs#is_bounded_bilinear_map.times_cont_diff

view this post on Zulip Sebastien Gouezel (Jul 08 2020 at 12:55):

Ah crap, this is not the right syntax

view this post on Zulip Johan Commelin (Jul 08 2020 at 12:55):

You need an s

view this post on Zulip Johan Commelin (Jul 08 2020 at 12:55):

docs#xyzzy

view this post on Zulip Sebastien Gouezel (Jul 08 2020 at 12:56):

Thanks!

view this post on Zulip Sebastien Gouezel (Jul 08 2020 at 12:56):

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

view this post on Zulip Heather Macbeth (Jul 08 2020 at 12:59):

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.


Last updated: May 11 2021 at 16:22 UTC