English
If a function f has finite L∞–norm (i.e., is essentially bounded), then for every natural number n, the pointwise power f^n also has finite L∞–norm. In particular, taking powers preserves membership in the ∞-normed Bochner space.
Русский
Если функция f имеет конечную ∞-норму (то есть она практически ограничена), то для любого натурального числа n функция f^n имеет конечную ∞-норму. Следовательно, возведение в степень сохраняет принадлежность к пространству с бесконечной нормой.
LaTeX
$$$\mathrm{Mem}_{\ell^{\infty}}(f^n) \quad\text{whenever}\quad \mathrm{Mem}_{\ell^{\infty}}(f).$$$
Lean4
theorem _root_.Memℓp.infty_pow {f : ∀ i, B i} (hf : Memℓp f ∞) (n : ℕ) : Memℓp (f ^ n) ∞ :=
(lpInftySubring B).pow_mem hf n
