opNorm_bound_of_ball_bound — Mathlib

English

The operator norm of a continuous linear map is bounded by a bound derived from its action on a ball: ||f|| ≤ c/r, assuming ∥f z∥ ≤ c for z in the ball of radius r.

Русский

Пусть линейное отображение ограничено на шаре радиуса r; тогда нормa оператора удовлетворяет ∥f∥ ≤ c/r.

LaTeX

$$$\\|f\\| \\le \\frac{c}{r}$$$

Lean4

theorem opNorm_bound_of_ball_bound {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : StrongDual 𝕜 E)
    (h : ∀ z ∈ closedBall (0 : E) r, ‖f z‖ ≤ c) : ‖f‖ ≤ c / r :=
  by
  apply ContinuousLinearMap.opNorm_le_bound
  · apply div_nonneg _ r_pos.le
    exact (norm_nonneg _).trans (h 0 (by simp only [norm_zero, mem_closedBall, dist_zero_left, r_pos.le]))
  apply LinearMap.bound_of_ball_bound' r_pos
  exact fun z hz => h z hz

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