English
If f decays along l with k, then for any z ∈ ℤ, the function a ↦ f(a) · (k(a))^z decays.
Русский
Если f затухает вдоль l по k, то для любого z ∈ ℤ функция a ↦ f(a) · (k(a))^z затухает.
LaTeX
$$$\mathrm{SuperpolynomialDecay}(l,k,f) \Rightarrow \forall z \in \mathbb{Z}, \mathrm{SuperpolynomialDecay}(l,k,\lambda a. f(a) \cdot (k(a))^z)$$$
Lean4
theorem superpolynomialDecay_iff_abs_isBoundedUnder (hk : Tendsto k l atTop) :
SuperpolynomialDecay l k f ↔ ∀ z : ℕ, IsBoundedUnder (· ≤ ·) l fun a : α => |k a ^ z * f a| :=
by
refine
⟨fun h z => Tendsto.isBoundedUnder_le (Tendsto.abs (h z)), fun h =>
(superpolynomialDecay_iff_abs_tendsto_zero l k f).2 fun z => ?_⟩
obtain ⟨m, hm⟩ := h (z + 1)
have h1 : Tendsto (fun _ : α => (0 : β)) l (𝓝 0) := tendsto_const_nhds
have h2 : Tendsto (fun a : α => |(k a)⁻¹| * m) l (𝓝 0) :=
zero_mul m ▸ Tendsto.mul_const m ((tendsto_zero_iff_abs_tendsto_zero _).1 hk.inv_tendsto_atTop)
refine
tendsto_of_tendsto_of_tendsto_of_le_of_le' h1 h2 (Eventually.of_forall fun x => abs_nonneg _)
((eventually_map.1 hm).mp ?_)
refine (hk.eventually_ne_atTop 0).mono fun x hk0 hx => ?_
refine Eq.trans_le ?_ (mul_le_mul_of_nonneg_left hx <| abs_nonneg (k x)⁻¹)
rw [← abs_mul, ← mul_assoc, pow_succ', ← mul_assoc, inv_mul_cancel₀ hk0, one_mul]
