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.
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)?
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 and , to prove that , defined by , is continuous.
Yury G. Kudryashov (May 07 2020 at 06:09):
Can't find anything.
Yury G. Kudryashov (May 07 2020 at 06:10):
The main lemma should be the continuity of the tensor product itself as a map
Heather Macbeth (May 07 2020 at 06:15):
Thank you. Is that lemma (the continuity of the tensor product) in mathlib?
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.
Yury G. Kudryashov (May 07 2020 at 06:18):
BTW, is it important that and have finite dimension?
Heather Macbeth (May 07 2020 at 06:19):
No, I just put E and F finite-dimensional and R as the domain for simplicity.
Heather Macbeth (May 07 2020 at 06:21):
I guess this should be a fact for normed/topological vector spaces.
Yury G. Kudryashov (May 07 2020 at 06:21):
According to wiki, there is more than one natural norm on the tensor product.
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?
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".
Yury G. Kudryashov (May 07 2020 at 06:28):
It seems that we don't have this lemma yet.
Yury G. Kudryashov (May 07 2020 at 06:30):
Or at least "any bilinear map is continuous".
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.
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 (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 (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 . This is probably the simplest thing to do.
Heather Macbeth (May 07 2020 at 16:04):
Last updated: May 06 2021 at 19:30 UTC