expGrowthSup_comp_mul — Mathlib

English

For a monotone u and nonzero m, expGrowthSup (fun n => u (m n)) = m · expGrowthSup u.

Русский

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

LaTeX

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

Lean4

theorem _root_.Monotone.expGrowthSup_comp_mul {m : ℕ} (h : Monotone u) (hm : m ≠ 0) :
    expGrowthSup (fun n ↦ u (m * n)) = m * expGrowthSup u :=
  (log_monotone.comp h).linearGrowthSup_comp_mul hm

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