mul_param_zpow — Mathlib

English

For any z ∈ ℤ, the function a ↦ f(a) · (k(a))^z decays if f decays.

Русский

Для любого z ∈ ℤ функция a ↦ f(a) · (k(a))^z затухает, если f затухает.

LaTeX

$$$\forall z \in \mathbb{Z}, \mathrm{SuperpolynomialDecay}(l,k,f) \Rightarrow \mathrm{SuperpolynomialDecay}(l,k,\lambda a. f(a) \cdot (k(a))^z)$$$

Lean4

theorem mul_param_zpow (hk : Tendsto k l atTop) (hf : SuperpolynomialDecay l k f) (z : ℤ) :
    SuperpolynomialDecay l k fun a => f a * k a ^ z :=
  (hf.param_zpow_mul hk z).congr fun _ => mul_comm _ _

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