English
Let hk: Tendsto k l atTop. Then f decays faster than any power of k along l iff for every z ∈ ℤ we have f =o_l (k^z).
Русский
Пусть hk: Tendsto k l atTop. Тогда f имеет сверхполиномиальное затухание вдоль l относительно k тогда и только тогда, когда для каждого z ∈ ℤ выполняется f =o_l (k^z).
LaTeX
$$$$ \text{SuperpolynomialDecay } l\\ k\\ f \\iff \\forall z \\in \\mathbb{Z},\\ f =o_l (k^z) $$$$
Lean4
theorem superpolynomialDecay_iff_isLittleO (hk : Tendsto k l atTop) :
SuperpolynomialDecay l k f ↔ ∀ z : ℤ, f =o[l] fun a : α => k a ^ z :=
by
refine ⟨fun h z => ?_, fun h => (superpolynomialDecay_iff_isBigO f hk).2 fun z => (h z).isBigO⟩
have hk0 : ∀ᶠ x in l, k x ≠ 0 := hk.eventually_ne_atTop 0
have : (fun _ : α => (1 : β)) =o[l] k :=
isLittleO_of_tendsto' (hk0.mono fun x hkx hkx' => absurd hkx' hkx) (by simpa using hk.inv_tendsto_atTop)
have : f =o[l] fun x : α => k x * k x ^ (z - 1) := by
simpa using this.mul_isBigO ((superpolynomialDecay_iff_isBigO f hk).1 h <| z - 1)
refine this.trans_isBigO <| IsBigO.of_bound' <| hk0.mono fun x hkx => le_of_eq ?_
simp [← zpow_one_add₀ hkx]
