English
Let u: N → E and v: N → N be functions with the usual growth assumptions: the supremum growth of v is finite and nonzero, v grows without bound in a suitable sense, and u takes nonnegative values frequently. Then the linear growth of the composition is bounded above by the product of the linear growth of v and the linear growth of u; i.e. linearGrowthSup(u ∘ v) ≤ linearGrowthSup(v) · linearGrowthSup(u).
Русский
Пусть u: ℕ → EReal и v: ℕ → ℕ удовлетворяют обычным предположениям о росте: линейный рост (верхняя стадия) функции v конечен и ненулевой, v растёт без ограничений в соответствующем смысле, а значения u часто неотрицательны. Тогда линейный рост композиции ограничен наверху произведением соответствующих линейных ростов: linearGrowthSup(u ∘ v) ≤ linearGrowthSup(v) · linearGrowthSup(u).
LaTeX
$$$\operatorname{linearGrowthSup}(u \circ v) \le \operatorname{linearGrowthSup}(v) \cdot \operatorname{linearGrowthSup}(u)$$$
Lean4
theorem linearGrowthSup_comp_le (hu : ∃ᶠ n in atTop, 0 ≤ u n) (hv₀ : (linearGrowthSup fun n ↦ v n : EReal) ≠ 0)
(hv₁ : (linearGrowthSup fun n ↦ v n : EReal) ≠ ⊤) (hv₂ : Tendsto v atTop atTop) :
linearGrowthSup (u ∘ v) ≤ (linearGrowthSup fun n ↦ v n : EReal) * linearGrowthSup u :=
by
have v_0 := hv₀.symm.lt_of_le <| (linearGrowthInf_natCast_nonneg v).trans (liminf_le_limsup)
refine le_mul_of_forall_lt (.inl v_0) (.inl hv₁) ?_
refine fun a v_a b u_b ↦ Eventually.linearGrowthSup_le ?_
have b_0 : 0 ≤ b := by
rw [← linearGrowthInf_const zero_ne_bot zero_ne_top]
exact (linearGrowthInf_le_linearGrowthSup_of_frequently_le hu).trans u_b.le
have uv_b : ∀ᶠ n in atTop, u (v n) ≤ b * v n := eventually_map.1 ((eventually_le_mul u_b).filter_mono hv₂)
filter_upwards [uv_b, eventually_lt_of_limsup_lt v_a, eventually_gt_atTop 0] with n uvn_b vn_a n_0
replace vn_a := ((div_lt_iff (Nat.cast_pos'.2 n_0) (natCast_ne_top n)).1 vn_a).le
rw [comp_apply, mul_comm a b, mul_assoc b a]
exact uvn_b.trans <| by gcongr
