star_mul_le_algebraMap_norm_sq — Mathlib

English

Similarly, the left product a* a is also bounded above by the same real algebra image of ‖a‖^2.

Русский

Аналогично, левая пара a* a также ограничена той же вещественной алгебраической картой от ‖a‖^2.

LaTeX

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

Lean4

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

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