English
Let f be a bounded linear operator between normed spaces. For every v, the sesquilinear form associated to f evaluated at v has norm bounded by the product of the operator norm of f and the norm of v, i.e., ‖toSesqForm(f)(v)‖ ≤ ‖f‖·‖v‖.
Русский
Пусть f — ограниченный линейный оператор между нормированными пространствами. Для каждого v нормируемая форма, соответствующая f, удовлетворяет неравенству ‖toSesqForm(f)(v)‖ ≤ ‖f‖·‖v‖.
LaTeX
$$$\|\operatorname{toSesqForm}(f)(v)\| \le \|f\| \cdot \|v\|$$$
Lean4
theorem toSesqForm_apply_norm_le {f : E →L[𝕜] E'} {v : E'} : ‖toSesqForm f v‖ ≤ ‖f‖ * ‖v‖ :=
by
refine opNorm_le_bound _ (by positivity) fun x ↦ ?_
have h₁ : ‖f x‖ ≤ ‖f‖ * ‖x‖ := le_opNorm _ _
have h₂ := @norm_inner_le_norm 𝕜 E' _ _ _ v (f x)
calc
‖⟪v, f x⟫‖ ≤ ‖v‖ * ‖f x‖ := h₂
_ ≤ ‖v‖ * (‖f‖ * ‖x‖) := (mul_le_mul_of_nonneg_left h₁ (norm_nonneg v))
_ = ‖f‖ * ‖v‖ * ‖x‖ := by ring
