English
If u is monotone and linearGrowthSup(v) ≠ 0 and linearGrowthSup(v) ≠ ⊤, then (linearGrowthInf v) · (linearGrowthSup u) ≤ linearGrowthSup(u ∘ v).
Русский
Если u монотонна и линейный рост линейной функции v не равен 0 и не равен ⊤, то (linearGrowthInf v) · (linearGrowthSup u) ≤ linearGrowthSup(u ∘ v).
LaTeX
$$$\operatorname{linearGrowthInf}(\!v\! ) \cdot \operatorname{linearGrowthSup}(u) \le \operatorname{linearGrowthSup}(u \circ v)$$$
Lean4
theorem _root_.Monotone.le_linearGrowthSup_comp (h : Monotone u) (hv : (linearGrowthInf fun n ↦ v n : EReal) ≠ 0) :
(linearGrowthInf fun n ↦ v n : EReal) * linearGrowthSup u ≤ linearGrowthSup (u ∘ v) :=
by
have v_0 :=
hv.symm.lt_of_le
(linearGrowthInf_natCast_nonneg v)
-- WLOG, `u` is non-bot, and we can apply `mul_le_of_forall_lt_of_nonneg`.
by_cases u_0 : u = ⊥
· rw [u_0, linearGrowthSup_bot, mul_bot_of_pos v_0]; exact bot_le
apply
EReal.mul_le_of_forall_lt_of_nonneg v_0.le
(linearGrowthSup_comp_nonneg h u_0 (tendsto_atTop_of_linearGrowthInf_natCast_pos hv))
intro a ⟨a_0, a_v⟩ b ⟨b_0, b_u⟩
apply Frequently.le_linearGrowthSup
obtain ⟨a', a_a', a_v'⟩ := exists_between a_v
have a_top' := ne_top_of_lt a_v'
have a_0' := a_0.trans a_a'
have a_a_inv' : a'⁻¹ < a⁻¹ := inv_strictAntiOn (Set.mem_Ioi.2 a_0) (Set.mem_Ioi.2 a_0') a_a'
replace a_v' : ∀ᶠ n : ℕ in atTop, a' * n ≤ v n :=
by
filter_upwards [eventually_lt_of_lt_liminf a_v', eventually_gt_atTop 0] with n a_vn' n_0
exact (le_div_iff_mul_le (Nat.cast_pos'.2 n_0) (natCast_ne_top n)).1 a_vn'.le
suffices h : (∀ᶠ n : ℕ in atTop, a' * n ≤ v n) → ∃ᶠ n : ℕ in atTop, a * b * n ≤ (u ∘ v) n from h a_v'
rw [← frequently_imp_distrib]
replace b_u :=
((frequently_mul_le b_u).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', ⟨bn_un, _⟩, k, an_k', k_an⟩ := frequently_atTop.1 b_u M'
refine ⟨k, ?_, fun ak_vk' ↦ ?_⟩
· 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, div_le_iff_le_mul a_0' a_top'] at an_k'
rw [← EReal.div_eq_inv_mul, le_div_iff_mul_le a_0 (ne_top_of_lt a_a'), mul_comm] at k_an
have n_vk := Nat.cast_le.1 (an_k'.trans ak_vk')
exact le_trans (by gcongr) <| bn_un.trans (h n_vk)
