family of linear maps is C^n if its applications are C^n

Stream: maths

[Floris van Doorn]

In the sphere eversion project (cc @Oliver Nash, @Patrick Massot) we have proven the following result, stating that a family of linear maps is C^n if its individual applications are C^n.

import analysis.calculus.cont_diff
variables {𝕜 E F G : Type*} {n : with_top ℕ}
variables [nondiscrete_normed_field 𝕜] [complete_space 𝕜]
variables [normed_group E] [normed_space 𝕜 E]
variables [normed_group F] [normed_space 𝕜 F]
variables [normed_group G] [normed_space 𝕜 G]

lemma cont_diff_clm_apply {n : with_top ℕ} {f : E → F →L[𝕜] G} [finite_dimensional 𝕜 F] :
  cont_diff 𝕜 n f ↔ ∀ y, cont_diff 𝕜 n (λ x, f x y)

The proof inherently assumes that F is finite dimensional. My question is whether this result is also valid for infinite dimensional F.

The reason why this is useful, is that this gives a characterization of being C^(n+1) in terms of functions with the same domain and codomain being C^n:

lemma cont_diff_succ_iff_fderiv_apply [finite_dimensional 𝕜 E] {n : ℕ} {f : E → F} :
  cont_diff 𝕜 ((n + 1) : ℕ) f ↔
  differentiable 𝕜 f ∧ ∀ y, cont_diff 𝕜 n (λ x, fderiv 𝕜 f x y)

This could be used in inductive arguments that prove cont_diff from a computation of fderiv (and similar results could be used for cont_diff_on theorems). The reason that this lemma is nice, is that you don't have to worry about universes, and you don't have to use tricks like proving it first for the special case where all types are in the same universe, and then lifting certain types to higher universes (like here).
We use this in the sphere eversion project to prove that parametric interval integrals of C^n functions are C^n.