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