param_mul — Mathlib

English

If f decays along l with parameter k, then the pointwise product a ↦ k(a) · f(a) also decays.

Русский

Если f затухает вдоль l по параметру k, то произведение по точкам a ↦ k(a) · f(a) также затухает.

LaTeX

$$$\mathrm{SuperpolynomialDecay}(l,k,f) \Rightarrow \mathrm{SuperpolynomialDecay}(l,k,\lambda a. k(a) \cdot f(a))$$$

Lean4

theorem param_mul (hf : SuperpolynomialDecay l k f) : SuperpolynomialDecay l k (k * f) := fun z =>
  tendsto_nhds.2 fun s hs hs0 =>
    l.sets_of_superset ((tendsto_nhds.1 (hf <| z + 1)) s hs hs0) fun x hx => by
      simpa only [Set.mem_preimage, Pi.mul_apply, ← mul_assoc, ← pow_succ] using hx

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