superpolynomialDecay_mul_param_iff

English

Let hk be Tendsto k l atTop. Then SuperpolynomialDecay l k (f · k) is equivalent to SuperpolynomialDecay l k f.

Русский

Пусть hk — Tendsto k l atTop. Тогда SuperpolynomialDecay l k (f · k) эквивалентно SuperpolynomialDecay l k f.

LaTeX

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

Lean4

theorem superpolynomialDecay_mul_param_iff (hk : Tendsto k l atTop) :
    SuperpolynomialDecay l k (f * k) ↔ SuperpolynomialDecay l k f := by
  simpa [mul_comm k] using superpolynomialDecay_param_mul_iff f hk

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