continuous bilinear map

Stream: Is there code for X?

[Floris van Doorn]

Is there a bilinear version of docs#continuous_linear_map or a bundled version of docs#is_bounded_bilinear_map? Or is someone working on this?
I'm realizing I need to generalize convolution to take a bilinear map as extra argument.

[Yaël Dillies]

I am semi-working on this with #11909 in the sense that we'll need this to do it the proper way.

[Yaël Dillies]

And, indeed, is_bounded_bilinear_map is the only thing that we have.

[Yaël Dillies]

However, it's still unclear to me whether currying works already.

[Floris van Doorn]

I think using the curried version doesn't buy you much, since I still want to use all the lemmas that you'd prove for a continuous_bilinear_map, (e.g. add_right, smul_right, "if f and g are continuous, then x ↦ L (f x) (g x) is continuous", ...)

[Frédéric Dupuis]

The curried version is the right object, but most of the relevant API might indeed be missing. One can at least convert using docs#continuous_linear_map.is_bounded_bilinear_map though.

[Floris van Doorn]

Good. I have indeed now written a little bit of API for the curried version, along the lines of

namespace continuous_linear_map

lemma map_add_left (L : E →L[ℝ] E' →L[ℝ] F) {x x' : E} {y : E'} : L (x + x') y = L x y + L x' y :=
by rw [L.map_add, add_apply]

lemma map_add_right (L : E →L[ℝ] E' →L[ℝ] F) {x : E} {y y' : E'} : L x (y + y') = L x y + L x y' :=
(L x).map_add y y'

lemma map_smul_left (L : E →L[ℝ] E' →L[ℝ] F) {c : ℝ} {x : E} {y : E'} : L (c • x) y = c • L x y :=
by rw [L.map_smul, smul_apply]

lemma map_smul_right (L : E →L[ℝ] E' →L[ℝ] F) {c : ℝ} {x : E} {y : E'} : L x (c • y) = c • L x y :=
(L x).map_smul c y

[...]

[Floris van Doorn]

(of course, I will generalize ℝ to 𝕜 and maybe →L to →SL in the version I PR)

[Eric Wieser]

map_add₂ might be a better name to match docs#linear_map.map_add₂

[Eric Wieser]

.. which obviously the linkifier doesn't link correctly... https://leanprover-community.github.io/mathlib_docs/find/linear_map.map_add%E2%82%82

[Floris van Doorn]

This should be easy from things in the library, but I cannot find a reasonably close result.

import analysis.normed_space.operator_norm

variables {𝕜 E₁ E₂ E₃ : Type*}
variables [nondiscrete_normed_field 𝕜]
variables [normed_group E₁] [normed_space 𝕜 E₁]
variables [normed_group E₂] [normed_space 𝕜 E₂]
variables [normed_group E₃] [normed_space 𝕜 E₃]

open function
lemma continuous₂ (L : E₁ →L[𝕜] E₂ →L[𝕜] E₃) : continuous (uncurry (λ x y, L x y)) :=
by { sorry }

[Patrick Massot]

import analysis.normed_space.operator_norm
import analysis.normed_space.bounded_linear_maps

variables {𝕜 E₁ E₂ E₃ : Type*}
variables [nondiscrete_normed_field 𝕜]
variables [normed_group E₁] [normed_space 𝕜 E₁]
variables [normed_group E₂] [normed_space 𝕜 E₂]
variables [normed_group E₃] [normed_space 𝕜 E₃]

open function
lemma continuous₂ (L : E₁ →L[𝕜] E₂ →L[𝕜] E₃) : continuous (uncurry (λ x y, L x y)) :=
L.is_bounded_bilinear_map.continuous

[Patrick Massot]

@Floris van Doorn

[Floris van Doorn]

Oh yes, of course. Thanks!