superpolynomialDecay_iff_zpow_tendsto_zero

English

If f decays, then for any polynomial p, the weighted f by p(k(x)) decays.

Русский

Если f затухает, тогда взвешивание полиномом p(k(x)) сохраняет затухание.

LaTeX

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

Lean4

theorem superpolynomialDecay_iff_zpow_tendsto_zero (hk : Tendsto k l atTop) :
    SuperpolynomialDecay l k f ↔ ∀ z : ℤ, Tendsto (fun a : α => k a ^ z * f a) l (𝓝 0) :=
  by
  refine ⟨fun h z => ?_, fun h n => by simpa only [zpow_natCast] using h (n : ℤ)⟩
  by_cases hz : 0 ≤ z
  · unfold Tendsto
    lift z to ℕ using hz
    simpa using h z
  · have : Tendsto (fun a => k a ^ z) l (𝓝 0) := Tendsto.comp (tendsto_zpow_atTop_zero (not_le.1 hz)) hk
    have h : Tendsto f l (𝓝 0) := by simpa using h 0
    exact zero_mul (0 : β) ▸ this.mul h

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