bound_of_ball_bound' — Mathlib

English

If a linear map f is bounded on the closed ball of radius r, then it satisfies the ball-bound inequality: ∥f z∥ ≤ (c/r) ∥z∥ for all z.

Русский

Если линейное отображение ограничено на замкнутой сфере радиуса r, то ∥f z∥ ≤ (c/r) ∥z∥ для всех z.

LaTeX

$$$\\forall z, \\|f z\\| \\le \\frac{c}{r} \\|z\\|$$$

Lean4

/-- `LinearMap.bound_of_ball_bound` is a version of this over arbitrary nontrivially normed fields.
It produces a less precise bound so we keep both versions. -/
theorem bound_of_ball_bound' {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →ₗ[𝕜] 𝕜) (h : ∀ z ∈ closedBall (0 : E) r, ‖f z‖ ≤ c)
    (z : E) : ‖f z‖ ≤ c / r * ‖z‖ :=
  f.bound_of_sphere_bound r_pos c (fun z hz => h z hz.le) z

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