opNorm_le_of_unit_norm — Mathlib

English

A final version of the unit-norm bound: if ∥x∥ ≤ 1, then ∥f x∥ ≤ ∥f∥.

Русский

Финальная версия границы по единичной норме: если ∥x∥ ≤ 1, то ∥f x∥ ≤ ∥f∥.

LaTeX

$$$\\|x\\| \\le 1 \\Rightarrow \\|f x\\| ≤ \\|f\\|$$$

Lean4

/-- For a continuous real linear map `f`, if one controls the norm of every `f x`, `‖x‖ = 1`, then
one controls the norm of `f`. -/
theorem opNorm_le_of_unit_norm [NormedAlgebra ℝ 𝕜] {f : E →SL[σ₁₂] F} {C : ℝ} (hC : 0 ≤ C)
    (hf : ∀ x, ‖x‖ = 1 → ‖f x‖ ≤ C) : ‖f‖ ≤ C :=
  by
  refine opNorm_le_bound' f hC fun x hx => ?_
  have H₁ : ‖algebraMap _ 𝕜 ‖x‖⁻¹ • x‖ = 1 := by simp [norm_smul, inv_mul_cancel₀ hx]
  have H₂ : ‖x‖⁻¹ * ‖f x‖ ≤ C := by simpa [norm_smul] using hf _ H₁
  rwa [← div_eq_inv_mul, div_le_iff₀] at H₂
  exact (norm_nonneg x).lt_of_ne' hx

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