[Merged by Bors] - chore(linear_algebra/basic, analysis/normed_space/operator_norm): bundle another argument into the homs

[eric-wieser]

---

[sgouezel]

We already have the fact that the application of a continuous linear map is a continuous bilinear operation, in is_bounded_bilinear_map_apply (in bounded_linear_maps.lean), together with other statements of the same flavor (for instance, the composition of two continuous linear maps is a bilinear operation). I don't know what do to with this -- at least registering the fact that a bounded bilinear map from E x F to G gives rise to a map E ->L[k] -> F ->L[k] G, from which your definition is then a particular case.

All these maps have been registered as (unbundled) bounded bilinear maps because this is the way it has been the most useful for applications, as far as I can tell.

There is the same question for the other definitions: should we register them as bilinear maps, or in which context. The question is really the applications: if you have an application in which your form is more convenient, then we should go this way. If this is just generalization for the sake of generalizing, maybe we should instead wait and see what is needed next.

[eric-wieser]

This is generalizing for the sake of consistency, not generalization itself - we already have the fully-bundled version for add_monoid_hom, this just adds them for two other homs

[sgouezel]

ok. Then I'd still like the continuous version to be a continuous linear map, not just a linear map, and then we can merge this. Also, was there a consensus on the renaming part?

[eric-wieser]

Renaming was something I was planning to leave for a follow-up.

[eric-wieser]

Then I'd still like the continuous version to be a continuous linear map,

I don't have the knowledge of how to prove this. To summarize:

1. Before the PR: apply : E → (E →L[𝕜] F) →L[𝕜] F
2. With the PR: apply : E →ₗ[𝕜] (E →L[𝕜] F) →L[𝕜] F
3. Your proposal: apply : E →L[𝕜] (E →L[𝕜] F) →L[𝕜] F`

While obviously 3 would be ideal, I have no idea if it's even true, and proving it is outside of my area of expertise.
Is there any harm in merging this as is? It still makes things like apply (a + b) = apply a + apply b provable by simp, which previously was not true. If you really strongly object, I can remove the map_add' := λ _ _, ext $ λ f, f.map_add _ _, lines, but I don't see why proving less is better than proving more.

[sgouezel]

I have pushed a version with the continuous version. If you're happy with it, you can merge yourself.
bors d+
Thanks!

[bors]

✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[eric-wieser]

bors r+

Thanks!

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests