nnnorm_pow_two_pow — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem nnnorm_pow_two_pow {x : E} (hx : IsSelfAdjoint x) (n : ℕ) : ‖x ^ 2 ^ n‖₊ = ‖x‖₊ ^ 2 ^ n := by
  induction n with
  | zero => simp only [pow_zero, pow_one]
  | succ k hk => rw [pow_succ', pow_mul', sq, (hx.pow (2 ^ k)).nnnorm_mul_self, hk, pow_mul']

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