Smoothness of linear evaluation map

Stream: Is there code for X?

[Oliver Nash]

I've just started using our amazing calculus technology. Do we have this, or something similar anywhere:

import analysis.calculus.times_cont_diff

variables (𝕜 E F : Type*) [nondiscrete_normed_field 𝕜] [complete_space 𝕜]
variables [normed_group E] [normed_space 𝕜 E] [finite_dimensional 𝕜 E]
variables [normed_group F] [normed_space 𝕜 F] [finite_dimensional 𝕜 F]

lemma times_cont_diff_continuous_linear_eval :
  times_cont_diff 𝕜 ⊤ $ λ p : (E →L[𝕜] F) × E, p.1 p.2 :=
begin
  sorry,
end

[Oliver Nash]

I.e., I want to use the smoothness of the evaluation map $Hom(E, F) \times E \to F$ for finite-dimensional normed vector spaces $E, F$.

[Heather Macbeth]

@Oliver Nash There is docs#is_bounded_bilinear_map_apply saying that evaluation is a bounded bilinear map, and docs#is_bounded_bilinear_map.times_cont_diff saying that a bounded bilinear map is smooth. I think that does it?

[Oliver Nash]

Oh thanks, looks like it does!

[Oliver Nash]

For the record:

import analysis.calculus.times_cont_diff

variables (𝕜 E F : Type*) [nondiscrete_normed_field 𝕜]
variables [normed_group E] [normed_space 𝕜 E]
variables [normed_group F] [normed_space 𝕜 F]

lemma times_cont_diff_continuous_linear_eval :
  times_cont_diff 𝕜 ⊤ $ λ p : (E →L[𝕜] F) × E, p.1 p.2 :=
is_bounded_bilinear_map_apply.times_cont_diff