inv_param_mul — Mathlib

English

Let l be a filter on α, k: α → β with Tendsto k l atTop, and f: α → β that decays superpolynomially along k. Then k^{-1} · f also decays superpolynomially along k.

Русский

Пусть l — фильтр на α, k: α → β с Tendsto(k,l,atTop), и f: α → β имеет сверхполиномиальное затухание вдоль k. Тогда k^{-1} · f также имеет сверхполиномиальное затухание вдоль k.

LaTeX

$$$\\operatorname{Tendsto}(k,l,\\operatorname{atTop}) \\Rightarrow \\bigl( \\operatorname{SuperpolynomialDecay}(l,k,f) \\Rightarrow \\operatorname{SuperpolynomialDecay}(l,k,k^{-1}\\cdot f) \\bigr) $$$

Lean4

theorem inv_param_mul (hk : Tendsto k l atTop) (hf : SuperpolynomialDecay l k f) : SuperpolynomialDecay l k (k⁻¹ * f) :=
  by simpa using hf.param_zpow_mul hk (-1)

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