trans_eventually_abs_le — Mathlib

English

If f decays along l with k, then multiplying by k^z decays for any integer z.

Русский

Если f затухает вдоль l по k, то умножение на k^z как целое число z сохраняет затухание.

LaTeX

$$$\mathrm{SuperpolynomialDecay}(l,k,f) \Rightarrow \forall z \in \mathbb{Z}, \mathrm{SuperpolynomialDecay}(l,k,\lambda a. (k(a))^z \cdot f(a))$$$

Lean4

theorem trans_eventually_abs_le (hf : SuperpolynomialDecay l k f) (hfg : abs ∘ g ≤ᶠ[l] abs ∘ f) :
    SuperpolynomialDecay l k g :=
  by
  rw [superpolynomialDecay_iff_abs_tendsto_zero] at hf ⊢
  refine fun z =>
    tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds (hf z) (Eventually.of_forall fun x => abs_nonneg _)
      (hfg.mono fun x hx => ?_)
  calc
    |k x ^ z * g x| = |k x ^ z| * |g x| := abs_mul (k x ^ z) (g x)
    _ ≤ |k x ^ z| * |f x| := by gcongr _ * ?_; exact hx
    _ = |k x ^ z * f x| := (abs_mul (k x ^ z) (f x)).symm

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