English
Let u be monotone; if linearGrowthSup(v) ≠ 0 and linearGrowthSup(v) ≠ ⊤, then linearGrowthInf(u ∘ v) ≤ linearGrowthSup(v) · linearGrowthInf(u).
Русский
Пусть u монотонна; если линейный рост верх неё композиции v не равен 0 и не равен ⊤, то линейный нижний рост (u ∘ v) не более произведения линейного роста v и линейного роста u.
LaTeX
$$$\operatorname{linearGrowthInf}(u \circ v) \le (\operatorname{linearGrowthSup}(v)) \cdot (\operatorname{linearGrowthInf}(u))$$$
Lean4
theorem _root_.Monotone.linearGrowthInf_comp_le (h : Monotone u) (hv₀ : (linearGrowthSup fun n ↦ v n : EReal) ≠ 0)
(hv₁ : (linearGrowthSup fun n ↦ v n : EReal) ≠ ⊤) :
linearGrowthInf (u ∘ v) ≤ (linearGrowthSup fun n ↦ v n : EReal) * linearGrowthInf u := by
-- First we apply `le_mul_of_forall_lt`.
by_cases u_0 : u = ⊥
· rw [u_0, Pi.bot_comp, linearGrowthInf_bot]; exact bot_le
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₁) fun a v_a b u_b ↦ ?_
have a_0 := v_0.trans v_a
have b_0 := (h.linearGrowthInf_nonneg u_0).trans_lt u_b
rcases eq_or_ne a ⊤ with rfl | a_top
· rw [top_mul_of_pos b_0]; exact le_top
apply Frequently.linearGrowthInf_le
obtain ⟨a', v_a', a_a'⟩ := exists_between v_a
have a_0' := v_0.trans v_a'
have a_a_inv' : a⁻¹ < a'⁻¹ := inv_strictAntiOn (Set.mem_Ioi.2 a_0') (Set.mem_Ioi.2 a_0) a_a'
replace v_a' : ∀ᶠ n : ℕ in atTop, v n ≤ a' * n :=
by
filter_upwards [eventually_lt_of_limsup_lt v_a', eventually_gt_atTop 0] with n vn_a' n_0
rw [mul_comm]
exact (div_le_iff_le_mul (Nat.cast_pos'.2 n_0) (natCast_ne_top n)).1 vn_a'.le
suffices h : (∀ᶠ n : ℕ in atTop, v n ≤ a' * n) → ∃ᶠ n : ℕ in atTop, (u ∘ v) n ≤ a * b * n from h v_a'
rw [← frequently_imp_distrib]
replace u_b :=
((frequently_le_mul u_b).and_eventually (eventually_gt_atTop 0)).and_eventually <|
EReal.eventually_atTop_exists_nat_between a_a_inv' (inv_nonneg_of_nonneg a_0'.le)
refine frequently_atTop.2 fun M ↦ ?_
obtain ⟨M', aM_M'⟩ := exists_nat_ge_mul a_top M
obtain ⟨n, n_M', ⟨un_bn, _⟩, k, an_k, k_an'⟩ := frequently_atTop.1 u_b M'
refine ⟨k, ?_, fun vk_ak' ↦ ?_⟩
· rw [mul_comm a, ← le_div_iff_mul_le a_0 a_top, EReal.div_eq_inv_mul] at aM_M'
apply Nat.cast_le.1 <| aM_M'.trans <| an_k.trans' _
gcongr
· rw [comp_apply, mul_comm a b, mul_assoc b a]
rw [← EReal.div_eq_inv_mul, le_div_iff_mul_le a_0' (ne_top_of_lt a_a'), mul_comm] at k_an'
rw [← EReal.div_eq_inv_mul, div_le_iff_le_mul a_0 a_top] at an_k
have vk_n := Nat.cast_le.1 (vk_ak'.trans k_an')
exact (h vk_n).trans <| un_bn.trans <| by gcongr
