English
If u and v are sequences with certain nonnegativity and monotonicity hypotheses, then the product of linearGrowthInf of a bound with u is bounded by linearGrowthInf of a composed bound.
Русский
При соблюдении условий неотрицательности и монотонности последовательностей, произведение lower роста единичного множителя с u ограничивает линейный Inf композиции.
LaTeX
$$$ (\text{hu} : 0 \leᶠ u) (\text{hv} : Tendsto v atTop atTop) \Rightarrow (linearGrowthInf (fun n \mapsto (v n).cast) \cdot linearGrowthInf u) \le linearGrowthInf (u \circ v) $$$
Lean4
theorem le_linearGrowthInf_comp (hu : 0 ≤ᶠ[atTop] u) (hv : Tendsto v atTop atTop) :
(linearGrowthInf fun n ↦ v n : EReal) * linearGrowthInf u ≤ linearGrowthInf (u ∘ v) :=
by
have uv_0 : 0 ≤ linearGrowthInf (u ∘ v) :=
by
rw [← linearGrowthInf_const zero_ne_bot zero_ne_top]
exact linearGrowthInf_eventually_monotone (hv.eventually hu)
apply EReal.mul_le_of_forall_lt_of_nonneg (linearGrowthInf_natCast_nonneg v) uv_0
refine fun a ⟨_, a_v⟩ b ⟨b_0, b_u⟩ ↦ Eventually.le_linearGrowthInf ?_
have b_uv := eventually_map.1 ((eventually_mul_le b_u).filter_mono hv)
filter_upwards [b_uv, eventually_lt_of_lt_liminf a_v, eventually_gt_atTop 0] with n b_uvn a_vn n_0
replace a_vn := ((lt_div_iff (Nat.cast_pos'.2 n_0) (natCast_ne_top n)).1 a_vn).le
rw [comp_apply, mul_comm a b, mul_assoc b a]
exact b_uvn.trans' <| by gcongr
