param_pow_mul — Mathlib

English

For any n, f multiplied by k^n decays if f does.

Русский

Для любого n f умножается на k^n, затухание сохраняется.

LaTeX

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

Lean4

theorem param_pow_mul (hf : SuperpolynomialDecay l k f) (n : ℕ) : SuperpolynomialDecay l k (k ^ n * f) := by
  induction n with
  | zero => simpa only [one_mul, pow_zero] using hf
  | succ n hn => simpa only [pow_succ', mul_assoc] using hn.param_mul

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