superpolynomialDecay_param_mul_iff

English

If Tendsto k l atTop and f decays superpolynomially along k, then k · f also decays superpolynomially along k iff f does.

Русский

Если Tendsto k l atTop и f имеет сверхполиномиальное затухание вдоль k, то k · f затухает сверхполиномиально тогда и только тогда, когда f затухает.

LaTeX

$$$\\operatorname{Tendsto}(k,l,\\operatorname{atTop}) \\Rightarrow \\Bigl( \\operatorname{SuperpolynomialDecay}(l,k,k\\cdot f) \\iff \\operatorname{SuperpolynomialDecay}(l,k,f) \\Bigr).$$$

Lean4

theorem superpolynomialDecay_param_mul_iff (hk : Tendsto k l atTop) :
    SuperpolynomialDecay l k (k * f) ↔ SuperpolynomialDecay l k f :=
  ⟨fun h =>
    (h.inv_param_mul hk).congr' ((hk.eventually_ne_atTop 0).mono fun x hx => by simp [← mul_assoc, inv_mul_cancel₀ hx]),
    fun h => h.param_mul⟩

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