mul_param — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem mul_param (hf : SuperpolynomialDecay l k f) : SuperpolynomialDecay l k (f * k) :=
  hf.param_mul.congr fun _ => mul_comm _ _

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