English
If M ∈ CStarMatrix(m,n,A) satisfies the bound ‖⟪w, toCLM M v⟫_A‖ ≤ C‖v‖‖w‖ for all vectors v,w in the corresponding modules, then the operator (matrix) norm satisfies ‖M‖ ≤ C.
Русский
Если M ∈ CStarMatrix(m,n,A) удовлетворяет неравенству ‖⟪w, toCLM M v⟫_A‖ ≤ C‖v‖‖w‖ для всех векторов v, w, то нормa оператора матрицы удовлетворяет ‖M‖ ≤ C.
LaTeX
$$$$\\forall v,w, \\ \\|\\langle w, \\Phi(M) v\\rangle_A\\| \\le C \\|v\\| \\|w\\| \\;\\Rightarrow\\; \\|M\\| \\le C.$$$$
Lean4
theorem norm_le_of_forall_inner_le {M : CStarMatrix m n A} {C : ℝ≥0} (h : ∀ v w, ‖⟪w, toCLM M v⟫_A‖ ≤ C * ‖v‖ * ‖w‖) :
‖M‖ ≤ C := by
refine (toCLM M).opNorm_le_bound (by simp) fun v ↦ ?_
obtain (h₀ | h₀) := (norm_nonneg (toCLM M v)).eq_or_lt
· rw [← h₀]
positivity
· refine le_of_mul_le_mul_right ?_ h₀
simpa [← sq, norm_sq_eq A] using h ..
