Continuity of bilinear maps

Stream: maths

[David Loeffler]

What's the least painful way of filling in the following sorry?

import analysis.normed_space.bounded_linear_maps

noncomputable theory

variables
  {V : Type*} [normed_add_comm_group V] [normed_space ℝ V]
  {W : Type*} [normed_add_comm_group W] [normed_space ℝ W]

lemma continuous_to_bilinear_map (L : V →L[ℝ] W →L[ℝ] ℝ) :
  continuous (λ p : V × W, L p.1 p.2) := sorry

I can bash out a proof by hand by choosing explicit epsilons and deltas etc, but it's disgusting. I found some general results about "currying" and "uncurrying" of continuous multilinear maps but I can't see how to use these here. I'd be grateful for any suggestions.

[David Loeffler]

(Context: in the library, continuous bilinear maps seem to be usually written in "curried" form; so continuous maps V × W → ℝ get written as V →L[ℝ] W →L[ℝ] ℝ, i.e. continuous maps from V to the space of continuous maps W → ℝ. However, I'm struggling to extract the continuity condition for the uncurried map from the curried one.)

[Eric Wieser]

continuous_linear_map.continuous₂? (edit: docs# doesn't work with the ₂)

[David Loeffler]

Ok, that seems to work! I was looking for things with uncurry in the name. Thanks!

[Scott Morrison]

@David Loeffler, here's a good meta-answer:

import analysis.normed_space.bounded_linear_maps

noncomputable theory

variables
  {V : Type*} [normed_add_comm_group V] [normed_space ℝ V]
  {W : Type*} [normed_add_comm_group W] [normed_space ℝ W]

lemma continuous_to_bilinear_map (L : V →L[ℝ] W →L[ℝ] ℝ) :
  continuous (λ p : V × W, L p.1 p.2) := by library_search!

[Scott Morrison]

(Sadly library_search is slow when you have lots of imports. Happily it is somewhat faster in Lean 4.)

[David Loeffler]

Scott Morrison said:

  continuous (λ p : V × W, L p.1 p.2) := by library_search!

I had tried library_search of course, but I didn't know library_search worked better if you shouted at it :-) I'll have to remember that in future.

(I think library_search actually timed out, rather than returning a failure message, in the original context where I had many more imports open. So another takeaway here is to make a MWE and _then_ try library_search! on it.)

[Kevin Buzzard]

For best results, make sure you only import the file containing the definition you're looking for.

[David Loeffler]

Kevin Buzzard said:

For best results, make sure you only import the file containing the definition you're looking for.

Doesn't that actually guarantee the worst results, since it ensures that lemmas which aren't in the same file as the definition won't get found? If your only metric for a search algorithm is how fast it runs then clearly the optimal answer is to return fail in all cases :-)

[Alex J. Best]

If library search is timing out and you are willing to wait for it ( :coffee:) you can always locally set the timeouts / memory limits to be longer using https://leanprover-community.github.io/tips_and_tricks.html#memory-and-deterministic-timeout (I believe you should increase both values mentioned there)

[Scott Morrison]

Also, library_search in mathlib4 will soon automatically stop work before timing out, reporting what it has found so far and warning that you might need to run with a longer maxHeartbeats.