antilipschitz_of_norm_ge — Mathlib

English

The operator norm of a seminormed group homomorphism is the greatest lower bound of all its nonnegative bounds C such that ∥f(x)∥ ≤ C∥x∥ for all x.

Русский

Операторная нормa гомоморфизма нормированных аддитивных групп есть наименьшее верхнее ограничение среди всех неотрицательных C, удовлетворяющих ∥f(x)∥ ≤ C∥x∥ для всех x.

LaTeX

$$$‖f‖ = \\inf\\{\,c\\ge0 : ∀x,\\ ‖f x‖ ≤ c \\|x\\|\,\\}$$$

Lean4

theorem antilipschitz_of_norm_ge {K : ℝ≥0} (h : ∀ x, ‖x‖ ≤ K * ‖f x‖) : AntilipschitzWith K f :=
  AntilipschitzWith.of_le_mul_dist fun x y => by simpa only [dist_eq_norm, map_sub] using h (x - y)

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