English
For a StrongDual c of 𝕜 and a vector f in F, the operator smulRight c f has operator norm equal to the product of the norms: ||smulRight c f|| = ||c|| · ||f||.
Русский
Для сильного двойственного элемента c над 𝕜 и вектора f из F нормa оператора smulRight c f равна произведению норм: ||smulRight c f|| = ||c|| · ||f||.
LaTeX
$$$ \\|\\mathrm{smulRight}(c,f)\\| = \\|c\\| \\cdot \\|f\\| $$$
Lean4
/-- The norm of the tensor product of a scalar linear map and of an element of a normed space
is the product of the norms. -/
@[simp]
theorem norm_smulRight_apply (c : StrongDual 𝕜 E) (f : Fₗ) : ‖smulRight c f‖ = ‖c‖ * ‖f‖ :=
by
refine le_antisymm ?_ ?_
· refine opNorm_le_bound _ (by positivity) fun x => ?_
calc
‖c x • f‖ = ‖c x‖ * ‖f‖ := norm_smul _ _
_ ≤ ‖c‖ * ‖x‖ * ‖f‖ := by gcongr; apply le_opNorm
_ = ‖c‖ * ‖f‖ * ‖x‖ := by ring
· obtain hf | hf := (norm_nonneg f).eq_or_lt'
· simp [hf]
· rw [← le_div_iff₀ hf]
refine opNorm_le_bound _ (by positivity) fun x => ?_
rw [div_mul_eq_mul_div, le_div_iff₀ hf]
calc
‖c x‖ * ‖f‖ = ‖c x • f‖ := (norm_smul _ _).symm
_ = ‖smulRight c f x‖ := rfl
_ ≤ ‖smulRight c f‖ * ‖x‖ := le_opNorm _ _
