opNNNorm_le_of_lipschitz — Mathlib

English

If one controls the norm of every A x with a nonzero x, then the operator norm is bounded by the same bound M.

Русский

Если для каждого x≠0 выполняется bound на ‖A x‖, тогда норма оператора ≤ bound.

LaTeX

$$$\\|f\\|_{+} \\le M$ from $\\forall x\\, \\|x\\|_{+} \\neq 0 \\rightarrow \\|f x\\|_{+} \\le M \\|x\\|_{+}$$$

Lean4

theorem opNNNorm_le_of_lipschitz {f : E →SL[σ₁₂] F} {K : ℝ≥0} (hf : LipschitzWith K f) : ‖f‖₊ ≤ K :=
  opNorm_le_of_lipschitz hf

Похожие утверждения