English
If u is monotone, v tends to top, and the composition is taken, then the lower linear growth is nonnegative: 0 ≤ linearGrowthInf(u ∘ v).
Русский
Если u монотонна и v стремится к бесконечности, то линейный нижний рост композиции неотрицателен: 0 ≤ linearGrowthInf(u ∘ v).
LaTeX
$$$0 \le \operatorname{linearGrowthInf}(u \circ v)$$$
Lean4
theorem linearGrowthInf_comp_nonneg (h : Monotone u) (h' : u ≠ ⊥) (hv : Tendsto v atTop atTop) :
0 ≤ linearGrowthInf (u ∘ v) := by
simp only [ne_eq, funext_iff, not_forall] at h'
obtain ⟨m, hum⟩ := h'
have um_uvn : ∀ᶠ n in atTop, u m ≤ (u ∘ v) n :=
by
apply (eventually_map (P := fun n : ℕ ↦ u m ≤ u n)).2
exact (eventually_atTop.2 ⟨m, fun n m_n ↦ h m_n⟩).filter_mono hv
apply (linearGrowthInf_eventually_monotone um_uvn).trans'
rcases eq_or_ne (u m) ⊤ with hum' | hum'
· rw [hum', ← Pi.top_def, linearGrowthInf_top]; exact le_top
· rw [linearGrowthInf_const hum hum']
