English
Let u be monotone, and let hv₀ and hv₁ denote that the linear growth sup of the sequence v is finite and nonzero. Then the infimum growth of the composed sequence satisfies an upper bound: expGrowthInf(u ∘ v) ≤ (linearGrowthSup v) · expGrowthInf u.
Русский
Пусть u монотонна; если линейная верхняя граница роста последовательности v конечна и ненулевая, то expGrowthInf(u ∘ v) не превысит (linearGrowthSup v) · expGrowthInf u.
LaTeX
$$$\expGrowthInf (u \circ v) \le (\text{linearGrowthSup } v) \cdot \expGrowthInf u$$$
Lean4
theorem _root_.Monotone.expGrowthInf_comp_le (h : Monotone u) (hv₀ : (linearGrowthSup fun n ↦ v n : EReal) ≠ 0)
(hv₁ : (linearGrowthSup fun n ↦ v n : EReal) ≠ ⊤) :
expGrowthInf (u ∘ v) ≤ (linearGrowthSup fun n ↦ v n : EReal) * expGrowthInf u :=
(log_monotone.comp h).linearGrowthInf_comp_le hv₀ hv₁
