superpolynomialDecay_mul_const_iff

English

If f decays along l with k, then multiplied by a nonzero constant or by k^z preserves decay for all z ∈ ℤ.

Русский

Если f затухает вдоль l по k, то умножение на константу c ≠ 0 или на k^z сохраняет затухание для всех z ∈ ℤ.

LaTeX

$$$\mathrm{SuperpolynomialDecay}(l,k,f) \Rightarrow (\forall c \neq 0, \mathrm{SuperpolynomialDecay}(l,k,\lambda n. c \cdot f(n))) \,\text{и}\, \mathrm{SuperpolynomialDecay}(l,k,f) \Rightarrow \forall z \in \mathbb{Z}, \mathrm{SuperpolynomialDecay}(l,k,\lambda a. (k(a))^z \cdot f(a))$$$

Lean4

theorem superpolynomialDecay_mul_const_iff [ContinuousMul β] {c : β} (hc0 : c ≠ 0) :
    (SuperpolynomialDecay l k fun n => f n * c) ↔ SuperpolynomialDecay l k f :=
  ⟨fun h => (h.mul_const c⁻¹).congr fun x => by simp [mul_assoc, mul_inv_cancel₀ hc0], fun h => h.mul_const c⟩

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