param_inv_mul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem param_inv_mul (hk : Tendsto k l atTop) (hf : SuperpolynomialDecay l k f) : SuperpolynomialDecay l k (f * k⁻¹) :=
  (hf.inv_param_mul hk).congr fun _ => mul_comm _ _

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