norm_posPart_le — Mathlib

English

For any a in A, the norm of its positive part is bounded by the norm of a: ||a^+|| ≤ ||a||.

Русский

Для любого a в A норма его положительной части не превосходит норму a: ||a^+|| ≤ ||a||.

LaTeX

$$‖a^+‖ ≤ ‖a‖$$

Lean4

@[simp]
theorem norm_posPart_le (a : A) : ‖a⁺‖ ≤ ‖a‖ :=
  by
  by_cases ha : IsSelfAdjoint a
  case neg => simp [CFC.posPart_def, cfcₙ_apply_of_not_predicate a ha]
  refine norm_cfcₙ_le fun x hx ↦ ?_
  obtain (h | h) := le_or_gt x 0
  · simp [posPart_def, max_eq_right h]
  · simp only [posPart_def, max_eq_left h.le]
    exact NonUnitalIsometricContinuousFunctionalCalculus.norm_quasispectrum_le a hx ha

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