le_opNorm_enorm — Mathlib

English

As in item 55703, the operator norm bound is equivalent to being Lipschitz with the same constant.

Русский

Как и в пункте 55703, ограничение нормы оператора эквивалентно тому, что отображение липшицево с той же константой.

LaTeX

$$$ \|f\| \le K \;\Leftrightarrow\; \text{LipschitzWith } K\, f $$$

Lean4

/-- The fundamental property of the operator norm, expressed with extended norms:
`‖f x‖ₑ ≤ ‖f‖ₑ * ‖x‖ₑ`. -/
theorem le_opNorm_enorm (x : E) : ‖f x‖ₑ ≤ ‖f‖ₑ * ‖x‖ₑ :=
  by
  simp_rw [← ofReal_norm]
  rw [← ENNReal.ofReal_mul (by positivity)]
  gcongr
  exact f.le_opNorm x

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