mul — Mathlib

English

If f and g both have superpolynomial decay along l with parameter k, then f · g also has superpolynomial decay (assuming the target space supports multiplication continuously).

Русский

Если f и g обладают сверхполиномиальным затуханием вдоль l по параметру k, то их произведение f · g тоже затухает сверхполиномиально.

LaTeX

$$$\mathrm{SuperpolynomialDecay}(l,k,f) \wedge \mathrm{SuperpolynomialDecay}(l,k,g) \Rightarrow \mathrm{SuperpolynomialDecay}(l,k,f\cdot g)$$$

Lean4

theorem mul [ContinuousMul β] (hf : SuperpolynomialDecay l k f) (hg : SuperpolynomialDecay l k g) :
    SuperpolynomialDecay l k (f * g) := fun z => by
  simpa only [mul_assoc, one_mul, mul_zero, pow_zero] using (hf z).mul (hg 0)

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