opNorm_le_of_shell — Mathlib

English

If f is controlled on a shell between radii ε and 1, then ‖f‖ ≤ C for the bound C.

Русский

Если управление f на оболочке между радиусами ε и 1 дает предел C, то ‖f‖ ≤ C.

LaTeX

$$$\\|f\\| \\le C \\quad\\text{если } ∀ x, ε < \\|x\\| < 1 \\Rightarrow \\|f x\\| ≤ C \\|x\\|$$$

Lean4

theorem opNorm_le_of_shell {f : E →SL[σ₁₂] F} {ε C : ℝ} (ε_pos : 0 < ε) (hC : 0 ≤ C) {c : 𝕜} (hc : 1 < ‖c‖)
    (hf : ∀ x, ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖) : ‖f‖ ≤ C :=
  f.opNorm_le_bound' hC fun _ hx => SemilinearMapClass.bound_of_shell_semi_normed f ε_pos hc hf hx

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