Continuity of multilinear maps in finite dimensions

Stream: Is there code for X?

[Oliver Nash]

Do we have this anywhere (it looks like we don't):

import analysis.normed_space.finite_dimension
import analysis.normed_space.multilinear

variables {ι 𝕜 F : Type*} {E : ι → Type*}
variables [decidable_eq ι] [fintype ι] [nondiscrete_normed_field 𝕜] [complete_space 𝕜]
variables [normed_group F] [normed_space 𝕜 F]
variables [∀ i, normed_group (E i)] [∀ i, normed_space 𝕜 (E i)] [∀ i, finite_dimensional 𝕜 (E i)]

lemma multilinear_map.continuous_of_finite_dimensional (f : multilinear_map 𝕜 E F) : continuous f :=
begin
  sorry,
end

[Oliver Nash]

I think there's an easy proof if we add the unnecessary assumption that F is finite-dimensional by just inductively iterating docs#linear_map.continuous_of_finite_dimensional and using the continuity of the linear evaluation map.

[Oliver Nash]

I can also think of alternative proofs, of course (e.g., prove that docs#pi_tensor_product.tprod is continuous for finite family in finite dimensions, after setting everything up).

[Oliver Nash]

Actually I think I like the proof that assumes F is finite-dimensional because if / when we get the setup in place to be able to have a topology on the tensor product, we can immediately deduce continuity of docs#pi_tensor_product.tprod by just taking F = ⨂[𝕜] i, E i and from there trivially deduce the result when F is not finite-dimensional. So we can separate out the work.

[Oliver Nash]

I'll see if I can plug this gap in the next few (working) days.

[Oliver Nash]

I guess this is step 0:

example [finite_dimensional 𝕜 F] : finite_dimensional 𝕜 (multilinear_map 𝕜 E F) := sorry