English
For Tendsto k l atTop, SPD(l,k,f) iff f = o[l] k^z for all z ∈ ℤ.
Русский
При Tendsto k l atTop SPD(l,k,f) эквивалентно f = o[l] k^z для всех z ∈ ℤ.
LaTeX
$$$\\operatorname{Tendsto}(k,l,\\operatorname{atTop}) \\Rightarrow \\operatorname{SPD}(l,k,f) \\iff \\forall z \\in \\mathbb{Z},\\ f =o[l](k^{z}).$$$
Lean4
theorem superpolynomialDecay_iff_isBigO (hk : Tendsto k l atTop) :
SuperpolynomialDecay l k f ↔ ∀ z : ℤ, f =O[l] fun a : α => k a ^ z :=
by
refine (superpolynomialDecay_iff_zpow_tendsto_zero f hk).trans ?_
have hk0 : ∀ᶠ x in l, k x ≠ 0 := hk.eventually_ne_atTop 0
refine ⟨fun h z => ?_, fun h z => ?_⟩
· refine isBigO_of_div_tendsto_nhds (hk0.mono fun x hx hxz ↦ absurd hxz (zpow_ne_zero _ hx)) 0 ?_
have : (fun a : α => k a ^ z)⁻¹ = fun a : α => k a ^ (-z) := funext fun x => by simp
rw [div_eq_mul_inv, mul_comm f, this]
exact h (-z)
· suffices (fun a : α => k a ^ z * f a) =O[l] fun a : α => (k a)⁻¹ from IsBigO.trans_tendsto this hk.inv_tendsto_atTop
refine ((isBigO_refl (fun a => k a ^ z) l).mul (h (-(z + 1)))).trans ?_
refine .of_bound' <| hk0.mono fun a ha0 => ?_
simp [← zpow_add₀ ha0]
