param_zpow_mul — Mathlib

English

If f decays, then f(x) multiplied by a polynomial in k(x) also decays for all polynomials.

Русский

Если f затухает, то f(x) умноженное на полином в k(x) тоже затухает.

LaTeX

$$$\mathrm{SuperpolynomialDecay}(l,k,f) \Rightarrow \forall p \in \mathbb{β}[X], \mathrm{SuperpolynomialDecay}(l,k,\lambda x. f(x) \cdot p(k(x)))$$$

Lean4

theorem param_zpow_mul (hk : Tendsto k l atTop) (hf : SuperpolynomialDecay l k f) (z : ℤ) :
    SuperpolynomialDecay l k fun a => k a ^ z * f a :=
  by
  rw [superpolynomialDecay_iff_zpow_tendsto_zero _ hk] at hf ⊢
  refine fun z' => (hf <| z' + z).congr' ((hk.eventually_ne_atTop 0).mono fun x hx => ?_)
  simp [zpow_add₀ hx, mul_assoc]

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