Continuity of pointwise tensor product

Stream: maths

[Heather Macbeth]

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.

[Yury G. Kudryashov]

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

[Heather Macbeth]

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: \mathbb{R}\to E$ and $g:\mathbb{R}\to F$, to prove that $f\otimes g:\mathbb{R}\to E\otimes F$, defined by $(f\otimes g)(x) := f(x) \otimes g(x)$, is continuous.

[Yury G. Kudryashov]

Can't find anything.

[Yury G. Kudryashov]

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

[Heather Macbeth]

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

[Yury G. Kudryashov]

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.

[Yury G. Kudryashov]

BTW, is it important that $E$ and $F$ have finite dimension?

[Heather Macbeth]

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

[Heather Macbeth]

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

[Yury G. Kudryashov]

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

[Heather Macbeth]

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?

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

Or at least "any bilinear map is continuous".

[Yury G. Kudryashov]

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.

[Sebastien Gouezel]

The difficulty is to put a topology on the tensor product: in general, there are uncountably many different "nice" topologies on $E \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).

[Sebastien Gouezel]

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

[Heather Macbeth]

Thank you!