English
If there is a frequently 1 ≤ u_n and v tends to top along atTop, then expGrowthSup(u∘v) ≤ (linearGrowthSup v) · expGrowthSup u.
Русский
Если частота удовлетворения неравенства 1 ≤ u_n есть и v стремится к бесконечности, то expGrowthSup(u∘v) ≤ (linearGrowthSup v) · expGrowthSup u.
LaTeX
$$$\expGrowthSup(u \circ v) \le (\text{linearGrowthSup } v) \cdot \expGrowthSup(u)$$$
Lean4
theorem expGrowthSup_comp_le (hu : ∃ᶠ n in atTop, 1 ≤ u n) (hv₀ : (linearGrowthSup fun n ↦ v n : EReal) ≠ 0)
(hv₁ : (linearGrowthSup fun n ↦ v n : EReal) ≠ ⊤) (hv₂ : Tendsto v atTop atTop) :
expGrowthSup (u ∘ v) ≤ (linearGrowthSup fun n ↦ v n : EReal) * expGrowthSup u :=
by
apply linearGrowthSup_comp_le (u := log ∘ u) (hu.mono fun n h ↦ ?_) hv₀ hv₁ hv₂
rwa [comp_apply, zero_le_log_iff]
