expGrowthInf_comp_mul — Mathlib

English

For a monotone u and nonzero m, expGrowthInf (n ↦ u(m n)) = m · expGrowthInf u.

Русский

Для монотонной u и ненулевого m: expGrowthInf (n ↦ u(m n)) = m · expGrowthInf u.

LaTeX

$$$\expGrowthInf (\lambda n. u(m \cdot n)) = m \cdot \expGrowthInf u$$$

Lean4

theorem _root_.Monotone.expGrowthInf_comp_mul {m : ℕ} (h : Monotone u) (hm : m ≠ 0) :
    expGrowthInf (fun n ↦ u (m * n)) = m * expGrowthInf u :=
  (log_monotone.comp h).linearGrowthInf_comp_mul hm

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