[Merged by Bors] - feat(analysis/normed_space/operator_norm): variants of continuous_linear_map.lsmul and their properties

[RemyDegenne]

---

[hrmacbeth]

Sorry for not pointing you in this direction earlier, but I wonder if lsmul_left is the same as continuous_linear_map.to_span_singleton?

Also, I wrote continuous_linear_map.to_span_singleton when I was new to Lean and didn't know the library. Probably lsmul_left is a better name. Also I would not be at all surprised if the construction exists in another place under some third name. And certainly it's currently in the wrong place, it should live in topology.algebra.module rather than analysis.operator_norm with a definition like

def continuous_linear_map.to_span_singleton (a : E)  : 𝕜 →L[𝕜] E :=
{ cont := continuous_smul.comp (continuous_id.prod_mk continuous_const),
  .. linear_map.to_span_singleton 𝕜 E a }

Anyway, feel free to fix any of this, but also feel free to just convert the lsmul_left part of your PR into lemmas about continuous_linear_map.to_span_singleton and leave the rest of the mess for someone (me?) later.

[hrmacbeth]

Also (again sorry for not noticing this earlier) another way of representing lsmul_right E r is as r • (continuous_linear_map.id 𝕜 E). Is it perhaps better to just use the latter rather than making the former as a formal definition?

I checked: replacing lsmul_right F (μ s).to_real by (μ s).to_real • (continuous_linear_map.id 𝕜 F) in your other PR works out (without developing a lsmul_right theory). Most proofs become by simp [weighted_smul]. The lemma norm_weighted_smul_le needs a bit of reworking to pass through norm_id_le (or maybe it'd be worth salvaging your lemma

lemma norm_lsmul_right_le (r : 𝕜) : ∥lsmul_right E r∥ ≤ ∥r∥ :=
op_norm_le_bound _ (norm_nonneg _) (λ x, by rw [lsmul_right_apply, norm_smul])

in the adapted form

lemma norm_smul_id_le (r : 𝕜) : ∥r • (continuous_linear_map.id 𝕜 E)∥ ≤ ∥r∥ :=
by simpa using mul_le_mul_of_nonneg_left norm_id_le (norm_nonneg r)

[RemyDegenne]

I remove lsmul_right and renamed the lemmas about lsmul_left to apply to to_span_singleton. One lemma is placed near lsmul and not near to_smul_singleton because apparently some normed_space instance is not yet defined near to_span_singleton.

[hrmacbeth]

Thanks!

bors r+

[bors]

Build failed (retrying...):

• Build mathlib

[sgouezel]

Can you merge master and fix the conflict?

[bors]

Canceled.

[RemyDegenne]

I merged master and fixed the conflict.

[hrmacbeth]

Thanks!

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

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