expGrowthSup_comp — Mathlib

English

For a monotone u and nonzero m, the index-scaling identity holds: expGrowthSup (n ↦ u (m n)) = m · expGrowthSup u.

Русский

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

LaTeX

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

Lean4

theorem _root_.Monotone.expGrowthSup_comp {a : EReal} (h : Monotone u)
    (hv : Tendsto (fun n ↦ (v n : EReal) / n) atTop (𝓝 a)) (ha : a ≠ 0) (ha' : a ≠ ⊤) :
    expGrowthSup (u ∘ v) = a * expGrowthSup u :=
  (log_monotone.comp h).linearGrowthSup_comp hv ha ha'

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