[Merged by Bors] - feat(analysis/normed_space/is_R_or_C): add three lemmas on bounds of linear maps over is_R_or_C.

[kkytola]

Adding lemmas linear_map.bound_of_sphere_bound, linear_map.bound_of_ball_bound, continuous_linear_map.op_norm_bound_of_ball_bound as a preparation of a PR on Banach-Alaoglu theorem.

---

I separated the three first lemmas of the proof https://github.com/kkytola/lean-questions/blob/main/alaoglu.lean of Banach-Alaoglu theorem, which I plan to PR next.

These three clearly need golfing and improving, but I hope the reviewers could help me with that. Doing them only in the generality of [is_R_or_C k] was discussed on Zulip https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/linear_map_bound_of_ball_bound/near/258265122.

I tend to believe the formulations are practical for real and complex linear maps, but in fact I don't know whether these are wanted in mathlib in the first place. Also I am not exactly sure where (in which file and which section) these should be placed, if at all. They require importing is_R_or_C, which in operator_norm.lean seemed to create a cyclic import.

[sgouezel]

This looks good to me. I'd put them in a new file, however, to avoid importing complex stuff in bounded_linear_maps. Maybe create a new file normed_space.is_R_or_C where we could gather facts that are specific to R or C?

[kkytola]

This looks good to me. I'd put them in a new file, however, to avoid importing complex stuff in bounded_linear_maps. Maybe create a new file normed_space.is_R_or_C where we could gather facts that are specific to R or C?

Sounds good, I did that. Thank you!

[PatrickMassot]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

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