norm_pow_two_pow

Mathlib.Analysis.CStarAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#IsSelfAdjoint.norm_pow_two_pow

English

If x is self-adjoint, then for every n, the norm of x^{2^n} equals the norm of x raised to 2^n.

Русский

Если x сам-сопряжён, то для каждого n нормa x^{2^n} равна норме x^{2^n}.

LaTeX

$$$ \|x^{2^{n}}\| = \|x\|^{2^{n}} $$$

Lean4

theorem norm_pow_two_pow {x : E} (hx : IsSelfAdjoint x) (n : ℕ) : ‖x ^ 2 ^ n‖ = ‖x‖ ^ 2 ^ n :=
  congr($(hx.nnnorm_pow_two_pow n))

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru