Images of (von Neumann) bounded sets under continuous multilinear maps

In this file we prove that continuous multilinear maps send von Neumann bounded sets to von Neumann bounded sets.

We prove 2 versions of the theorem: one assumes that the index type is nonempty, and the other assumes that the codomain is a topological vector space.

Implementation notes

We do not assume the index type ι to be finite. While for a nonzero continuous multilinear map the family ∀ i, E i has to be essentially finite (more precisely, all but finitely many E i has to be trivial), proving theorems without a [Finite ι] assumption saves us some typeclass searches here and there.

theorem Bornology.IsVonNBounded.image_multilinear' {ι : Type u_1} {𝕜 : Type u_2} {F : Type u_3} {E : ι → Type u_4} [NormedField 𝕜] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [(i : ι) → TopologicalSpace (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [Nonempty ι] {s : Set ((i : ι) → E i)} (hs : Bornology.IsVonNBounded 𝕜 s) (f : ContinuousMultilinearMap 𝕜 E F) : Bornology.IsVonNBounded 𝕜 (⇑f '' s)

The image of a von Neumann bounded set under a continuous multilinear map is von Neumann bounded.

This version does not assume that the topologies on the domain and on the codomain agree with the vector space structure in any way but it assumes that ι is nonempty.

theorem Bornology.IsVonNBounded.image_multilinear {ι : Type u_1} {𝕜 : Type u_2} {F : Type u_3} {E : ι → Type u_4} [NormedField 𝕜] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [(i : ι) → TopologicalSpace (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousSMul 𝕜 F] {s : Set ((i : ι) → E i)} (hs : Bornology.IsVonNBounded 𝕜 s) (f : ContinuousMultilinearMap 𝕜 E F) : Bornology.IsVonNBounded 𝕜 (⇑f '' s)

The image of a von Neumann bounded set under a continuous multilinear map is von Neumann bounded.

This version assumes that the codomain is a topological vector space.