superpolynomialDecay_const_mul_iff

English

For nonzero c, (f) · c has the same decay behavior as f; more precisely, decay of f implies decay of f · c and vice versa when c ≠ 0.

Русский

Для непустой константы c затухание f эквивалентно затуханию f · c.

LaTeX

$$$\text{[ContinuousMul]} \; \{c\}\; (c \neq 0) \Rightarrow \big( \mathrm{SuperpolynomialDecay}(l,k,\lambda n. f(n) \cdot c) \iff \mathrm{SuperpolynomialDecay}(l,k,f) \big)$$$

Lean4

theorem superpolynomialDecay_const_mul_iff [ContinuousMul β] {c : β} (hc0 : c ≠ 0) :
    (SuperpolynomialDecay l k fun n => c * f n) ↔ SuperpolynomialDecay l k f :=
  ⟨fun h => (h.const_mul c⁻¹).congr fun x => by simp [← mul_assoc, inv_mul_cancel₀ hc0], fun h => h.const_mul c⟩

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