norm_apply_le_of_nonneg — Mathlib

English

For a positive linear map f and x ≥ 0, the norm of f(x) is bounded by the norm of f(1) times the norm of x.

Русский

Для положительного линейного отображения f и x ≥ 0, норма f(x) ≤ норма f(1) · норма x.

LaTeX

$$$\|f(x)\| \le \|f(1)\| \cdot \|x\|$ for $x \ge 0$$$

Lean4

theorem norm_apply_le_of_nonneg [StarOrderedRing B₂] (f : B₁ →ₚ[ℂ] B₂) (x : B₁) (hx : 0 ≤ x) : ‖f x‖ ≤ ‖f 1‖ * ‖x‖ :=
  by
  have h : ‖‖x‖‖ = ‖x‖ := by simp
  rw [mul_comm, ← h, ← norm_smul ‖x‖ (f 1)]
  clear h
  refine CStarAlgebra.norm_le_norm_of_nonneg_of_le (f.map_nonneg hx) ?_
  rw [← Complex.coe_smul, ← LinearMapClass.map_smul f]
  gcongr
  rw [← Algebra.algebraMap_eq_smul_one]
  exact IsSelfAdjoint.le_algebraMap_norm_self <| .of_nonneg hx

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