Zulip Chat Archive

Stream: maths

Topic: Continuity of pointwise tensor product


view this post on Zulip Heather Macbeth (May 07 2020 at 05:56):

Does mathlib currently know that given finite-dimensional vector spaces E and F, the pointwise tensor product of continuous functions f : R -> E and g : R -> F is continuous? If yes, does this occur via a construction of a topological monoid structure on the (infinite-dimensional) algebra of all iterated tensor products of E and F?
I asked this to @Johan Commelin in the new members stream, and he sent me over here.

view this post on Zulip Yury G. Kudryashov (May 07 2020 at 05:59):

Could you please write exactly what function you are talking about (if possible, as a Lean lemma with no proof)?

view this post on Zulip Heather Macbeth (May 07 2020 at 06:02):

I'm sorry, I am new to Lean and don't know the tensor-product syntax in particular. But in LaTex: given continuous functions f:REf: \mathbb{R}\to E and g:RFg:\mathbb{R}\to F, to prove that fg:REFf\otimes g:\mathbb{R}\to E\otimes F, defined by (fg)(x):=f(x)g(x)(f\otimes g)(x) := f(x) \otimes g(x), is continuous.

view this post on Zulip Yury G. Kudryashov (May 07 2020 at 06:09):

Can't find anything.

view this post on Zulip Yury G. Kudryashov (May 07 2020 at 06:10):

The main lemma should be the continuity of the tensor product itself as a map E×FEFE\times F\to E\otimes F

view this post on Zulip Heather Macbeth (May 07 2020 at 06:15):

Thank you. Is that lemma (the continuity of the tensor product) in mathlib?

view this post on Zulip Yury G. Kudryashov (May 07 2020 at 06:17):

Not (yet). Let us ask @Sebastien Gouezel who wrote analysis/normed_space/finite_dimension whether we have some general fact that implies continuity of the tensor product in finite dimension spaces.

view this post on Zulip Yury G. Kudryashov (May 07 2020 at 06:18):

BTW, is it important that EE and FF have finite dimension?

view this post on Zulip Heather Macbeth (May 07 2020 at 06:19):

No, I just put E and F finite-dimensional and R as the domain for simplicity.

view this post on Zulip Heather Macbeth (May 07 2020 at 06:21):

I guess this should be a fact for normed/topological vector spaces.

view this post on Zulip Yury G. Kudryashov (May 07 2020 at 06:21):

According to wiki, there is more than one natural norm on the tensor product.

view this post on Zulip Heather Macbeth (May 07 2020 at 06:24):

I guess that's right, it's true even for matrices. I don't know whether it can occur (in infinite dimensions) that the natural norms are topologically inequivalent?

view this post on Zulip Yury G. Kudryashov (May 07 2020 at 06:26):

In case of finite dimensional spaces probably the right generality is "any multilinear map is continuous".

view this post on Zulip Yury G. Kudryashov (May 07 2020 at 06:28):

It seems that we don't have this lemma yet.

view this post on Zulip Yury G. Kudryashov (May 07 2020 at 06:30):

Or at least "any bilinear map is continuous".

view this post on Zulip Yury G. Kudryashov (May 07 2020 at 06:36):

Note that the hard work is already done in continuous_equiv_fun_basis, so you need a lemma similar to linear_map.continuous_on_pi and a lemma similar to linear_map.continuous_of_finite_dimensional. Both of them are relatively short.

view this post on Zulip Sebastien Gouezel (May 07 2020 at 07:22):

The difficulty is to put a topology on the tensor product: in general, there are uncountably many different "nice" topologies on EFE \otimes F (with two which are nicer than the others, but are distinct in general). Of course, they all coincide in finite dimension. So, this is definitely not in mathlib, but it could be done in this way:
1) construct a definition taking as input a finite-dimensional space over the reals (or more generally any nondiscrete normed field) and outputting some (any) normed space structure on it.
2) declare it locally as an instance.
3) Prove that any bilinear (or multilinear) map between finite-dimensional normed spaces over the reals (or more generally any nondiscrete normed field) is continuous. (This is already known for linear maps, so this shouldn't be hard).

view this post on Zulip Sebastien Gouezel (May 07 2020 at 08:02):

Or, to get rid of 1) and 2), you could just assume that there is some normed space structure on EFE \otimes F. This is probably the simplest thing to do.

view this post on Zulip Heather Macbeth (May 07 2020 at 16:04):

Thank you!


Last updated: May 06 2021 at 19:30 UTC