mul_star_le_algebraMap_norm_sq — Mathlib

English

In any C*-algebra A, for any a, the element a a* is bounded above by the real-algebra image of ‖a‖^2, i.e., a a* ≤ algebraMap ℝ A(‖a‖^2).

Русский

В C*-алгебре A для любого a выполняется неравенство: a a* ≤ algebraMapℝ A(‖a‖^2).

LaTeX

$$$a\,a^{*} \\le \\operatorname{algebraMap}_{\\mathbb{R}} A\\bigl( \\|a\\|^{2} \\bigr)$$$

Lean4

theorem mul_star_le_algebraMap_norm_sq {a : A} : a * star a ≤ algebraMap ℝ A (‖a‖ ^ 2) :=
  by
  have : a * star a ≤ algebraMap ℝ A ‖a * star a‖ := IsSelfAdjoint.le_algebraMap_norm_self
  rwa [CStarRing.norm_self_mul_star, ← pow_two] at this

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